Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Dimension-independent moments of low-degree Boolean polynomials

Lax253009.Hypercontractivity · concepts/Lax253009/Hypercontractivity.lean · lax-253009

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    For a Boolean polynomial with coefficients cSc_S supported on sets of size at most ℓ\ell, its fourth moment satisfies EP4≤32ℓ(∑ScS2)2\mathbb E P^4\leq 3^{2\ell}(\sum_S c_S^2)^2. Equivalently, for a real function of Fourier degree at most ℓ\ell, EF4≤32ℓ(EF2)2\mathbb E F^4\leq 3^{2\ell}(\mathbb E F^2)^2.

    The proof is a coordinate induction with Cauchy–Schwarz. Its constant is independent of the number of coordinates. This is the fourth-moment case of the hypercontractive estimate used in Lemma 4.13. Multiplication adds Fourier degrees, so iteration gives dyadic moment bounds. Comparing a general power with a higher even power then bounds every moment in terms of degree and second moment, with explicit nonoptimal constants.

    Concept map
    2 concepts; 5 descendants hidden
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 5 statements. Each proof establishes one of them relative to its assumptions.

    1 bounded_moment proven

    2 dyadic_moment proven

    3 fourier_fourth_moment proven

    4 fourth_moment proven

    5 product_degree proven

    Lean source view on GitHub

    1import Lax253009.BooleanFourier
    2import Mathlib.Algebra.BigOperators.Expect
    3
    4/-!
    5---
    6title: Dimension-independent moments of low-degree Boolean polynomials
    7type: theorem
    8---
    9For a Boolean polynomial with coefficients cSc_S supported on sets of size
    10at most ℓ\ell, its fourth moment satisfies
    11EP4≤32ℓ(∑ScS2)2\mathbb E P^4\leq 3^{2\ell}(\sum_S c_S^2)^2.
    12Equivalently, for a real function of Fourier degree at most ℓ\ell,
    13EF4≤32ℓ(EF2)2\mathbb E F^4\leq 3^{2\ell}(\mathbb E F^2)^2.
    14
    15The proof is a coordinate induction with Cauchy–Schwarz. Its constant is
    16independent of the number of coordinates. This is the fourth-moment case
    17of the hypercontractive estimate used in Lemma 4.13. Multiplication adds
    18Fourier degrees, so iteration gives dyadic moment bounds. Comparing a
    19general power with a higher even power then bounds every moment in terms
    20of degree and second moment, with explicit nonoptimal constants.
    21-/
    22
    23namespace Lax253009.Hypercontractivity
    24
    25open BooleanFourier
    26open scoped BigOperators
    27
    28axiom fourth_moment {ι : Type} [Fintype ι] [DecidableEq ι]
    29 (c : Finset ι → ℝ) (l : ℕ) (hdegree : ∀ S, l < S.card → c S = 0) :
    30 (𝔼 x : Cube ι, (∑ S, c S * character S x) ^ 4) ≤
    31 ((3 : ℝ) ^ l * ∑ S, c S ^ 2) ^ 2
    32
    33axiom fourier_fourth_moment {ι : Type} [Fintype ι] [DecidableEq ι]
    34 (F : Cube ι → ℝ) (l : ℕ) (hdegree : ∀ S, l < S.card → coefficient F S = 0) :
    35 (𝔼 x, F x ^ 4) ≤ ((3 : ℝ) ^ l * (𝔼 x, F x ^ 2)) ^ 2
    36
    37axiom product_degree {ι : Type} [Fintype ι] [DecidableEq ι]
    38 (F G : Cube ι → ℝ) (l k : ℕ)
    39 (hF : ∀ S, l < S.card → coefficient F S = 0)
    40 (hG : ∀ S, k < S.card → coefficient G S = 0) :
    41 ∀ S, l + k < S.card → coefficient (fun x ↦ F x * G x) S = 0
    42
    43axiom dyadic_moment {ι : Type} [Fintype ι] [DecidableEq ι]
    44 (F : Cube ι → ℝ) (l k : ℕ) (hdegree : ∀ S, l < S.card → coefficient F S = 0) :
    45 (𝔼 x, F x ^ (2 ^ (k + 1))) ≤
    46 (3 : ℝ) ^ (l * k * 2 ^ k) * (𝔼 x, F x ^ 2) ^ (2 ^ k)
    47
    48axiom bounded_moment {ι : Type} [Fintype ι] [DecidableEq ι]
    49 (F : Cube ι → ℝ) (l m : ℕ) (V : ℝ)
    50 (hdegree : ∀ S, l < S.card → coefficient F S = 0)
    51 (hvariance : (𝔼 x, F x ^ 2) ≤ V) :
    52 (𝔼 x, F x ^ m) ≤ 1 + (3 : ℝ) ^ (l * m * 2 ^ m) * V ^ (2 ^ m)
    53
    54end Lax253009.Hypercontractivity
    55
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…