RootedRestartStages.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Successive selected-root restart stages

The reference law is refreshed by the exact trace at each successive parameter. Only that reference law is asserted to be warm. The actual bounded-return law is compared to it by contraction and accumulated error.

lemma OAI.ContingencyTables.RootedRestartStages.accumulate line 23
def OAI.ContingencyTables.RootedRestartStages.reference line 31
lemma OAI.ContingencyTables.RootedRestartStages.reference_nonnegative line 39
lemma OAI.ContingencyTables.RootedRestartStages.reference_mass line 51
theorem OAI.ContingencyTables.RootedRestartStages.reference_two_warm line 65
theorem OAI.ContingencyTables.RootedRestartStages.reference_next_four_warm line 85
def OAI.ContingencyTables.RootedRestartStages.implemented line 97
theorem OAI.ContingencyTables.RootedRestartStages.implemented_distance line 110
Source documentation
Every new stage starts from a four-warm exact reference. Errors of the actual bounded-word implementation add, without conditioning on a successful return or requiring its incoming distribution to be warm.
```
theorem implemented_distance (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (C : ℕ) (hC : 0 < C) (K H L k n : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
    (hB : (K:ℝ)=CompanionOracleDensity.binWidth A C)
    (hH : H ≤ CompanionOracleDensity.rationalHeight A C)
    (hbox : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1)) ≤ (2:ℝ)^L)
    (xi : ℚ) (hx0 : 0 < xi) (hx1 : xi ≤ 1/4)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (CompanionOracleDensity.dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger
      (Grid (I := Fin (CompanionOracleDensity.dimension A)) K))
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.CompanionOracleDensity.binWidth, OAI.ContingencyTables.CompanionOracleDensity.rationalHeight, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.CompanionOracleDensity.dimension, OAI.ContingencyTables.PublishedInputs.FiniteCheeger