OAI/Combinatorics/ContingencyTables/Rooted/RootedPhaseAccuracy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Actual selected-root guarded rational phase update and logarithmic error

  1. lemma OAI.ContingencyTables.RootedPhaseAccuracy.indicator_sum line 17
  2. lemma OAI.ContingencyTables.RootedPhaseAccuracy.count_positive_of_empirical line 24
  3. theorem OAI.ContingencyTables.RootedPhaseAccuracy.accurate_counts_positive line 35
  4. theorem OAI.ContingencyTables.RootedPhaseAccuracy.observed_ratio_error line 58
  5. theorem OAI.ContingencyTables.RootedPhaseAccuracy.update_success line 95

    Source documentation

    The actual guarded rational update succeeds on the proved accuracy events; its stored multipliers are good for the next literal weight.

    theorem update_success (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j N : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ) (hx0 : 0≤xi) (hx1 : xi≤1/4)
    (v : Grid (I := Fin (dimension A)) K) (old : Stored A)
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection