Lax Lean Archive

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

Fourier shifts, odd tables and disagreement indicators

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

    Multiplication by the character of TT shifts Fourier indices by symmetric difference with TT. If F(−x)=−F(x)F(-x)=-F(x), all coefficients on even supports vanish, as observed after equation (1) of Håstad's paper.

    For a Boolean table AA and a coordinate yy, the indicator that A(x)A(x) disagrees with the point evaluation xyx_y is Iy(x)=(1−sign⁡(A(x))sign⁡(xy))/2I_y(x)=(1-\operatorname{sign}(A(x))\operatorname{sign}(x_y))/2. Its coefficient on SS is 121S=∅−12A^(S△{y})\tfrac12\mathbf1_{S=\varnothing}-\tfrac12\widehat A(S\mathbin\triangle\{y\}). This combines equations (4) and (5) in Section 4.1.

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

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

    1 character_shift proven

    2 disagreement_coefficient proven

    3 disagreement_indicator proven

    4 odd_even_vanish proven

    Lean source view on GitHub

    1import Lax253009.BooleanFourier
    2import Mathlib.Data.Finset.SymmDiff
    3import Mathlib.Algebra.Ring.Parity
    4
    5/-!
    6---
    7title: Fourier shifts, odd tables and disagreement indicators
    8type: theorem
    9---
    10Multiplication by the character of TT shifts Fourier indices by symmetric
    11difference with TT. If F(−x)=−F(x)F(-x)=-F(x), all coefficients on even supports
    12vanish, as observed after equation (1) of Håstad's paper.
    13
    14For a Boolean table AA and a coordinate yy, the indicator that A(x)A(x)
    15disagrees with the point evaluation xyx_y is
    16Iy(x)=(1−sign⁡(A(x))sign⁡(xy))/2I_y(x)=(1-\operatorname{sign}(A(x))\operatorname{sign}(x_y))/2.
    17Its coefficient on SS is
    18121S=∅−12A^(S△{y})\tfrac12\mathbf1_{S=\varnothing}-\tfrac12\widehat A(S\mathbin\triangle\{y\}).
    19This combines equations (4) and (5) in Section 4.1.
    20-/
    21
    22namespace Lax253009.FourierIdentities
    23
    24open BooleanFourier
    25open scoped symmDiff
    26
    27def bitFlip {ι : Type} (x : Cube ι) : Cube ι := fun i ↦ !(x i)
    28
    29noncomputable def disagreement {ι : Type} (A : Cube ι → Bool) (y : ι)
    30 (x : Cube ι) : ℝ :=
    31 (1 - sign (A x) * sign (x y)) / 2
    32
    33axiom character_shift {ι : Type} [Fintype ι] [DecidableEq ι]
    34 (F : Cube ι → ℝ) (S T : Finset ι) :
    35 coefficient (fun x ↦ F x * character T x) S = coefficient F (S ∆ T)
    36
    37axiom odd_even_vanish {ι : Type} [Fintype ι] [DecidableEq ι]
    38 (F : Cube ι → ℝ) (hF : ∀ x, F (bitFlip x) = -F x)
    39 (S : Finset ι) (hS : Even S.card) : coefficient F S = 0
    40
    41axiom disagreement_indicator {ι : Type} (A : Cube ι → Bool) (y : ι) (x : Cube ι) :
    42 disagreement A y x = if A x = x y then 0 else 1
    43
    44axiom disagreement_coefficient {ι : Type} [Fintype ι] [DecidableEq ι]
    45 (A : Cube ι → Bool) (y : ι) (S : Finset ι) :
    46 coefficient (disagreement A y) S =
    47 ((if S = ∅ then 1 else 0) - coefficient (fun x ↦ sign (A x)) (S ∆ {y})) / 2
    48
    49end Lax253009.FourierIdentities
    50
    Show ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

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

    Loading discussion…