Lax Lean Archive

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

Affine-slice comparison for every actual atom flavor

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

    Lemma 9.4 uses independent uniform affine coefficients on exactly the actual retained coordinates of the chosen flavor. The free projection is exactly uniform for generic, shared-only and every pure flavor. Conditioning on all prescribed component Grams has the explicit beta^-2 cost, with no cost for setting excluded flavor coordinates to zero. Arbitrary bounded common tests of the actual primal image arrays satisfy the checked variance budget.

    Concept map
    46 concepts; 4 descendants hidden
    100%
    Exact-image bounds for independent affinecolumnsIndependent nominal affine slices from thefree blockConditioned affine-slice variance under theactual raw lawPoint atoms and finite flavor distributionsWalsh operator bounds with explicit bilinearrankConcrete cut-space testers and the orderedmixer formConcrete 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 tailsAffine-slice comparison for every actual atomflavorFinite 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 4 statements. Each proof establishes one of them relative to its assumptions.

    1 conditioned_pair_failure proven

    2 flavor_slice_variance proven

    3 free_pair_uniform proven

    4 nominal_pair_failure proven

    Lean source view on GitHub

    1import Lax342547.AffineSliceVariance
    2import Lax342547.Atoms
    3
    4/-!
    5---
    6title: Affine-slice comparison for every actual atom flavor
    7type: lemma
    8---
    9Lemma 9.4 uses independent uniform affine coefficients on exactly the actual
    10retained coordinates of the chosen flavor. The free projection is exactly
    11uniform for generic, shared-only and every pure flavor. Conditioning on all
    12prescribed component Grams has the explicit beta^-2 cost, with no cost for
    13setting excluded flavor coordinates to zero. Arbitrary bounded common tests
    14of the actual primal image arrays satisfy the checked variance budget.
    15-/
    16
    17namespace Lax342547.FlavorAffineSlices
    18noncomputable section
    19open Lax342547.MomentSpace Lax342547.Atoms Lax342547.TagGeometry Lax342547.ConcreteGeometry
    20open Lax342547.AffineSliceIndependence Lax342547.RetainedImages Lax342547.RealCellLaws
    21open Lax342547.RawFrames Lax342547.FrameTuples Lax342547.GramOrbitDensity Lax342547.RelativeEntropy
    22open Lax342547.AffineSliceVariance
    23open scoped BigOperators ENNReal
    24
    25abbrev Coefficients {k : ℕ} (n : ℕ) (l : Tag k) (f : Flavor k) (D : Type) :=
    26 Matrix {i : Base k n // i ∈ retained (k := k) (n := n) l f} (Option D) Binary
    27
    28 noncomputable instance {k n : ℕ} (l : Tag k) (f : Flavor k) (D : Type) [Fintype D] :
    29 Fintype (Coefficients n l f D) := Fintype.ofFinite _
    30
    31noncomputable def value {k n : ℕ} {l : Tag k} {f : Flavor k} {D : Type}
    32 (V : Coefficients n l f D) : Matrix (Base k n) (Option D) Binary :=
    33 fun i j => parameterValue (fun a => V a j) i
    34
    35def freeIndex {k n : ℕ} (l : Tag k) (f : Flavor k) (i : Fin n) :
    36 {a : Base k n // a ∈ retained (k := k) (n := n) l f} :=
    37 ⟨free i,by
    38 cases f with
    39 | generic => trivial
    40 | sharedOnly => trivial
    41 | pure blocks => change (2 : Fin 3) ≠ 0; decide⟩
    42
    43def freePairMap {k n : ℕ} {l : Tag k} {f : Flavor k} {D : Type} :
    44 (Coefficients n l f D × Coefficients n l f D) →ₗ[Binary]
    45 (Matrix (Fin n) (Option D) Binary × Matrix (Fin n) (Option D) Binary) where
    46 toFun V := (fun i j => V.1 (freeIndex l f i) j,fun i j => V.2 (freeIndex l f i) j)
    47 map_add' _ _ := rfl
    48 map_smul' _ _ := rfl
    49
    50axiom free_pair_uniform {k n : ℕ} (l : Tag k) (f : Flavor k) {D : Type}
    51 [Fintype D] [DecidableEq D] :
    52 (PMF.uniformOfFintype (Coefficients n l f D × Coefficients n l f D)).map freePairMap =
    53 PMF.uniformOfFintype (Matrix (Fin n) (Option D) Binary × Matrix (Fin n) (Option D) Binary)
    54
    55axiom nominal_pair_failure {k n b degree : ℕ} (l : Tag k) (f : Flavor k)
    56 {D : Type} [Fintype D] [DecidableEq D] (s : Fin b → Binary) :
    57 (PMF.uniformOfFintype (Coefficients n l f D × Coefficients n l f D)).toOuterMeasure
    58 {V | ¬ Function.Injective (fun uv : (Option D → Binary) × (Option D → Binary) =>
    59 (pointColumns (degree := degree) s (value V.1)).mulVec uv.1+
    60 (pointColumns (degree := degree) s (value V.2)).mulVec uv.2)} ≤
    61 (2 : ℝ≥0∞)^(2*Fintype.card D+1)/(2 : ℝ≥0∞)^n
    62
    63axiom conditioned_pair_failure {k n b degree : ℕ} (l : Tag k) (f : Flavor k)
    64 {D : Type} [Fintype D] [DecidableEq D] (s : Fin b → Binary)
    65 (C : Coefficients n l f D → Prop) (β : ℝ) (hβ : 0 < β)
    66 (hC : β ≤ cellMass (weights (PMF.uniformOfFintype (Coefficients n l f D))) C) :
    67 cellMass (fun V : Coefficients n l f D × Coefficients n l f D =>
    68 conditionalLaw (weights (PMF.uniformOfFintype _)) C V.1*
    69 conditionalLaw (weights (PMF.uniformOfFintype _)) C V.2)
    70 (fun V => ¬ Function.Injective (fun uv : (Option D → Binary) × (Option D → Binary) =>
    71 (pointColumns (degree := degree) s (value V.1)).mulVec uv.1+
    72 (pointColumns (degree := degree) s (value V.2)).mulVec uv.2)) ≤
    73 ((2 : ℝ)^(2*Fintype.card D+1)/(2 : ℝ)^n)/β^2
    74
    75axiom flavor_slice_variance {S H D : Type} [Fintype S] [DecidableEq S]
    76 [Fintype H] [Fintype D] [DecidableEq D] {k n b degree : ℕ}
    77 (l : Tag k) (f : Flavor k)
    78 (N : ℕ) (sel : Fin b → Binary)
    79 (E : S → Matrix (Coordinate k n b degree) (Coordinate k n b degree) Binary)
    80 (G : S → Matrix (Option D) (Option D) Binary)
    81 [∀ i,Nonempty (Frame (Coordinate k n b degree) H (Fin N) (E i))]
    82 [∀ i,Nonempty (Orbit (Fin N) (G i))]
    83 (β : ℝ) (hβ : 0 < β)
    84 (hGram : β ≤ cellMass (weights (PMF.uniformOfFintype (Coefficients n l f D)))
    85 (fun V : Coefficients n l f D => GramEvent sel E G (value V)))
    86 (test : (S → (Fin N × (Option D ⊕ Option D) → Binary)) → ℝ) (htest : ∀ z,|test z| ≤ 1)
    87 (hN : Fintype.card (Option D)+Fintype.card (Option D)+1 ≤ N)
    88 (hsmall : ((2 : ℝ)^(Fintype.card (Option D)*Fintype.card (Option D)+2))*
    89 ((2 : ℝ)^(Fintype.card (Option D)*Fintype.card (Option D)+2))/Real.sqrt ((2 : ℝ)^N) ≤
    90 1/(2 : ℝ)^(Fintype.card (Lax342547.CrossGramBasis.Slots (Option D) (Option D) (Option D) (Option D))+1)) :
    91 (∑ o : ∀ i,Frame (Coordinate k n b degree) H (Fin N) (E i),weights (PMF.uniformOfFintype _) o*
    92 ((∑ V : Coefficients n l f D,
    93 conditionalLaw (weights (PMF.uniformOfFintype _)) (fun V : Coefficients n l f D => GramEvent sel E G (value V)) V*
    94 test (fun i => batchEquiv ((o i).P*pointColumns (k := k) (n := n) (b := b) (degree := degree) sel (value V),(o i).Q*pointColumns (k := k) (n := n) (b := b) (degree := degree) sel (value V))))-
    95 referenceMean N G test)^2) ≤
    96 (Fintype.card S : ℝ)*Lax342547.RawFrameComparison.errorBound N (Option D) (Option D) (Option D) (Option D)+
    97 4*(((2 : ℝ)^(2*Fintype.card D+1)/(2 : ℝ)^n)/β^2)
    98
    99end
    100end Lax342547.FlavorAffineSlices
    101
    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…