Lax Lean Archive

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

Early channel choice and injection exponent budgets

Lax342547.InjectionBudgets · concepts/Lax342547/InjectionBudgets.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 channel dimension chosen before unit laws pays the accepting-family union, while actual conditioned primal avoidance retains an exponential margin.

    Concept map
    62 concepts; 7 descendants hidden
    100%
    Actual projected span deficitSampling after exposed coordinatesAdaptive sampling on disjoint coordinatesetsUnion over adaptive component coversExact uniform bilinear character meanWalsh operator bounds with explicit bilinearrankRank of a lifted tensor sumIndependent binary channel charactersActual channel moments and phase tailsCombined column and row mode exposureRows of diagonal tensor mapsMoment estimates for actual componenttensor phasesComponentwise mode spaces and diagonaltensorsExact 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 even moment expansionFinite independent sampling and vertexexception tailsGreedy mode space exposureSmall actual greedy exposure tailsNo-cover rank growth on arbitrary finiteindicesEarly channel choice and injection exponentbudgetsActual deficits indexed by a distinct listFinite list tail statisticsDimension deficits after an arbitrary modemapExposed mode dimension budgetExplicit no-cover moment parameter marginsBoolean point moments with restricted basecoordinatesFinite moment probability and rank splitA low rank sum supplies an actual adaptivecoverNo-cover phase momentsRank 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 sumCharacters of all independent tensor channelsAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 accepting_family_exponential_budget proven

    2 amplified_ratio_budget proven

    3 conditioned_avoidance_budget proven

    4 early_channel_margin proven

    5 primal_avoidance_exponent proven

    6 quotient_probe_length proven

    Lean source view on GitHub

    1import Lax342547.MomentBudgets
    2
    3/-!
    4---
    5title: Early channel choice and injection exponent budgets
    6type: lemma
    7---
    8The channel dimension chosen before unit laws pays the accepting-family union, while actual conditioned primal avoidance retains an exponential margin.
    9-/
    10
    11namespace Lax342547.InjectionBudgets
    12
    13
    14
    15axiom amplified_ratio_budget (h K ℓ t m c N : ℕ) (L gap count : ℝ)
    16 (hL : 0 ≤ L) (hg : 1/(2 : ℝ)^t ≤ gap)
    17 (hLc : L ≤ (2 : ℝ)^m) (hc : count ≤ (2 : ℝ)^c) (hcount : 0 ≤ count)
    18 (hb : m+c+h*K+(2*K+t)*ℓ+N ≤ h*ℓ) :
    19 count*((L*((2 : ℝ)^(h*K+2*K*ℓ)/(2 : ℝ)^(h*ℓ)))/gap^ℓ) ≤ 1/(2 : ℝ)^N
    20
    21axiom quotient_probe_length (K N : ℕ) (hN : 20*(K+1) ≤ N) :
    22 N ≤ 20*(K+1)*(N/(10*(K+1)))
    23
    24axiom early_channel_margin (K t Cs m h N : ℕ)
    25 (hh : 2*K+t+20*(K+1)*(Cs+3) ≤ h)
    26 (hN : 20*(K+1) ≤ N) (hm : m+h*K ≤ N) :
    27 (m+N)+Cs*N+h*K+(2*K+t)*(N/(10*(K+1)))+N ≤ h*(N/(10*(K+1)))
    28
    29axiom accepting_family_exponential_budget (K t Cs m h N : ℕ) (L gap count : ℝ)
    30 (hL : 0 ≤ L) (hcount : 0 ≤ count) (hg : 1/(2 : ℝ)^t ≤ gap)
    31 (hLc : L ≤ (2 : ℝ)^(m+N)) (hc : count ≤ (2 : ℝ)^(Cs*N))
    32 (hh : 2*K+t+20*(K+1)*(Cs+3) ≤ h)
    33 (hN : 20*(K+1) ≤ N) (hm : m+h*K ≤ N) :
    34 count*((L*((2 : ℝ)^(h*K+2*K*(N/(10*(K+1))))/(2 : ℝ)^(h*(N/(10*(K+1))))))/gap^(N/(10*(K+1)))) ≤
    35 1/(2 : ℝ)^N
    36
    37axiom primal_avoidance_exponent (K b h m N : ℕ)
    38 (hb : b ≤ N/8) (hm : m+h+1 ≤ N/10) :
    39 m+N/100+b+h+K*(N/(10*(K+1)))+1+N/2 ≤ N
    40
    41axiom conditioned_avoidance_budget (K b h m N : ℕ) (M : ℝ)
    42 (hM : 0 ≤ M) (hMc : M ≤ (2 : ℝ)^m)
    43 (hb : b ≤ N/8) (hm : m+h+1 ≤ N/10) :
    44 (M/(1/(2 : ℝ)^(N/100)))*(2*((2 : ℝ)^(b+h+K*(N/(10*(K+1))))/(2 : ℝ)^N)) ≤
    45 1/(2 : ℝ)^(N/2)
    46
    47end Lax342547.InjectionBudgets
    48
    Show ProofShow 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…