Lax Lean Archive

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

Rank growth without an adaptive mode cover

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

    Actual low rank sums force a cover based on exposed indices; conditioning on those indices and taking the finite union yields a checked no-cover probability bound for any join-stable cover classes.

    Concept map
    48 concepts
    100%
    Actual projected span deficitSampling after exposed coordinatesAdaptive sampling on disjoint coordinatesetsUnion over adaptive component coversRank of a lifted tensor sumCombined column and row mode exposureExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsIndependence of distinct sample positionsJoin-stable classes of mode coversCount tensors killed by exposureActual exposure cover projectionRank of a diagonal familyDyadic span deficit estimatesA small dyadic tail scaleActual dyadic deficit recurrenceEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionProjection removes the exposed termsCount tested index occurrencesFinite independent sampling and vertexexception tailsGreedy mode space exposureSmall actual greedy exposure tailsActual deficits indexed by a distinct listFinite list tail statisticsDimension deficits after an arbitrary modemapExposed mode dimension budgetBoolean point moments with restricted basecoordinatesA low rank sum supplies an actual adaptivecoverRank growth without an adaptive modecoverSquared restriction cost for independent uniteventsFinite exposure partitionsProjected nonzero terms in the actualremaining sumDimensions of projected mode spacesWalsh bounds for independent image lawsand separated phasesRank of a tensor killed in two quotientspacesRank loss under two restrictionsOriginal retained-cell laws from finite PMFsFinite relative entropy and support costsRank loss under restriction of a bilinear formImage caps inside original retained cellsOne exposure controls both modesMonotonicity of span deficitsMode space span deficitsNonzero tensor count from span deficitsRank of an actual linear map sumAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax342547.NoCoverCertificate
    2import Lax342547.CoverClasses
    3import Lax342547.AdaptiveUnion
    4
    5/-!
    6---
    7title: Rank growth without an adaptive mode cover
    8type: lemma
    9---
    10Actual low rank sums force a cover based on exposed indices; conditioning on those indices and taking the finite union yields a checked no-cover probability bound for any join-stable cover classes.
    11-/
    12
    13namespace Lax342547.NoCoverRank
    14
    15open Lax342547.CoverProjection Lax342547.CoverClasses
    16open Lax342547.RelativeEntropy Lax342547.FiniteSampling Lax342547.RetainedImages
    17open scoped BigOperators
    18
    19axiom no_cover_rank_probability {K V W ι Ω : Type} [Field K]
    20 [Fintype ι] [DecidableEq ι] [Fintype Ω]
    21 [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W]
    22 [FiniteDimensional K V] [FiniteDimensional K W]
    23 (μ : Ω → ℝ) (M : Ω → V →ₗ[K] W) (P : Submodule K W → Prop)
    24 (Q : Submodule K (Module.Dual K V) → Prop) (r p : ℝ) (k n : ℕ)
    25 (hμ : Probability μ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hr : 0 ≤ r)
    26 (hM : ∀ x, (Module.finrank K (LinearMap.range (M x)) : ℝ) ≤ r)
    27 (hP : JoinClosed P) (hQ : JoinClosed Q)
    28 (hPC : ∀ x, P (LinearMap.range (M x))) (hQR : ∀ x, Q (LinearMap.range (M x).dualMap))
    29 (hcard : Fintype.card ι = 2^k) (hnk : n ≤ k) (hn : 16*r < n)
    30 (hcover : ∀ S T, P S → Q T →
    31 (Module.finrank K S : ℝ) ≤ r*Fintype.card ι →
    32 (Module.finrank K T : ℝ) ≤ r*Fintype.card ι →
    33 cellMass μ (fun x => projection (M x) S T = 0) ≤ p) :
    34 cellMass (productLaw (fun _ : ι => μ))
    35 (fun sample => (Module.finrank K (LinearMap.range (∑ i, M (sample i))) : ℝ) < (2^(k-n) : ℝ)/4) ≤
    36 (4 : ℝ)^Fintype.card ι*p^(2^(k-n))
    37
    38end Lax342547.NoCoverRank
    39
    Show 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…