OAI/Combinatorics/ContingencyTables/Rooted/RootedCountingWords.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedCountingWords.estimate line 20
2. lemma OAI.ContingencyTables.RootedCountingWords.estimate_accurate line 24
3. theorem OAI.ContingencyTables.RootedCountingWords.accuracy line 41

   Source documentation

   The actual stored rational value has the stated error probability. No equality to an ideal empirical-ratio estimator is assumed.

   theorem accuracy (A : Instance I J) (R : RootedCompletion.Selection A.T) (s : Settings A)
       (E : Endpoints A) (epsilon : ℝ) (he0 : 0 < epsilon) (he1 : epsilon < 1)
       (hW : 20*A.d ≤ A.W) (hL : (∏ a : I×J,(A.b a.1 a.2+1)) ≤ 2^s.L)
       (hfinal : s.H=finalPhase A s.L epsilon)
       (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

4. def OAI.ContingencyTables.RootedCountingWords.bitCount line 68
5. def OAI.ContingencyTables.RootedCountingWords.flatEstimate line 70
6. lemma OAI.ContingencyTables.RootedCountingWords.flatEstimate_law line 74