OAI/Combinatorics/ContingencyTables/Rooted/RootedHistoryStep.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedHistoryStep.default_failure line 20
2. def OAI.ContingencyTables.RootedHistoryStep.error line 29
3. lemma OAI.ContingencyTables.RootedHistoryStep.error_mono line 39
4. theorem OAI.ContingencyTables.RootedHistoryStep.step_failure line 51

   Source documentation

   On each good past history, the actual next stored value fails the source update conditions with the proved common error bound.

   theorem step_failure (A : Instance I J) (R : RootedCompletion.Selection A.T) (s : Settings A)
       (hC : 0 < s.C) (hB : (s.K:ℝ)=binWidth A s.C)
       (hH : s.H ≤ rationalHeight A s.C)
       (hbox : (∏ a : SmallCell A,((A.b a.val.1 a.val.2:ℝ)+1)) ≤ (2:ℝ)^s.L)
       (hx0 : 0 < s.xi) (hx1 : s.xi ≤ 1/4)
       (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
       (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) s.K))
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger