Lax Lean Archive

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

Fourier analysis on a finite Boolean cube

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

    Write a Boolean value as a sign, with true represented by −1-1 and false by 11. For a subset SS of a finite coordinate set II, the character χS(x)\chi_S(x) is the product of the signs of xix_i over i∈Si\in S. For a real function FF on the cube, set F^(S)=2−∣I∣∑xF(x)χS(x)\widehat F(S)=2^{-|I|}\sum_x F(x)\chi_S(x).

    The characters are orthonormal for the uniform average. Fourier inversion recovers F(x)=∑SF^(S)χS(x)F(x)=\sum_S\widehat F(S)\chi_S(x), and Parseval's identity gives ∑SF^(S)2=ExF(x)2\sum_S\widehat F(S)^2=\mathbb E_x F(x)^2. In particular, a sign-valued function has total squared Fourier mass one. These are the Fourier identities used at the start of Section 4 of Håstad's paper.

    Concept map
    1 concept; 18 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 boolean_energy proven

    2 bounded_energy proven

    3 inversion proven

    4 orthogonality proven

    5 parseval proven

    Lean source view on GitHub

    1import Mathlib.Data.Real.Basic
    2import Mathlib.Data.Fintype.Powerset
    3import Mathlib.Data.Fintype.Pi
    4import Mathlib.Algebra.BigOperators.Ring.Finset
    5
    6/-!
    7---
    8title: Fourier analysis on a finite Boolean cube
    9type: theorem
    10---
    11Write a Boolean value as a sign, with true represented by −1-1 and false
    12by 11. For a subset SS of a finite coordinate set II, the character
    13χS(x)\chi_S(x) is the product of the signs of xix_i over i∈Si\in S.
    14For a real function FF on the cube, set
    15F^(S)=2−∣I∣∑xF(x)χS(x)\widehat F(S)=2^{-|I|}\sum_x F(x)\chi_S(x).
    16
    17The characters are orthonormal for the uniform average. Fourier inversion
    18recovers F(x)=∑SF^(S)χS(x)F(x)=\sum_S\widehat F(S)\chi_S(x), and Parseval's identity gives
    19∑SF^(S)2=ExF(x)2\sum_S\widehat F(S)^2=\mathbb E_x F(x)^2. In particular, a sign-valued
    20function has total squared Fourier mass one. These are the Fourier
    21identities used at the start of Section 4 of Håstad's paper.
    22-/
    23
    24namespace Lax253009.BooleanFourier
    25
    26abbrev Cube (ι : Type) := ι → Bool
    27
    28def sign (b : Bool) : ℝ := if b then -1 else 1
    29
    30noncomputable def character {ι : Type} (S : Finset ι) (x : Cube ι) : ℝ :=
    31 ∏ i ∈ S, sign (x i)
    32
    33noncomputable def average {ι : Type} [Fintype ι] [DecidableEq ι] (F : Cube ι → ℝ) : ℝ :=
    34 (∑ x, F x) / (2 : ℝ) ^ Fintype.card ι
    35
    36noncomputable def coefficient {ι : Type} [Fintype ι] [DecidableEq ι] (F : Cube ι → ℝ)
    37 (S : Finset ι) : ℝ :=
    38 average fun x ↦ F x * character S x
    39
    40axiom orthogonality {ι : Type} [Fintype ι] [DecidableEq ι] (S T : Finset ι) :
    41 average (fun x ↦ character S x * character T x) = if S = T then 1 else 0
    42
    43axiom inversion {ι : Type} [Fintype ι] [DecidableEq ι] (F : Cube ι → ℝ) (x : Cube ι) :
    44 F x = ∑ S, coefficient F S * character S x
    45
    46axiom parseval {ι : Type} [Fintype ι] [DecidableEq ι] (F : Cube ι → ℝ) :
    47 ∑ S, coefficient F S ^ 2 = average (fun x ↦ F x ^ 2)
    48
    49axiom boolean_energy {ι : Type} [Fintype ι] [DecidableEq ι] (A : Cube ι → Bool) :
    50 ∑ S, coefficient (fun x ↦ sign (A x)) S ^ 2 = 1
    51
    52axiom bounded_energy {ι : Type} [Fintype ι] [DecidableEq ι]
    53 (F : Cube ι → ℝ) (hF : ∀ x, |F x| ≤ 1) :
    54 ∑ S, coefficient F S ^ 2 ≤ 1
    55
    56end Lax253009.BooleanFourier
    57
    Show ProofShow ProofShow ProofShow ProofShow Proof
    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…