Lax Lean Archive

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

Actual reference-batch laws for mutual Gram tests

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

    Flatten both signs of a paired Gram orbit into one batch. Its independent-bit density denominator is explicit; arbitrary tests retain the reciprocal mutual-Gram comparison with no independence assumption inside either batch.

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

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

    1 batch_point_cap proven

    2 batch_probability proven

    3 mutual_gram_comparison proven

    Lean source view on GitHub

    1import Lax342547.FrameTuples
    2import Lax342547.RealCellLaws
    3import Lax342547.CrossGramBasis
    4
    5/-!
    6---
    7title: Actual reference-batch laws for mutual Gram tests
    8type: lemma
    9---
    10Flatten both signs of a paired Gram orbit into one batch. Its independent-bit
    11density denominator is explicit; arbitrary tests retain the reciprocal
    12mutual-Gram comparison with no independence assumption inside either batch.
    13-/
    14
    15namespace Lax342547.GramOrbitDensity
    16
    17open Lax342547.RelativeEntropy
    18open scoped BigOperators
    19
    20open Lax342547.MomentSpace Lax342547.FrameTuples Lax342547.RealCellLaws
    21
    22def batchEquiv {I J N : Type} :
    23 (Matrix N I Binary × Matrix N J Binary) ≃ (N × (I ⊕ J) → Binary) where
    24 toFun z p := match p.2 with
    25 | Sum.inl i => z.1 p.1 i
    26 | Sum.inr j => z.2 p.1 j
    27 invFun x := (fun n i => x (n,Sum.inl i),fun n j => x (n,Sum.inr j))
    28 left_inv z := rfl
    29 right_inv x := by funext p; rcases p with ⟨n,i|j⟩ <;> rfl
    30
    31noncomputable def batchLaw {I J N : Type} [Fintype I] [Fintype J] [Fintype N]
    32 [DecidableEq N] (G : Matrix I J Binary) [Nonempty (Orbit N G)] :
    33 (N × (I ⊕ J) → Binary) → ℝ :=
    34 weights ((PMF.uniformOfFintype (Orbit N G)).map (fun z => batchEquiv z.val))
    35
    36axiom batch_probability {I J N : Type} [Fintype I] [Fintype J] [Fintype N]
    37 [DecidableEq I] [DecidableEq J] [DecidableEq N] (G : Matrix I J Binary)
    38 [Nonempty (Orbit N G)] : Probability (batchLaw (N := N) G)
    39
    40axiom batch_point_cap {I J N : Type} [Fintype I] [Fintype J] [Fintype N]
    41 [DecidableEq I] [DecidableEq J] [DecidableEq N] (G : Matrix I J Binary)
    42 [Nonempty (Orbit N G)] (hN : Fintype.card I+Fintype.card J+1 ≤ Fintype.card N)
    43 (x : N × (I ⊕ J) → Binary) :
    44 batchLaw G x ≤ (2 : ℝ)^(Fintype.card I*Fintype.card J+2)/
    45 (2 : ℝ)^(Fintype.card N*(Fintype.card I+Fintype.card J))
    46
    47axiom mutual_gram_comparison {I J K L : Type} [Fintype I] [Fintype J]
    48 [Fintype K] [Fintype L] [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L]
    49 (N : ℕ) (G : Matrix I J Binary) (H : Matrix K L Binary)
    50 [Nonempty (Orbit (Fin N) G)] [Nonempty (Orbit (Fin N) H)]
    51 (f : (Fin N × (I ⊕ J) → Binary) → ℝ) (g : (Fin N × (K ⊕ L) → Binary) → ℝ)
    52 (target : Lax342547.CrossGramBasis.Slots I J K L → Binary)
    53 (hN₁ : Fintype.card I+Fintype.card J+1 ≤ N)
    54 (hN₂ : Fintype.card K+Fintype.card L+1 ≤ N)
    55 (hf : ∀ x,|f x| ≤ 1) (hg : ∀ y,|g y| ≤ 1)
    56 (hsmall : ((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    57 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))/Real.sqrt ((2 : ℝ)^N) ≤
    58 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+1)) :
    59 |Lax342547.FourierTests.patternMass (fun xy => batchLaw G xy.1*batchLaw H xy.2*(f xy.1*g xy.2))
    60 (Lax342547.CrossBatchMixing.crossBits Lax342547.CrossGramBasis.tests N) target /
    61 Lax342547.FourierTests.patternMass (fun xy => batchLaw G xy.1*batchLaw H xy.2)
    62 (Lax342547.CrossBatchMixing.crossBits Lax342547.CrossGramBasis.tests N) target -
    63 (∑ x,batchLaw G x*f x)*(∑ y,batchLaw H y*g y)| ≤
    64 (2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots I J K L)+2)*
    65 (((2 : ℝ)^(Fintype.card I*Fintype.card J+2))*
    66 ((2 : ℝ)^(Fintype.card K*Fintype.card L+2))/Real.sqrt ((2 : ℝ)^N))
    67
    68end Lax342547.GramOrbitDensity
    69
    Show 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…