OAI/Combinatorics/ContingencyTables/Rooted/RootedStoredEstimate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedStoredEstimate.initialTotal line 22
2. def OAI.ContingencyTables.RootedStoredEstimate.initialStored line 26
3. lemma OAI.ContingencyTables.RootedStoredEstimate.initialTotal_cast line 29
4. lemma OAI.ContingencyTables.RootedStoredEstimate.initialStored_positive line 35
5. lemma OAI.ContingencyTables.RootedStoredEstimate.initialStored_good line 44
6. theorem OAI.ContingencyTables.RootedStoredEstimate.stored_log_error line 57

   Source documentation

   The actual rational estimates telescope through their proved per-phase multiplicative errors, including every weight-oracle error.

   theorem stored_log_error (A : Instance I J) (R : RootedCompletion.Selection A.T)
       (stored : ℕ → Stored A) (hinit : stored 0=initialStored A)
       (xi : ℚ) (eta : ℝ) (H : ℕ)
       (hstep : ∀ j,j < H → ValidOutput A R j (stored j) xi eta (stored (j+1))) :
       0 < (stored H).estimate ∧
         |Real.log (((stored H).estimate:ℝ)/total A R H)| ≤
           (H:ℝ)*(4*(xi:ℝ)+4*eta) := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedStoredEstimate.initialStored

7. theorem OAI.ContingencyTables.RootedStoredEstimate.stored_count_accuracy line 96