CompanionMultiplierUpdate.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual companion 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.CompanionMultiplierUpdate.ratio line 21
lemma OAI.ContingencyTables.CompanionMultiplierUpdate.ratio_bounds line 24
lemma OAI.ContingencyTables.CompanionMultiplierUpdate.ratio_mean line 32

theorem OAI.ContingencyTables.CompanionMultiplierUpdate.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) (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 j) (ratio A j) eta l) :
    GoodMultipliers pairs (weight A (j+1)) (learnedMultipliers pairs w l) := by
…

Mentions: OAI.ContingencyTables.CompanionMultiplierUpdate.ratio

theorem OAI.ContingencyTables.CompanionMultiplierUpdate.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) (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 j) (ratio A j) eta l) :
    |Real.log (empiricalRatio pairs (ratio A j) l/
      (slotTotal pairs (weight A (j+1)) ∅/slotTotal pairs (weight A j) ∅))|≤4*eta := by
…

Mentions: OAI.ContingencyTables.CompanionMultiplierUpdate.ratio