TerminalMassCover.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Finite mass accounting for the terminal far and near regions

theorem OAI.ContingencyTables.TerminalMassCover.mass_le_cover line 19

Source documentation

A finite union estimate retaining the feasible unit summands exactly. The application proves the cover from the original root and tree penalties.

theorem mass_le_cover (w : X → ℝ) (feasible far : X → Prop) (near : C → X → Prop)
    (hw : ∀ x,0 ≤ w x) (hunit : ∀ x,feasible x → w x=1)
    (hcover : ∀ x,0 < w x → ¬feasible x → far x ∨ ∃ c,near c x) :
    (∑ x,w x) ≤ (∑ x,if feasible x then (1:ℝ) else 0)+
      (∑ x,if far x then w x else 0)+∑ c,∑ x,if near c x then w x else 0 := by
…

theorem OAI.ContingencyTables.TerminalMassCover.relative_count_bound line 55
Source documentation
The manuscript's final conversion from a small fraction of the normalizer to a relative error against the exact table count.
```
theorem relative_count_bound (Z M epsilon : ℝ) (hZ : 0 ≤ Z)
    (he : 0 < epsilon) (he1 : epsilon < 1) (hZM : Z ≤ M)
    (hbad : M ≤ Z+(epsilon/64)*M) :
    Z ≤ M ∧ M ≤ (1+epsilon/32)*Z := by
…
```