RootedTrace.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Trace restart bounds for the selected-root companion weights

The actual factorial lifts supply the trace inverse gap, and exact binomial cancellation supplies its minimum mass. The restart stage therefore has a two-warm endpoint from every initial subprobability law.

def OAI.ContingencyTables.RootedTrace.trace line 26
lemma OAI.ContingencyTables.RootedTrace.trace_pi line 33
lemma OAI.ContingencyTables.RootedTrace.actual_dual_degree line 40
lemma OAI.ContingencyTables.RootedTrace.actual_plain_agreement line 47
lemma OAI.ContingencyTables.RootedTrace.actual_lift_comparison line 52
lemma OAI.ContingencyTables.RootedTrace.omission_instance line 62
lemma OAI.ContingencyTables.RootedTrace.addition_instance line 68
lemma OAI.ContingencyTables.RootedTrace.trace_poincare_raw line 74
theorem OAI.ContingencyTables.RootedTrace.trace_poincare line 108
lemma OAI.ContingencyTables.RootedTrace.trace_minimum line 121

theorem OAI.ContingencyTables.RootedTrace.trace_point_mixing line 133

Source documentation

The pointwise error estimate has no new signature or minimum-mass assumption: both are supplied by the actual count/lift application.

theorem trace_point_mixing (A : Instance I J) (R : RootedCompletion.Selection A.T) (H K j : ℕ) (hj : j ≤ H)
    (hB : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1)) ≤ (2:ℝ)^K)
    (hp : 0 < Fintype.card (Labels A))
    (w : ((Labels A×Bool)×(Labels A×Bool)) → ((Labels A×Bool)×(Labels A×Bool)) → ℝ)
    (hw : GoodMultipliers pairs (weight A R j) w) (t : ℕ)
    (x y : PlainIndex (pairs : List ((Labels A×Bool)×(Labels A×Bool)))) :
    |((trace A R j hp w hw.positive).kernel.power t).P x y/
        RootedWarmStart.law A R j y.val.val-1| ≤
      Real.exp (-(t:ℝ)/observableConstant (Fintype.card (Labels A)) ((A.W:ℝ)^2))/minimumMass A H K := by
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTrace.trace, OAI.ContingencyTables.RootedWarmStart.law

theorem OAI.ContingencyTables.RootedTrace.stage_warm line 155

Source documentation

A stage with pointwise relative error at most one ends two-warm, even when its incoming law is merely a subprobability law.

theorem stage_warm (A : Instance I J) (R : RootedCompletion.Selection A.T) (H K j : ℕ) (hj : j ≤ H)
    (hB : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1)) ≤ (2:ℝ)^K)
    (hp : 0 < Fintype.card (Labels A))
    (w : ((Labels A×Bool)×(Labels A×Bool)) → ((Labels A×Bool)×(Labels A×Bool)) → ℝ)
    (hw : GoodMultipliers pairs (weight A R j) w) (t : ℕ)
    (ht : Real.exp (-(t:ℝ)/observableConstant (Fintype.card (Labels A)) ((A.W:ℝ)^2))/minimumMass A H K ≤ 1)
    (nu : PlainIndex (pairs : List ((Labels A×Bool)×(Labels A×Bool))) → ℝ)
    (hnu : ∀ S,0 ≤ nu S) (hmass : ∑ S,nu S ≤ 1)
    (y : PlainIndex (pairs : List ((Labels A×Bool)×(Labels A×Bool)))) :
    ((trace A R j hp w hw.positive).kernel.power t).push nu y ≤ 2*RootedWarmStart.law A R j y.val.val := by
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTrace.trace, OAI.ContingencyTables.RootedWarmStart.law