Lax Lean Archive

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

Finite scalar agreement from binary character bounds

Lax342547.FourierTests · concepts/Lax342547/FourierTests.lean · lax-342547

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

    Lemma

    Exact Fourier inversion yields simultaneous agreement of all scalar bits without any independence assumption on those bits.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

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

    1 character_zero proven

    2 four_bit_pattern proven

    3 pattern_inversion proven

    4 pattern_lower proven

    5 pattern_lower_sharp proven

    6 scalar_agreement_half proven

    Lean source view on GitHub

    1import Lax342547.Walsh
    2
    3/-!
    4---
    5title: Finite scalar agreement from binary character bounds
    6type: lemma
    7---
    8Exact Fourier inversion yields simultaneous agreement of all scalar bits without any independence assumption on those bits.
    9-/
    10
    11namespace Lax342547.FourierTests
    12
    13open Lax342547.MomentSpace Lax342547.Walsh
    14
    15noncomputable def patternMass {Ω I : Type} [Fintype Ω] [Fintype I]
    16 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target : I → Binary) : ℝ := by
    17 classical
    18 exact ∑ ω, if bits ω = target then ρ ω else 0
    19
    20noncomputable def characterMean {Ω I : Type} [Fintype Ω] [Fintype I]
    21 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target t : I → Binary) : ℝ :=
    22 ∑ ω, ρ ω * phase t (bits ω) * phase t target
    23
    24axiom character_zero {Ω I : Type} [Fintype Ω] [Fintype I]
    25 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target : I → Binary) :
    26 characterMean ρ bits target 0 = ∑ ω, ρ ω
    27
    28axiom pattern_inversion {Ω I : Type} [Fintype Ω] [Fintype I] [DecidableEq I]
    29 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target : I → Binary) :
    30 (∑ t : I → Binary, characterMean ρ bits target t) =
    31 (2 : ℝ) ^ Fintype.card I * patternMass ρ bits target
    32
    33axiom pattern_lower {Ω I : Type} [Fintype Ω] [Fintype I] [DecidableEq I]
    34 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target : I → Binary) (ε : ℝ)
    35 (hε : 0 ≤ ε) (hρ : ∑ ω, ρ ω = 1)
    36 (hchar : ∀ t : I → Binary, t ≠ 0 → -ε ≤ characterMean ρ bits target t) :
    37 1 / (2 : ℝ) ^ Fintype.card I - ε ≤ patternMass ρ bits target
    38
    39axiom pattern_lower_sharp {Ω I : Type} [Fintype Ω] [Fintype I] [DecidableEq I]
    40 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target : I → Binary) (ε : ℝ)
    41 (hρ : ∑ ω, ρ ω = 1)
    42 (hchar : ∀ t : I → Binary, t ≠ 0 → -ε ≤ characterMean ρ bits target t) :
    43 (1 - ((2 : ℝ) ^ Fintype.card I - 1) * ε) / (2 : ℝ) ^ Fintype.card I ≤
    44 patternMass ρ bits target
    45
    46axiom four_bit_pattern {Ω : Type} [Fintype Ω]
    47 (ρ : Ω → ℝ) (bits : Ω → Fin 4 → Lax342547.MomentSpace.Binary)
    48 (target : Fin 4 → Lax342547.MomentSpace.Binary) (hρ : ∑ ω, ρ ω = 1)
    49 (hchar : ∀ t : Fin 4 → Lax342547.MomentSpace.Binary, t ≠ 0 →
    50 |characterMean ρ bits target t| ≤ 1 / 200) :
    51 (37 : ℝ) / 640 ≤ patternMass ρ bits target
    52
    53axiom scalar_agreement_half {Ω I : Type} [Fintype Ω] [Fintype I] [DecidableEq I]
    54 (ρ : Ω → ℝ) (bits : Ω → I → Binary) (target : I → Binary) (ε : ℝ)
    55 (hε : 0 ≤ ε) (hρ : ∑ ω, ρ ω = 1)
    56 (hchar : ∀ t : I → Binary, t ≠ 0 → -ε ≤ characterMean ρ bits target t)
    57 (hsmall : ε ≤ 1 / (2 : ℝ) ^ (Fintype.card I + 1)) :
    58 1 / (2 : ℝ) ^ (Fintype.card I + 1) ≤ patternMass ρ bits target
    59
    60end Lax342547.FourierTests
    61
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…