CompanionTrace.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Trace restart bounds for the literal 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.

lemma OAI.ContingencyTables.CompanionTrace.restart_exponential line 22
def OAI.ContingencyTables.CompanionTrace.integerConstant line 38
lemma OAI.ContingencyTables.CompanionTrace.integerConstant_cast line 42
def OAI.ContingencyTables.CompanionTrace.time line 48
def OAI.ContingencyTables.CompanionTrace.trace line 51
lemma OAI.ContingencyTables.CompanionTrace.trace_pi line 58
lemma OAI.ContingencyTables.CompanionTrace.actual_dual_degree line 65
lemma OAI.ContingencyTables.CompanionTrace.actual_plain_agreement line 72
lemma OAI.ContingencyTables.CompanionTrace.actual_lift_comparison line 77
lemma OAI.ContingencyTables.CompanionTrace.omission_instance line 87
lemma OAI.ContingencyTables.CompanionTrace.addition_instance line 93
lemma OAI.ContingencyTables.CompanionTrace.trace_poincare_raw line 99
theorem OAI.ContingencyTables.CompanionTrace.trace_poincare line 133
def OAI.ContingencyTables.CompanionTrace.minimumMass line 146
lemma OAI.ContingencyTables.CompanionTrace.minimumMass_positive line 149
theorem OAI.ContingencyTables.CompanionTrace.schedule_error line 155
Source documentation
The manuscript's literal integer restart schedule gives pointwise relative error at most one with the proved minimum mass.
```
theorem schedule_error (A : Instance I J) (H K : ℕ)
    (hp : 0 < Fintype.card (Labels A)) :
    Real.exp (-(time A H K:ℝ)/observableConstant (Fintype.card (Labels A)) ((A.W:ℝ)^2))/
      minimumMass A H K ≤ 1 := by
…
```
Mentions: OAI.ContingencyTables.CompanionTrace.time, OAI.ContingencyTables.CompanionTrace.minimumMass
lemma OAI.ContingencyTables.CompanionTrace.trace_minimum line 174

theorem OAI.ContingencyTables.CompanionTrace.trace_point_mixing line 186

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) (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 j) w) (t : ℕ)
    (x y : PlainIndex (pairs : List ((Labels A×Bool)×(Labels A×Bool)))) :
    |((trace A j hp w hw.positive).kernel.power t).P x y/
        CompanionWarmStart.law A j y.val.val-1| ≤
      Real.exp (-(t:ℝ)/observableConstant (Fintype.card (Labels A)) ((A.W:ℝ)^2))/minimumMass A H K := by
…

Mentions: OAI.ContingencyTables.CompanionTrace.trace, OAI.ContingencyTables.CompanionWarmStart.law, OAI.ContingencyTables.CompanionTrace.minimumMass

theorem OAI.ContingencyTables.CompanionTrace.stage_warm line 208

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) (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 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 j hp w hw.positive).kernel.power t).push nu y ≤ 2*CompanionWarmStart.law A j y.val.val := by
…

Mentions: OAI.ContingencyTables.CompanionTrace.minimumMass, OAI.ContingencyTables.CompanionTrace.trace, OAI.ContingencyTables.CompanionWarmStart.law