Lax Lean Archive

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

Even-cover expansion of a Boolean polynomial moment

Lax253009.EvenCovers · concepts/Lax253009/EvenCovers.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

    A family of supports is an even cover if every coordinate occurs an even number of times. The uniform mean of the product of its Boolean characters is one for an even cover and zero otherwise. Consequently the mmth moment of a Boolean polynomial is the sum of the coefficient products over its even-cover tuples.

    This is the moment identity in the proof of Lemma 4.13, before application of the hypercontractive inequality. The coefficients may be arbitrary real numbers; choosing absolute Fourier coefficients gives the nonnegative weighted sum used in the paper. Every even cover is a double cover of its union.

    Concept map
    4 concepts
    100%
    Proven claimThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 character_moment proven

    2 even_implies_double proven

    3 polynomial_moment proven

    Lean source view on GitHub

    1import Lax253009.BooleanFourier
    2import Lax253009.HigherMoments
    3
    4/-!
    5---
    6title: Even-cover expansion of a Boolean polynomial moment
    7type: theorem
    8---
    9A family of supports is an even cover if every coordinate occurs an even
    10number of times. The uniform mean of the product of its Boolean characters
    11is one for an even cover and zero otherwise. Consequently the mmth moment
    12of a Boolean polynomial is the sum of the coefficient products over its
    13even-cover tuples.
    14
    15This is the moment identity in the proof of Lemma 4.13, before application
    16of the hypercontractive inequality. The coefficients may be arbitrary real
    17numbers; choosing absolute Fourier coefficients gives the nonnegative
    18weighted sum used in the paper. Every even cover is a double cover of its
    19union.
    20-/
    21
    22namespace Lax253009.EvenCovers
    23
    24open BooleanFourier HigherMoments
    25open scoped BigOperators
    26
    27def EvenCover {ι : Type} [DecidableEq ι] {m : ℕ} (S : Fin m → Finset ι) : Prop :=
    28 ∀ i, Even (Finset.univ.filter fun j ↦ i ∈ S j).card
    29
    30instance decidableEvenCover {ι : Type} [Fintype ι] [DecidableEq ι]
    31 {m : ℕ} (S : Fin m → Finset ι) : Decidable (EvenCover S) :=
    32 inferInstanceAs (Decidable (∀ i, Even (Finset.univ.filter fun j ↦ i ∈ S j).card))
    33
    34axiom character_moment {ι : Type} [Fintype ι] [DecidableEq ι]
    35 {m : ℕ} (S : Fin m → Finset ι) :
    36 (𝔼 x : Cube ι, ∏ j, character (S j) x) =
    37 if EvenCover S then 1 else 0
    38
    39axiom polynomial_moment {ι α : Type} [Fintype ι] [DecidableEq ι]
    40 [Fintype α] (S : α → Finset ι) (c : α → ℝ) (m : ℕ) :
    41 (𝔼 x : Cube ι, (∑ a, c a * character (S a) x) ^ m) =
    42 ∑ a : Fin m → α, if EvenCover (fun j ↦ S (a j)) then ∏ j, c (a j) else 0
    43
    44axiom even_implies_double {ι : Type} [DecidableEq ι] {m : ℕ}
    45 (S : Fin m → Finset ι) (hS : EvenCover S) : DoubleCover S
    46
    47end Lax253009.EvenCovers
    48
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…