FiniteExposureVariance.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite exposure variance with zero-mass children

The exact variance decomposition uses only finite nonnegative weights. A child of mass zero has zero moment, so its mean can be set to zero. This is the algebraic decomposition iterated by the small-slot exposure.

def OAI.ContingencyTables.FiniteExposureVariance.mean line 19
def OAI.ContingencyTables.FiniteExposureVariance.variance line 21
lemma OAI.ContingencyTables.FiniteExposureVariance.zero_mass_weights line 24
lemma OAI.ContingencyTables.FiniteExposureVariance.mean_moment line 30
lemma OAI.ContingencyTables.FiniteExposureVariance.mean_second line 39
lemma OAI.ContingencyTables.FiniteExposureVariance.variance_formula line 48
Source documentation
The second-moment identity also holds at mass zero.
```
lemma variance_formula (w H : X → ℝ) (hw : ∀ x, 0 ≤ w x) :
    variance w H=(∑ x, w x*(H x)^2)-(∑ x, w x*H x)^2/(∑ x, w x) := by
…
```
Mentions: OAI.ContingencyTables.FiniteExposureVariance.variance
theorem OAI.ContingencyTables.FiniteExposureVariance.variance_split line 58
Source documentation
Exact conditional variance decomposition, allowing arbitrary zero-mass child fibres and a zero-mass whole space.
```
theorem variance_split (w H : Y → X → ℝ) (hw : ∀ y x, 0 ≤ w y x) :
    variance (fun p : X×Y => w p.2 p.1) (fun p => H p.2 p.1)=
      (∑ y, variance (w y) (H y))+
        variance (fun y => ∑ x, w y x) (fun y => mean (w y) (H y)) := by
…
```
Mentions: OAI.ContingencyTables.FiniteExposureVariance.variance, OAI.ContingencyTables.FiniteExposureVariance.mean

theorem OAI.ContingencyTables.FiniteExposureVariance.sum_context_energy_le line 85

Source documentation

A fixed-depth partition uses each nonnegative edge energy at most once. The same statement applies to profile contexts and directed edges.

theorem sum_context_energy_le {E C : Type*} [Fintype C]
    (edges : Finset E) (energy : E → ℝ) (context : E → C)
    (eligible : E → Prop) (henergy : ∀ e ∈ edges, 0 ≤ energy e) :
    (∑ c : C, ∑ e ∈ edges.filter (fun e => eligible e ∧ context e=c), energy e) ≤
      ∑ e ∈ edges, energy e := by
…