Lax Lean Archive

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

Actual vanishing predictions on a retained population

Lax342547.RetainedEmptyPredictions · concepts/Lax342547/RetainedEmptyPredictions.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 aggregate generic parameter error gives an explicit discarded-mass bound, while the actual whole cut-space residual and common diagonal coefficient vanish exactly on retained units.

    Concept map
    35 concepts
    100%
    Actual point atoms determine cut-spacefunctionalsActual finite atom parameterization anddegreesPoint atoms and finite flavor distributionsThe exact space of binary base momentsBoolean polynomial nonvanishing andexactificationCommon star atoms eliminate the diagonalpredictor coefficientConcrete cut-space testers and the orderedmixer formConcrete coordinates, quadratic testers, andthe self-Gram formExact conditioning costs and recovery offinite probability massesEntropy progress for residual pair lawsCut profiles and the constant kernelExactification of actual vanishing pointpredictionsEntropy along feasible mixture lines,including new supportFull feasible support and finite informationprojectionFinite even moment expansionFinite independent sampling and vertexexception tailsThe symmetric binary gradient formThe binary hole relationBoolean point moments with restricted basecoordinatesFinite moment probability and rank splitSquared restriction cost for independent uniteventsBoolean degree of actual point-tensorevaluationsPolynomial degree of actual tensorevaluationsWalsh bounds for independent image lawsand separated phasesLinear point-tensor evaluations are BooleanquadraticsRaw matrix frames and their tensorrealizationOriginal retained-cell laws from finite PMFsFinite relative entropy and support costsActual vanishing predictions on a retainedpopulationImage caps inside original retained cellsInterpolation of finitely many binary selectorlabelsAn actual common point with diagonaltester oneMajority intersections in the cyclic taggeometryAdmissible pair lawsOrthogonality and finite Walsh correlationbounds
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

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

    1 prediction_error_le_total proven

    2 prediction_error_nonneg proven

    3 retained_vanishing_predictions proven

    Lean source view on GitHub

    1import Lax342547.EmptyPredictions
    2import Lax342547.MomentTails
    3
    4/-!
    5---
    6title: Actual vanishing predictions on a retained population
    7type: lemma
    8---
    9The aggregate generic parameter error gives an explicit discarded-mass bound, while the actual whole cut-space residual and common diagonal coefficient vanish exactly on retained units.
    10-/
    11
    12namespace Lax342547.RetainedEmptyPredictions
    13
    14open Lax342547.MomentSpace Lax342547.Atoms Lax342547.TagGeometry Lax342547.ConcreteCut
    15open Lax342547.ConcreteGeometry Lax342547.RetainedImages Lax342547.RelativeEntropy
    16open Lax342547.AtomParameters
    17open scoped BigOperators
    18
    19noncomputable def predictionError {k n b degree r : ℕ} (hr : 2*r ≤ n)
    20 (φ : Module.Dual Binary (Profile k n b degree)) (γ : Binary) (l : Tag k) (s : Fin b → Binary) : ℝ :=
    21 cellMass (fun _ : Fin (ParameterSize n l Flavor.generic) → Binary =>
    22 1/(2 : ℝ)^(ParameterSize n l Flavor.generic))
    23 (fun x => φ (parameterAtom (degree := degree) l s Flavor.generic x)+
    24 γ*eta (b := b) (degree := degree) hr (pointMoment selectorEval s (parameterBase l Flavor.generic x)) ≠ 0)
    25
    26noncomputable def totalPredictionError {k n b degree r : ℕ} (hr : 2*r ≤ n)
    27 (φ : Module.Dual Binary (Profile k n b degree)) (γ : Binary) (E : Finset (Fin b → Binary)) : ℝ := by
    28 classical
    29 exact ∑ l : Tag k,∑ s : Fin b → Binary,if s ∈ E then 0 else predictionError hr φ γ l s
    30
    31axiom prediction_error_nonneg {k n b degree r : ℕ} (hr : 2*r ≤ n)
    32 (φ : Module.Dual Binary (Profile k n b degree)) (γ : Binary) (l : Tag k) (s : Fin b → Binary) :
    33 0 ≤ predictionError hr φ γ l s
    34
    35axiom prediction_error_le_total {k n b degree r : ℕ} (hr : 2*r ≤ n)
    36 (φ : Module.Dual Binary (Profile k n b degree)) (γ : Binary) (E : Finset (Fin b → Binary))
    37 (l : Tag k) (s : Fin b → Binary) (hs : s ∉ E) :
    38 predictionError hr φ γ l s ≤ totalPredictionError hr φ γ E
    39
    40axiom retained_vanishing_predictions {U : Type} [Fintype U] {k n b degree r : ℕ}
    41 (hr : 2*r ≤ n) (hr0 : 0 < r) (β : U → ℝ)
    42 (φ : U → Module.Dual Binary (Profile k n b degree)) (γ : U → Binary)
    43 (E : U → Finset (Fin b → Binary)) (ε : ℝ) (hβ : Probability β)
    44 (hE : ∀ u,2^(degree+degree)*(E u).card < 2^b)
    45 (herr : (∑ u,β u*totalPredictionError hr (φ u) (γ u) (E u)) ≤ ε) :
    46 1-4*ε ≤ cellMass β (fun u => γ u = 0 ∧ φ u = 0)
    47
    48end Lax342547.RetainedEmptyPredictions
    49
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…