RootedMultiplierUpdate.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Selected-root empirical multiplier and counting updates

The observables and empirical counts are those of the actual labelled chain. The update cancels the preceding multiplier, and the next-parameter comparison is derived from the literal bounded forest penalty.

def OAI.ContingencyTables.RootedMultiplierUpdate.ratio line 21
lemma OAI.ContingencyTables.RootedMultiplierUpdate.ratio_bounds line 24
lemma OAI.ContingencyTables.RootedMultiplierUpdate.ratio_mean line 32

theorem OAI.ContingencyTables.RootedMultiplierUpdate.successful_phase_learns line 45

Source documentation

The explicit observed-type-count update gives good multipliers for j+1. Its only statistical hypothesis is relative accuracy of the actual finite observations at phase j.

theorem successful_phase_learns (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ)
    (w : ((Labels A×Bool)×(Labels A×Bool)) → ((Labels A×Bool)×(Labels A×Bool)) → ℝ)
    (hw : ∀ p r,0< w p r) (eta : ℝ) (he0 : 0≤ eta) (he : eta≤1/4)
    (l : List (Set (Labels A×Bool)))
    (hacc : AccuratePhase pairs w (weight A R j) (ratio A R j) eta l) :
    GoodMultipliers pairs (weight A R (j+1)) (learnedMultipliers pairs w l) := by
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedMultiplierUpdate.ratio

theorem OAI.ContingencyTables.RootedMultiplierUpdate.successful_phase_ratio_log line 93

Source documentation

Relative accuracy of the actual counting and plain observations bounds one logarithmic counting-ratio error by 4 eta.

theorem successful_phase_ratio_log (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ)
    (w : ((Labels A×Bool)×(Labels A×Bool)) → ((Labels A×Bool)×(Labels A×Bool)) → ℝ)
    (hw : ∀ p r,0< w p r) (eta : ℝ) (he0 : 0≤ eta) (he : eta≤1/4)
    (l : List (Set (Labels A×Bool)))
    (hacc : AccuratePhase pairs w (weight A R j) (ratio A R j) eta l) :
    |Real.log (empiricalRatio pairs (ratio A R j) l/
      (slotTotal pairs (weight A R (j+1)) ∅/slotTotal pairs (weight A R j) ∅))|≤4*eta := by
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedMultiplierUpdate.ratio