FiniteSupportVariance.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing zero-weight states preserves finite weighted variance

theorem OAI.ContingencyTables.FiniteExposureVariance.sum_support_embedding line 14

Source documentation

An injective encoding may omit only states of weight zero.

theorem sum_support_embedding (e : X → Y) (he : Function.Injective e)
    (w : Y → ℝ) (hw : ∀ y ∉ Set.range e,w y=0) (H : Y → ℝ) :
    (∑ x,w (e x)*H (e x))=∑ y,w y*H y := by
…

theorem OAI.ContingencyTables.FiniteExposureVariance.mean_support_embedding line 23
theorem OAI.ContingencyTables.FiniteExposureVariance.variance_support_embedding line 31
theorem OAI.ContingencyTables.FiniteExposureVariance.variance_positive_support line 41
Source documentation
In particular, restriction to the strictly positive support does not change any weighted variance, including the empty-support case.
```
theorem variance_positive_support (w H : X → ℝ) (hw : ∀ x,0 ≤ w x) :
    variance (fun x : {x // 0 < w x} => w x.val)
      (fun x => H x.val)=variance w H := by
…
```
Mentions: OAI.ContingencyTables.FiniteExposureVariance.variance