AnnealingMultipliers.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The companion's multiplier update from empirical type counts

The old multiplier cancels from the update relative to the current ideal multiplier. Relative accuracy of two positive type means, followed by the proved adjacent-parameter factor two, gives the required factor four at the next parameter. This is deterministic algebra of the actual update.

theorem OAI.ContingencyTables.AnnealingMultipliers.empirical_positive line 18

theorem OAI.ContingencyTables.AnnealingMultipliers.relative_ratio line 24

Source documentation

The normalized ratio of two empirically observed positive means.

theorem relative_ratio (hp : 0<p) (hq : 0<q) (he0 : 0≤eta) (he : eta≤1/4)
    (hph : (1-eta)*p≤ph ∧ ph≤(1+eta)*p)
    (hqh : (1-eta)*q≤qh ∧ qh≤(1+eta)*q) :
    0<ph*q/(qh*p) ∧
      1/2≤ph*q/(qh*p) ∧ ph*q/(qh*p)≤2 ∧
      |Real.log (ph*q/(qh*p))|≤4*eta := by
…

theorem OAI.ContingencyTables.AnnealingMultipliers.update_good line 68

Source documentation

The concrete update w*(observed plain count)/(observed defect count) is good for the next parameter. Earlier multiplier errors do not compound.

theorem update_good (hp : 0<p) (hq : 0<q) (hw : 0<w)
    (he0 : 0≤eta) (he : eta≤1/4)
    (hph : (1-eta)*p≤ph ∧ ph≤(1+eta)*p)
    (hqh : (1-eta)*q≤qh ∧ qh≤(1+eta)*q)
    (hideal : w*p/q=ideal)
    (hnext : ideal/2≤nextIdeal ∧ nextIdeal≤2*ideal) :
    nextIdeal/4≤w*ph/qh ∧ w*ph/qh≤4*nextIdeal := by
…