Lax Lean Archive

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

Conditioned affine-slice variance under the actual raw law

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

    The actual one-batch orbit law and grouped two-batch comparison discharge the finite empirical-variance hypotheses. The coefficient law may have arbitrary other coordinates and an independent uniform free block. Conditioning on a positive-mass prescribed Gram event retains its explicit squared mass cost.

    Concept map
    43 concepts; 6 descendants hidden
    100%
    Exact-image bounds for independent affinecolumnsIndependent nominal affine slices from thefree blockConditioned affine-slice variance under theactual raw lawWalsh operator bounds with explicit bilinearrankConcrete coordinates, quadratic testers, andthe self-Gram formActual conditioned affine coefficientdependence boundsExact finite conditioning of separated FouriertestsExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsQuantitative comparison after cross-batchGram conditioningIndependent characters of actual mutualGram entriesCut profiles and the constant kernelFinite empirical variance from atwo-coefficient comparisonEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionFinite linear images and their uniform-lawdensity boundsFinite independent sampling and vertexexception tailsFinite scalar agreement from binarycharacter boundsAmbient symmetries and frame marginalsUniform tuple images on prescribed GramorbitsThe symmetric binary gradient formGram-conditioned columns and theirrank-failure probabilityTwo-sided Gram normalization forindividually injective framesActual reference-batch laws for mutual GramtestsTwo-batch comparison across independentcomponent groupsThe binary hole relationExact joining of two prescribed Gram orbitsJoint-injectivity loss for two actual referencebatchesBoolean point moments with restricted basecoordinatesSquared restriction cost for independent uniteventsWalsh bounds for independent image lawsand separated phasesBounded tests under the actual two-batchGram lawActual raw frame observations with uniformtwo-batch decayRaw matrix frames and their tensorrealizationActual grouped raw observations witharbitrary common testsThe finite uniform raw-vertex lawOriginal retained-cell laws from finite PMFsFinite relative entropy and support costsImage caps inside original retained cellsBit rank and Walsh bounds for globalvector-slot pairingsMajority intersections in the cyclic taggeometryAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 affine_slice_variance proven

    2 coefficient_variance proven

    3 flavored_slice_variance proven

    4 independent_free_pair_bound proven

    5 reference_mean proven

    Lean source view on GitHub

    1import Lax342547.ConditionedAffineColumns
    2import Lax342547.RawGroupedComparison
    3import Lax342547.EmpiricalVariance
    4
    5/-!
    6---
    7title: Conditioned affine-slice variance under the actual raw law
    8type: lemma
    9---
    10The actual one-batch orbit law and grouped two-batch comparison discharge the
    11finite empirical-variance hypotheses. The coefficient law may have arbitrary
    12other coordinates and an independent uniform free block. Conditioning on a
    13positive-mass prescribed Gram event retains its explicit squared mass cost.
    14-/
    15
    16namespace Lax342547.AffineSliceVariance
    17noncomputable section
    18open Lax342547.MomentSpace Lax342547.FrameTuples Lax342547.RawFrames
    19open Lax342547.RealCellLaws Lax342547.GramOrbitDensity Lax342547.RelativeEntropy
    20open Lax342547.TagGeometry Lax342547.ConcreteGeometry Lax342547.AffineSliceIndependence
    21open Lax342547.RetainedImages
    22open scoped BigOperators
    23
    24def referenceMean {S D : Type} [Fintype S] [DecidableEq S] [Fintype D] [DecidableEq D]
    25 (n : ℕ) (G : S → Matrix D D Binary) [∀ s,Nonempty (Orbit (Fin n) (G s))]
    26 (test : (S → (Fin n × (D ⊕ D) → Binary)) → ℝ) : ℝ :=
    27 ∑ z : ∀ s,Orbit (Fin n) (G s),weights (PMF.uniformOfFintype _) z*
    28 test (fun s => batchEquiv (z s).val)
    29
    30axiom reference_mean {S B H D : Type} [Fintype S] [DecidableEq S]
    31 [Fintype B] [Fintype H] [Fintype D] [DecidableEq D]
    32 (n : ℕ) (E : S → Matrix B B Binary) (G : S → Matrix D D Binary)
    33 [∀ s,Nonempty (Frame B H (Fin n) (E s))] [∀ s,Nonempty (Orbit (Fin n) (G s))]
    34 (C : Matrix B D Binary) (hC : Function.Injective C.mulVec)
    35 (hG : ∀ s,C.transpose*E s*C = G s)
    36 (test : (S → (Fin n × (D ⊕ D) → Binary)) → ℝ) :
    37 (∑ o : ∀ s,Frame B H (Fin n) (E s),weights (PMF.uniformOfFintype _) o*
    38 test (fun s => batchEquiv ((o s).P*C,(o s).Q*C))) =
    39 ∑ z : ∀ s,Orbit (Fin n) (G s),weights (PMF.uniformOfFintype _) z*
    40 test (fun s => batchEquiv (z s).val)
    41
    42axiom coefficient_variance {S B H D A : Type} [Fintype S] [DecidableEq S]
    43 [Fintype B] [Fintype H] [Fintype D] [DecidableEq D] [Fintype A]
    44 (n : ℕ) (E : S → Matrix B B Binary) (G : S → Matrix D D Binary)
    45 [∀ s,Nonempty (Frame B H (Fin n) (E s))] [∀ s,Nonempty (Orbit (Fin n) (G s))]
    46 (C : A → Matrix B D Binary) (κ : A → ℝ) (hκ : Probability κ)
    47 (hGram : ∀ a,κ a ≠ 0 → ∀ s,(C a).transpose*E s*C a = G s)
    48 (test : (S → (Fin n × (D ⊕ D) → Binary)) → ℝ) (htest : ∀ z,|test z| ≤ 1)
    49 (δ : ℝ) (hbad : Lax342547.RetainedImages.cellMass (fun ab : A × A => κ ab.1*κ ab.2)
    50 (fun ab => ¬ Function.Injective (Matrix.fromCols (C ab.1) (C ab.2)).mulVec) ≤ δ)
    51 (hN : Fintype.card D+Fintype.card D+1 ≤ n)
    52 (hsmall : ((2 : ℝ)^(Fintype.card D*Fintype.card D+2))*
    53 ((2 : ℝ)^(Fintype.card D*Fintype.card D+2))/Real.sqrt ((2 : ℝ)^n) ≤
    54 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots D D D D)+1)) :
    55 (∑ o : ∀ s,Frame B H (Fin n) (E s),weights (PMF.uniformOfFintype _) o*
    56 ((∑ a,κ a*test (fun s => batchEquiv ((o s).P*C a,(o s).Q*C a)))-
    57 referenceMean n G test)^2) ≤
    58 (Fintype.card S : ℝ)*Lax342547.RawFrameComparison.errorBound n D D D D+4*δ
    59
    60def GramEvent {S D : Type} {k n b degree : ℕ} [Fintype D]
    61 (sel : Fin b → Binary) (E : S → Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary)
    62 (G : S → Matrix (Option D) (Option D) Binary)
    63 (V : Matrix (Base k n) (Option D) Binary) : Prop :=
    64 ∀ i,(pointColumns sel V).transpose*E i*pointColumns sel V = G i
    65
    66axiom affine_slice_variance {S H D : Type} [Fintype S] [DecidableEq S]
    67 [Fintype H] [Fintype D] [DecidableEq D] {k n b degree : ℕ}
    68 (N : ℕ) (sel : Fin b → Binary)
    69 (E : S → Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary)
    70 (G : S → Matrix (Option D) (Option D) Binary)
    71 [∀ i,Nonempty (Frame (Coordinate k n b degree) H (Fin N) (E i))]
    72 [∀ i,Nonempty (Orbit (Fin N) (G i))]
    73 (β : ℝ) (hβ : 0 < β)
    74 (hGram : β ≤ cellMass (weights (PMF.uniformOfFintype (Matrix (Base k n) (Option D) Binary)))
    75 (GramEvent sel E G))
    76 (test : (S → (Fin N × (Option D ⊕ Option D) → Binary)) → ℝ) (htest : ∀ z,|test z| ≤ 1)
    77 (hN : Fintype.card (Option D)+Fintype.card (Option D)+1 ≤ N)
    78 (hsmall : ((2 : ℝ)^(Fintype.card (Option D)*Fintype.card (Option D)+2))*
    79 ((2 : ℝ)^(Fintype.card (Option D)*Fintype.card (Option D)+2))/Real.sqrt ((2 : ℝ)^N) ≤
    80 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots (Option D) (Option D) (Option D) (Option D))+1)) :
    81 (∑ o : ∀ i,Frame (Coordinate k n b degree) H (Fin N) (E i),weights (PMF.uniformOfFintype _) o*
    82 ((∑ V : Matrix (Base k n) (Option D) Binary,
    83 conditionalLaw (weights (PMF.uniformOfFintype _)) (GramEvent sel E G) V*
    84 test (fun i => batchEquiv ((o i).P*pointColumns sel V,(o i).Q*pointColumns sel V)))-
    85 referenceMean N G test)^2) ≤
    86 (Fintype.card S : ℝ)*Lax342547.RawFrameComparison.errorBound N (Option D) (Option D) (Option D) (Option D)+
    87 4*(((2 : ℝ)^(2*Fintype.card D+1)/(2 : ℝ)^n)/β^2)
    88
    89axiom independent_free_pair_bound {A B : Type} [Fintype A] [Fintype B]
    90 (α : A → ℝ) (β : B → ℝ) (hα : Probability α) (_hβ : Probability β)
    91 (bad : (A × B) × (A × B) → Prop) (δ : ℝ)
    92 (hbad : ∀ a : A × A,cellMass (fun z : B × B => β z.1*β z.2)
    93 (fun z => bad ((a.1,z.1),(a.2,z.2))) ≤ δ) :
    94 cellMass (fun z : (A × B) × (A × B) => (α z.1.1*β z.1.2)*(α z.2.1*β z.2.2)) bad ≤ δ
    95
    96def flavoredLaw {A D : Type} [Fintype D] [DecidableEq D] {n : ℕ} (μ : A → ℝ) :
    97 (A × Matrix (Fin n) (Option D) Binary) → ℝ :=
    98 fun a => μ a.1*weights (PMF.uniformOfFintype (Matrix (Fin n) (Option D) Binary)) a.2
    99
    100def conditionedFlavorLaw {S A D : Type} [Fintype A] [Fintype D] [DecidableEq D]
    101 {k n b degree : ℕ} (sel : Fin b → Binary)
    102 (E : S → Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary)
    103 (G : S → Matrix (Option D) (Option D) Binary)
    104 (μ : A → ℝ) (V : A → Matrix (Base k n) (Option D) Binary) :
    105 (A × Matrix (Fin n) (Option D) Binary) → ℝ :=
    106 conditionalLaw (flavoredLaw μ) (fun a => GramEvent sel E G (setFree (V a.1) a.2))
    107
    108axiom flavored_slice_variance {S H D A : Type} [Fintype S] [DecidableEq S]
    109 [Fintype H] [Fintype D] [DecidableEq D] [Fintype A] {k n b degree : ℕ}
    110 (N : ℕ) (sel : Fin b → Binary)
    111 (E : S → Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary)
    112 (G : S → Matrix (Option D) (Option D) Binary)
    113 [∀ i,Nonempty (Frame (Coordinate k n b degree) H (Fin N) (E i))]
    114 [∀ i,Nonempty (Orbit (Fin N) (G i))]
    115 (μ : A → ℝ) (hμ : Probability μ) (V : A → Matrix (Base k n) (Option D) Binary)
    116 (β : ℝ) (hβ : 0 < β)
    117 (hGram : β ≤ cellMass (flavoredLaw (n := n) (D := D) μ) (fun a => GramEvent (k := k) (n := n) (b := b) (degree := degree) sel E G (setFree (k := k) (n := n) (D := D) (V a.1) a.2)))
    118 (test : (S → (Fin N × (Option D ⊕ Option D) → Binary)) → ℝ) (htest : ∀ z,|test z| ≤ 1)
    119 (hN : Fintype.card (Option D)+Fintype.card (Option D)+1 ≤ N)
    120 (hsmall : ((2 : ℝ)^(Fintype.card (Option D)*Fintype.card (Option D)+2))*
    121 ((2 : ℝ)^(Fintype.card (Option D)*Fintype.card (Option D)+2))/Real.sqrt ((2 : ℝ)^N) ≤
    122 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots (Option D) (Option D) (Option D) (Option D))+1)) :
    123 (∑ o : ∀ i,Frame (Coordinate k n b degree) H (Fin N) (E i),weights (PMF.uniformOfFintype _) o*
    124 ((∑ a : A × Matrix (Fin n) (Option D) Binary,conditionedFlavorLaw sel E G μ V a*
    125 test (fun i => batchEquiv ((o i).P*pointColumns (k := k) (n := n) (b := b) (degree := degree) (D := D) sel (setFree (k := k) (n := n) (D := D) (V a.1) a.2),
    126 (o i).Q*pointColumns (k := k) (n := n) (b := b) (degree := degree) (D := D) sel (setFree (k := k) (n := n) (D := D) (V a.1) a.2))))-referenceMean N G test)^2) ≤
    127 (Fintype.card S : ℝ)*Lax342547.RawFrameComparison.errorBound N (Option D) (Option D) (Option D) (Option D)+
    128 4*(((2 : ℝ)^(2*Fintype.card D+1)/(2 : ℝ)^n)/β^2)
    129
    130end
    131end Lax342547.AffineSliceVariance
    132
    Show 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…