OAI/Combinatorics/ContingencyTables/Rooted/RootedHistoryConfidence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedHistoryConfidence.success_of_failure line 18
2. def OAI.ContingencyTables.RootedHistoryConfidence.GoodWords line 32
3. lemma OAI.ContingencyTables.RootedHistoryConfidence.error_nonnegative line 36
4. theorem OAI.ContingencyTables.RootedHistoryConfidence.history_success line 44

   Source documentation

   Each conditional probability is proved from the actual finite-word phase; independent word histories then accumulate these losses.

   theorem history_success (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