Lax Lean Archive

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

Walsh bounds for independent image laws and separated phases

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

    Image pushforwards and conditional bounded weights translate the finite Walsh bound to arbitrary orientation laws, preserving separate phases from frozen vectors.

    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 7 statements. Each proof establishes one of them relative to its assumptions.

    1 conditional_weight_bound proven

    2 conditional_weight_reconstruction proven

    3 image_walsh_bound proven

    4 push_integral proven

    5 push_nonneg proven

    6 push_total proven

    7 signed_push_bound proven

    Lean source view on GitHub

    1import Lax342547.Walsh
    2
    3/-!
    4---
    5title: Walsh bounds for independent image laws and separated phases
    6type: lemma
    7---
    8Image pushforwards and conditional bounded weights translate the finite Walsh bound to arbitrary orientation laws, preserving separate phases from frozen vectors.
    9-/
    10
    11namespace Lax342547.PushforwardWalsh
    12
    13open Lax342547.MomentSpace Lax342547.Walsh
    14
    15noncomputable def push {Ω X : Type} [Fintype Ω] (ρ : Ω → ℝ) (image : Ω → X) (x : X) : ℝ := by
    16 classical
    17 exact ∑ ω, if image ω = x then ρ ω else 0
    18
    19axiom push_nonneg {Ω X : Type} [Fintype Ω] (ρ : Ω → ℝ) (image : Ω → X)
    20 (hρ : ∀ ω, 0 ≤ ρ ω) (x : X) : 0 ≤ push ρ image x
    21
    22axiom push_total {Ω X : Type} [Fintype Ω] [Fintype X] (ρ : Ω → ℝ) (image : Ω → X) :
    23 ∑ x, push ρ image x = ∑ ω, ρ ω
    24
    25axiom push_integral {Ω X : Type} [Fintype Ω] [Fintype X]
    26 (ρ : Ω → ℝ) (image : Ω → X) (f : X → ℝ) :
    27 ∑ x, push ρ image x * f x = ∑ ω, ρ ω * f (image ω)
    28
    29axiom signed_push_bound {Ω X : Type} [Fintype Ω] (ρ w : Ω → ℝ) (image : Ω → X)
    30 (hρ : ∀ ω, 0 ≤ ρ ω) (hw : ∀ ω, |w ω| ≤ 1) (x : X) :
    31 |push (fun ω => ρ ω * w ω) image x| ≤ push ρ image x
    32
    33noncomputable def conditionalWeight {Ω X : Type} [Fintype Ω]
    34 (ρ w : Ω → ℝ) (image : Ω → X) (x : X) : ℝ :=
    35 push (fun ω => ρ ω * w ω) image x / push ρ image x
    36
    37axiom conditional_weight_bound {Ω X : Type} [Fintype Ω]
    38 (ρ w : Ω → ℝ) (image : Ω → X) (hρ : ∀ ω, 0 ≤ ρ ω)
    39 (hw : ∀ ω, |w ω| ≤ 1) (x : X) : |conditionalWeight ρ w image x| ≤ 1
    40
    41axiom conditional_weight_reconstruction {Ω X : Type} [Fintype Ω]
    42 (ρ w : Ω → ℝ) (image : Ω → X) (hρ : ∀ ω, 0 ≤ ρ ω)
    43 (hw : ∀ ω, |w ω| ≤ 1) (x : X) :
    44 push ρ image x * conditionalWeight ρ w image x =
    45 push (fun ω => ρ ω * w ω) image x
    46
    47axiom image_walsh_bound {ΩA ΩB I : Type} [Fintype ΩA] [Fintype ΩB]
    48 [Fintype I] [DecidableEq I]
    49 (α : ΩA → ℝ) (β : ΩB → ℝ) (imageA : ΩA → I → Binary) (imageB : ΩB → I → Binary)
    50 (f : ΩA → ℝ) (g : ΩB → ℝ) (pA pB : ℝ)
    51 (hα : ∀ a, 0 ≤ α a) (hβ : ∀ b, 0 ≤ β b)
    52 (hαsum : ∑ a, α a ≤ 1) (hβsum : ∑ b, β b ≤ 1)
    53 (hcapA : ∀ x, push α imageA x ≤ pA) (hcapB : ∀ y, push β imageB y ≤ pB)
    54 (hf : ∀ a, |f a| ≤ 1) (hg : ∀ b, |g b| ≤ 1) :
    55 |∑ a, ∑ b, α a * β b * f a * g b * phase (imageA a) (imageB b)| ≤
    56 Real.sqrt ((2 : ℝ) ^ Fintype.card I * pA * pB)
    57
    58end Lax342547.PushforwardWalsh
    59
    Show ProofShow 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…