Lax Lean Archive

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

Orthogonality and finite Walsh correlation bounds

Lax342547.Walsh · concepts/Lax342547/Walsh.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

    The real binary character is 1 on zero and -1 on one. Its dot-product matrix has orthogonal rows. The resulting exact squared operator bound controls correlations of bounded weights and subprobability masses.

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

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

    1 dot_correlation_sq proven

    2 linear_orthogonality proven

    3 orthogonality proven

    4 subprobability_dot_bound proven

    5 transform_energy proven

    Lean source view on GitHub

    1import Lax342547.MomentSpace
    2import Mathlib.Analysis.SpecialFunctions.Sqrt
    3import Mathlib.LinearAlgebra.Matrix.Rank
    4
    5/-!
    6---
    7title: Orthogonality and finite Walsh correlation bounds
    8type: lemma
    9---
    10The real binary character is 1 on zero and -1 on one. Its dot-product
    11matrix has orthogonal rows. The resulting exact squared operator bound
    12controls correlations of bounded weights and subprobability masses.
    13-/
    14
    15namespace Lax342547.Walsh
    16
    17open Lax342547.MomentSpace
    18
    19noncomputable def sign (z : Binary) : ℝ := if z = 0 then 1 else -1
    20
    21noncomputable def phase {I : Type} [Fintype I] (x y : I → Binary) : ℝ :=
    22 sign (dotProduct x y)
    23
    24noncomputable def transform {I : Type} [Fintype I] [DecidableEq I]
    25 (f : (I → Binary) → ℝ) (x : I → Binary) : ℝ := ∑ y, phase x y * f y
    26
    27axiom linear_orthogonality {V : Type} [AddCommGroup V] [Module Binary V] [Fintype V]
    28 (f : V →ₗ[Binary] Binary) (hf : f ≠ 0) : ∑ x, sign (f x) = 0
    29
    30axiom orthogonality {I : Type} [Fintype I] [DecidableEq I]
    31 (x z : I → Binary) :
    32 ∑ y, phase x y * phase z y = if x = z then (2 : ℝ) ^ Fintype.card I else 0
    33
    34axiom transform_energy {I : Type} [Fintype I] [DecidableEq I]
    35 (f : (I → Binary) → ℝ) :
    36 ∑ x, (transform f x) ^ 2 = (2 : ℝ) ^ Fintype.card I * ∑ y, (f y) ^ 2
    37
    38axiom dot_correlation_sq {I : Type} [Fintype I] [DecidableEq I]
    39 (f g : (I → Binary) → ℝ) :
    40 (∑ x, ∑ y, f x * g y * phase x y) ^ 2 ≤
    41 (2 : ℝ) ^ Fintype.card I * (∑ x, (f x) ^ 2) * ∑ y, (g y) ^ 2
    42
    43axiom subprobability_dot_bound {I : Type} [Fintype I] [DecidableEq I]
    44 (α β f g : (I → Binary) → ℝ) (p₁ p₂ : ℝ)
    45 (hα : ∀ x, 0 ≤ α x ∧ α x ≤ p₁) (hβ : ∀ y, 0 ≤ β y ∧ β y ≤ p₂)
    46 (hαsum : ∑ x, α x ≤ 1) (hβsum : ∑ y, β y ≤ 1)
    47 (hf : ∀ x, |f x| ≤ 1) (hg : ∀ y, |g y| ≤ 1) :
    48 |∑ x, ∑ y, α x * β y * f x * g y * phase x y| ≤
    49 Real.sqrt ((2 : ℝ) ^ Fintype.card I * p₁ * p₂)
    50
    51end Lax342547.Walsh
    52
    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…