Lax Lean Archive

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

Actual grouped raw observations with arbitrary common tests

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

    Theorem

    Nominal joint independence is checked separately in every component and sign. Independent raw frame groups then compare arbitrary common tests of the separate observed arrays, with the sum of their explicit two-batch errors. Both Gram matrices and column dimensions may vary by group.

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

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

    1 full_groups proven

    2 primal_groups proven

    Lean source view on GitHub

    1import Lax342547.GroupTensorComparison
    2
    3/-!
    4---
    5title: Actual grouped raw observations with arbitrary common tests
    6type: theorem
    7---
    8Nominal joint independence is checked separately in every component and
    9sign. Independent raw frame groups then compare arbitrary common tests of
    10the separate observed arrays, with the sum of their explicit two-batch
    11errors. Both Gram matrices and column dimensions may vary by group.
    12-/
    13
    14namespace Lax342547.RawGroupedComparison
    15noncomputable section
    16open Lax342547.MomentSpace Lax342547.RawFrames Lax342547.GramOrbitDensity
    17open Lax342547.FrameTuples Lax342547.RealCellLaws Lax342547.RawFrameComparison
    18open scoped BigOperators
    19
    20variable {S B H : Type} [Fintype S] [DecidableEq S] [Fintype B] [Fintype H]
    21 {I J K L : S → Type} [∀ s,Fintype (I s)] [∀ s,Fintype (J s)]
    22 [∀ s,Fintype (K s)] [∀ s,Fintype (L s)]
    23
    24axiom primal_groups [∀ s,DecidableEq (I s)] [∀ s,DecidableEq (J s)]
    25 [∀ s,DecidableEq (K s)] [∀ s,DecidableEq (L s)] (n : ℕ) (E : S → Matrix B B Binary)
    26 [∀ s,Nonempty (Frame B H (Fin n) (E s))]
    27 (C₁ : ∀ s,Matrix B (I s) Binary) (D₁ : ∀ s,Matrix B (J s) Binary)
    28 (C₂ : ∀ s,Matrix B (K s) Binary) (D₂ : ∀ s,Matrix B (L s) Binary)
    29 (hC : ∀ s,Function.Injective (Matrix.fromCols (C₁ s) (C₂ s)).mulVec)
    30 (hD : ∀ s,Function.Injective (Matrix.fromCols (D₁ s) (D₂ s)).mulVec)
    31 (f : (∀ s,Fin n × (I s ⊕ J s) → Binary) → ℝ)
    32 (g : (∀ s,Fin n × (K s ⊕ L s) → Binary) → ℝ)
    33 (hN₁ : ∀ s,Fintype.card (I s)+Fintype.card (J s)+1 ≤ n)
    34 (hN₂ : ∀ s,Fintype.card (K s)+Fintype.card (L s)+1 ≤ n)
    35 (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1)
    36 (hsmall : ∀ s,((2 : ℝ)^(Fintype.card (I s)*Fintype.card (J s)+2))*
    37 ((2 : ℝ)^(Fintype.card (K s)*Fintype.card (L s)+2))/Real.sqrt ((2 : ℝ)^n) ≤
    38 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots (I s) (J s) (K s) (L s))+1)) :
    39 |(∑ o : ∀ s,Frame B H (Fin n) (E s),weights (PMF.uniformOfFintype _) o*
    40 (f (fun s => batchEquiv ((o s).P*C₁ s,(o s).Q*D₁ s))*
    41 g (fun s => batchEquiv ((o s).P*C₂ s,(o s).Q*D₂ s))))-
    42 (∑ o : ∀ s,Frame B H (Fin n) (E s),weights (PMF.uniformOfFintype _) o*
    43 f (fun s => batchEquiv ((o s).P*C₁ s,(o s).Q*D₁ s)))*
    44 (∑ o : ∀ s,Frame B H (Fin n) (E s),weights (PMF.uniformOfFintype _) o*
    45 g (fun s => batchEquiv ((o s).P*C₂ s,(o s).Q*D₂ s)))| ≤
    46 ∑ s,errorBound n (I s) (J s) (K s) (L s)
    47
    48axiom full_groups [∀ s,DecidableEq (I s)] [∀ s,DecidableEq (J s)]
    49 [∀ s,DecidableEq (K s)] [∀ s,DecidableEq (L s)] (n : ℕ) (E : S → Matrix B B Binary) (T : S → Matrix H H Binary)
    50 [∀ s,Nonempty (ChannelFiber (N := Fin n) (E s) (T s))]
    51 (C₁ : ∀ s,Matrix (B ⊕ H) (I s) Binary) (D₁ : ∀ s,Matrix (B ⊕ H) (J s) Binary)
    52 (C₂ : ∀ s,Matrix (B ⊕ H) (K s) Binary) (D₂ : ∀ s,Matrix (B ⊕ H) (L s) Binary)
    53 (hC : ∀ s,Function.Injective (Matrix.fromCols (C₁ s) (C₂ s)).mulVec)
    54 (hD : ∀ s,Function.Injective (Matrix.fromCols (D₁ s) (D₂ s)).mulVec)
    55 (f : (∀ s,Fin n × (I s ⊕ J s) → Binary) → ℝ)
    56 (g : (∀ s,Fin n × (K s ⊕ L s) → Binary) → ℝ)
    57 (hN₁ : ∀ s,Fintype.card (I s)+Fintype.card (J s)+1 ≤ n)
    58 (hN₂ : ∀ s,Fintype.card (K s)+Fintype.card (L s)+1 ≤ n)
    59 (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1)
    60 (hsmall : ∀ s,((2 : ℝ)^(Fintype.card (I s)*Fintype.card (J s)+2))*
    61 ((2 : ℝ)^(Fintype.card (K s)*Fintype.card (L s)+2))/Real.sqrt ((2 : ℝ)^n) ≤
    62 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots (I s) (J s) (K s) (L s))+1)) :
    63 |(∑ o : ∀ s,ChannelFiber (N := Fin n) (E s) (T s),weights (PMF.uniformOfFintype _) o*
    64 (f (fun s => batchEquiv ((Lax342547.FrameSymmetry.plus (o s).val).val*C₁ s,(Lax342547.FrameSymmetry.minus (o s).val).val*D₁ s))*
    65 g (fun s => batchEquiv ((Lax342547.FrameSymmetry.plus (o s).val).val*C₂ s,(Lax342547.FrameSymmetry.minus (o s).val).val*D₂ s))))-
    66 (∑ o : ∀ s,ChannelFiber (N := Fin n) (E s) (T s),weights (PMF.uniformOfFintype _) o*
    67 f (fun s => batchEquiv ((Lax342547.FrameSymmetry.plus (o s).val).val*C₁ s,(Lax342547.FrameSymmetry.minus (o s).val).val*D₁ s)))*
    68 (∑ o : ∀ s,ChannelFiber (N := Fin n) (E s) (T s),weights (PMF.uniformOfFintype _) o*
    69 g (fun s => batchEquiv ((Lax342547.FrameSymmetry.plus (o s).val).val*C₂ s,(Lax342547.FrameSymmetry.minus (o s).val).val*D₂ s)))| ≤
    70 ∑ s,errorBound n (I s) (J s) (K s) (L s)
    71
    72end
    73end Lax342547.RawGroupedComparison
    74
    Show 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…