Lax Lean Archive

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

Actual raw frame observations with uniform two-batch decay

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

    Independent combined coefficient columns give a comparison for arbitrary separate bounded tests under the actual raw frame law, or under the full self-channel Gram fiber law. The explicit threshold and error constants depend only on the four fixed column counts and not on their Gram entries.

    Concept map
    22 concepts; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 errorBound_half_decay proven

    2 eventually_valid proven

    3 full_test_comparison proven

    4 primal_test_comparison proven

    Lean source view on GitHub

    1import Lax342547.RawBatchComparison
    2
    3/-!
    4---
    5title: Actual raw frame observations with uniform two-batch decay
    6type: lemma
    7---
    8Independent combined coefficient columns give a comparison for arbitrary
    9separate bounded tests under the actual raw frame law, or under the full
    10self-channel Gram fiber law. The explicit threshold and error constants
    11depend only on the four fixed column counts and not on their Gram entries.
    12-/
    13
    14namespace Lax342547.RawFrameComparison
    15noncomputable section
    16open Lax342547.MomentSpace Lax342547.FrameTuples Lax342547.RealCellLaws
    17open Lax342547.GramOrbitDensity Lax342547.RawFrames
    18open scoped BigOperators
    19
    20def errorBound (n : ℕ) (I J K L : Type) [Fintype I] [Fintype J] [Fintype K] [Fintype L] : ℝ :=
    21 (2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+2)*
    22 ((((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    23 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))/Real.sqrt ((2 : ℝ)^n))+
    24 (((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    25 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))*
    26 (((2 : ℝ)^(Fintype.card I+Fintype.card K)+(2 : ℝ)^(Fintype.card J+Fintype.card L))/(2 : ℝ)^n)))
    27
    28def scale (I J K L : Type) [Fintype I] [Fintype J] [Fintype K] [Fintype L] : ℝ :=
    29 (2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+2)*
    30 ((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    31 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))*
    32 (1+((2 : ℝ)^(Fintype.card I+Fintype.card K)+(2 : ℝ)^(Fintype.card J+Fintype.card L)))
    33
    34axiom errorBound_half_decay (n : ℕ) (I J K L : Type)
    35 [Fintype I] [Fintype J] [Fintype K] [Fintype L] :
    36 errorBound n I J K L ≤ scale I J K L/Real.sqrt ((2 : ℝ)^n)
    37
    38axiom eventually_valid (I J K L : Type) [Fintype I] [Fintype J] [Fintype K] [Fintype L] :
    39 ∃ n₀ : ℕ,∀ n ≥ n₀,Fintype.card I+Fintype.card J+1 ≤ n ∧
    40 Fintype.card K+Fintype.card L+1 ≤ n ∧
    41 ((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    42 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))/Real.sqrt ((2 : ℝ)^n) ≤
    43 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+1)
    44
    45variable {I J K L : Type} [Fintype I] [Fintype J] [Fintype K] [Fintype L]
    46variable {B H : Type} [Fintype B] [Fintype H]
    47
    48axiom primal_test_comparison [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] (n : ℕ) (E : Matrix B B Binary)
    49 [Nonempty (Frame B H (Fin n) E)]
    50 (C₁ : Matrix B I Binary) (D₁ : Matrix B J Binary)
    51 (C₂ : Matrix B K Binary) (D₂ : Matrix B L Binary)
    52 (hC : Function.Injective (Matrix.fromCols C₁ C₂).mulVec)
    53 (hD : Function.Injective (Matrix.fromCols D₁ D₂).mulVec)
    54 (f : (Fin n × (I ⊕ J) → Binary) → ℝ) (g : (Fin n × (K ⊕ L) → Binary) → ℝ)
    55 (hN₁ : Fintype.card I+Fintype.card J+1 ≤ n)
    56 (hN₂ : Fintype.card K+Fintype.card L+1 ≤ n)
    57 (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1)
    58 (hsmall : ((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    59 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))/Real.sqrt ((2 : ℝ)^n) ≤
    60 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+1)) :
    61 |(∑ F : Frame B H (Fin n) E,weights (PMF.uniformOfFintype _) F*
    62 (f (batchEquiv (F.P*C₁,F.Q*D₁))*g (batchEquiv (F.P*C₂,F.Q*D₂))))-
    63 (∑ F : Frame B H (Fin n) E,weights (PMF.uniformOfFintype _) F*f (batchEquiv (F.P*C₁,F.Q*D₁)))*
    64 (∑ F : Frame B H (Fin n) E,weights (PMF.uniformOfFintype _) F*g (batchEquiv (F.P*C₂,F.Q*D₂)))| ≤
    65 errorBound n I J K L
    66
    67axiom full_test_comparison [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] (n : ℕ) (E : Matrix B B Binary) (S : Matrix H H Binary)
    68 [Nonempty (ChannelFiber (N := Fin n) E S)]
    69 (C₁ : Matrix (B ⊕ H) I Binary) (D₁ : Matrix (B ⊕ H) J Binary)
    70 (C₂ : Matrix (B ⊕ H) K Binary) (D₂ : Matrix (B ⊕ H) L Binary)
    71 (hC : Function.Injective (Matrix.fromCols C₁ C₂).mulVec)
    72 (hD : Function.Injective (Matrix.fromCols D₁ D₂).mulVec)
    73 (f : (Fin n × (I ⊕ J) → Binary) → ℝ) (g : (Fin n × (K ⊕ L) → Binary) → ℝ)
    74 (hN₁ : Fintype.card I+Fintype.card J+1 ≤ n)
    75 (hN₂ : Fintype.card K+Fintype.card L+1 ≤ n)
    76 (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1)
    77 (hsmall : ((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    78 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))/Real.sqrt ((2 : ℝ)^n) ≤
    79 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+1)) :
    80 |(∑ F : ChannelFiber (N := Fin n) E S,weights (PMF.uniformOfFintype _) F*
    81 (f (batchEquiv ((Lax342547.FrameSymmetry.plus F.val).val*C₁,(Lax342547.FrameSymmetry.minus F.val).val*D₁))*g (batchEquiv ((Lax342547.FrameSymmetry.plus F.val).val*C₂,(Lax342547.FrameSymmetry.minus F.val).val*D₂))))-
    82 (∑ F : ChannelFiber (N := Fin n) E S,weights (PMF.uniformOfFintype _) F*f (batchEquiv ((Lax342547.FrameSymmetry.plus F.val).val*C₁,(Lax342547.FrameSymmetry.minus F.val).val*D₁)))*
    83 (∑ F : ChannelFiber (N := Fin n) E S,weights (PMF.uniformOfFintype _) F*g (batchEquiv ((Lax342547.FrameSymmetry.plus F.val).val*C₂,(Lax342547.FrameSymmetry.minus F.val).val*D₂)))| ≤
    84 errorBound n I J K L
    85
    86end
    87end Lax342547.RawFrameComparison
    88
    Show 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…