Lax Lean Archive

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

Walsh operator bounds with explicit bilinear rank

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

    A rectangular bilinear phase factors through its column-image map. Grouping the second weight by the fibers of that map costs at most the kernel cardinality in squared energy. Rank-nullity then gives the exact rank-dependent Walsh estimate, including bounded-density laws and affine phases confined to either input group.

    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 bounded_weight_bound proven

    2 conditional_mixture_bound proven

    3 correlation_sq proven

    4 density_bound proven

    5 separate_phase_bound proven

    6 uniform_bound proven

    Lean source view on GitHub

    1import Lax342547.Walsh
    2
    3/-!
    4---
    5title: Walsh operator bounds with explicit bilinear rank
    6type: lemma
    7---
    8A rectangular bilinear phase factors through its column-image map.
    9Grouping the second weight by the fibers of that map costs at most the
    10kernel cardinality in squared energy. Rank-nullity then gives the exact
    11rank-dependent Walsh estimate, including bounded-density laws and affine
    12phases confined to either input group.
    13-/
    14
    15namespace Lax342547.BilinearWalsh
    16
    17open Lax342547.MomentSpace Lax342547.Walsh
    18
    19noncomputable def correlation {I J : Type} [Fintype I] [Fintype J]
    20 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    21 (f : (I → Binary) → ℝ) (g : (J → Binary) → ℝ) : ℝ :=
    22 ∑ x, ∑ y, f x * g y * phase x (A.mulVec y)
    23
    24noncomputable def average {I J : Type} [Fintype I] [Fintype J]
    25 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    26 (f : (I → Binary) → ℝ) (g : (J → Binary) → ℝ) : ℝ :=
    27 correlation A f g / (2 ^ Fintype.card I * 2 ^ Fintype.card J)
    28
    29axiom correlation_sq {I J : Type} [Fintype I] [Fintype J]
    30 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    31 (f : (I → Binary) → ℝ) (g : (J → Binary) → ℝ) :
    32 (correlation A f g) ^ 2 ≤ (2 : ℝ) ^ (Fintype.card I + (Fintype.card J - A.rank)) *
    33 (∑ x, (f x) ^ 2) * ∑ y, (g y) ^ 2
    34
    35axiom uniform_bound {I J : Type} [Fintype I] [Fintype J]
    36 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    37 (f : (I → Binary) → ℝ) (g : (J → Binary) → ℝ)
    38 (hf : ∀ x, |f x| ≤ 1) (hg : ∀ y, |g y| ≤ 1) :
    39 |average A f g| ≤ 1 / Real.sqrt ((2 : ℝ) ^ A.rank)
    40
    41axiom bounded_weight_bound {I J : Type} [Fintype I] [Fintype J]
    42 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    43 (f : (I → Binary) → ℝ) (g : (J → Binary) → ℝ) (C₁ C₂ : ℝ)
    44 (hC₁ : 0 ≤ C₁) (hC₂ : 0 ≤ C₂) (hf : ∀ x, |f x| ≤ C₁) (hg : ∀ y, |g y| ≤ C₂) :
    45 |average A f g| ≤ C₁ * C₂ / Real.sqrt ((2 : ℝ) ^ A.rank)
    46
    47axiom density_bound {I J : Type} [Fintype I] [Fintype J]
    48 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    49 (α f : (I → Binary) → ℝ) (β g : (J → Binary) → ℝ) (C₁ C₂ : ℝ)
    50 (hα : ∀ x, 0 ≤ α x ∧ α x ≤ C₁) (hβ : ∀ y, 0 ≤ β y ∧ β y ≤ C₂)
    51 (hf : ∀ x, |f x| ≤ 1) (hg : ∀ y, |g y| ≤ 1) :
    52 |average A (fun x => α x * f x) (fun y => β y * g y)| ≤
    53 C₁ * C₂ / Real.sqrt ((2 : ℝ) ^ A.rank)
    54
    55axiom separate_phase_bound {I J : Type} [Fintype I] [Fintype J]
    56 [DecidableEq I] [DecidableEq J] (A : Matrix I J Binary)
    57 (f : (I → Binary) → ℝ) (g : (J → Binary) → ℝ)
    58 (u : (I → Binary) → Binary) (v : (J → Binary) → Binary) (c : Binary)
    59 (hf : ∀ x, |f x| ≤ 1) (hg : ∀ y, |g y| ≤ 1) :
    60 |(∑ x, ∑ y, f x * g y * sign (dotProduct x (A.mulVec y) + u x + v y + c)) /
    61 ((2 : ℝ) ^ Fintype.card I * 2 ^ Fintype.card J)| ≤ 1 / Real.sqrt ((2 : ℝ) ^ A.rank)
    62
    63axiom conditional_mixture_bound {T : Type} [Fintype T] {I J : T → Type}
    64 [∀ t, Fintype (I t)] [∀ t, Fintype (J t)]
    65 [∀ t, DecidableEq (I t)] [∀ t, DecidableEq (J t)]
    66 (A : ∀ t, Matrix (I t) (J t) Binary)
    67 (f : ∀ t, (I t → Binary) → ℝ) (g : ∀ t, (J t → Binary) → ℝ)
    68 (w C₁ C₂ : T → ℝ) (R : ℕ) (hw : ∀ t, 0 ≤ w t)
    69 (hC₁ : ∀ t, 0 ≤ C₁ t) (hC₂ : ∀ t, 0 ≤ C₂ t)
    70 (hf : ∀ t x, |f t x| ≤ C₁ t) (hg : ∀ t y, |g t y| ≤ C₂ t)
    71 (hR : ∀ t, R ≤ (A t).rank) :
    72 |∑ t, w t * average (A t) (f t) (g t)| ≤
    73 (∑ t, w t * C₁ t * C₂ t) / Real.sqrt ((2 : ℝ) ^ R)
    74
    75end Lax342547.BilinearWalsh
    76
    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…