OAI/Combinatorics/ContingencyTables/Rooted/RootedCountingSchedule.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedCountingSchedule.settings line 23

   Source documentation

   Only natural/rational arithmetic selects the phase precision and all finite loops. The supplied grid point is the evaluator's fixed start.

   def settings (A : Instance I J) (C K H L : ℕ)
       (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (epsilon : ℚ)
       (v : Grid (I := Fin (dimension A)) K) : Settings A :=
   …

2. lemma OAI.ContingencyTables.RootedCountingSchedule.settings_positive line 34
3. lemma OAI.ContingencyTables.RootedCountingSchedule.observable_cast line 46
4. lemma OAI.ContingencyTables.RootedCountingSchedule.error_bound line 52
5. lemma OAI.ContingencyTables.RootedCountingSchedule.total_error_bound line 83
6. lemma OAI.ContingencyTables.RootedCountingSchedule.logarithmic_bound line 94
7. theorem OAI.ContingencyTables.RootedCountingSchedule.constant_success line 105

   Source documentation

   Constant success for the actual finite Boolean estimator. The binary confidence parameter is handled by independent medians afterward.

   theorem constant_success (A : Instance I J) (R : RootedCompletion.Selection A.T)
       (C K H L : ℕ) (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W)
       (epsilon : ℚ) (he0 : 0 < epsilon) (he1 : epsilon < 1)
       (v : Grid (I := Fin (dimension A)) K) (E : Endpoints A)
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection