Hellinger.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The finite probability estimate in the phase argument

This is the Hellinger-affinity calculation in §7, proof of phase:quantile-gap, of A uniform Hilbert transform estimate for Lipschitz directions. The finite probability calculation is proved directly.

def OAI.LipschitzHilbert.affinity line 21
Source documentation
Hellinger affinity of finite probability weights.
```
noncomputable def affinity {ι : Type*} [Fintype ι] (p q : ι → ℝ) : ℝ :=
…
```

theorem OAI.LipschitzHilbert.l1_sq_le_affinity line 25

Source documentation

Squared total variation estimate, before division of the ℓ¹ distance by two.

theorem l1_sq_le_affinity {ι : Type*} [Fintype ι]
    (p q : ι → ℝ) (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
    (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i = 1) :
    (∑ i, |p i - q i|) ^ 2 ≤ 4 * (1 - affinity p q ^ 2) := by
…

Mentions: OAI.LipschitzHilbert.affinity

theorem OAI.LipschitzHilbert.event_deficit_le_l1_half line 64

Source documentation

Each event deficit is at most the total variation distance.

theorem event_deficit_le_l1_half {ι : Type*} [Fintype ι]
    (p q : ι → ℝ) (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i = 1)
    (s : Finset ι) :
    2 * |∑ i ∈ s, (p i - q i)| ≤ ∑ i, |p i - q i| := by
…

theorem OAI.LipschitzHilbert.event_deficit_sq_le_one_sub_affinity_sq line 84

Source documentation

The event estimate used to turn a quantile deficit into a fourth-moment gap.

theorem event_deficit_sq_le_one_sub_affinity_sq {ι : Type*} [Fintype ι]
    (p q : ι → ℝ) (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
    (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i = 1) (s : Finset ι) :
    (∑ i ∈ s, (p i - q i)) ^ 2 ≤ 1 - affinity p q ^ 2 := by
…

Mentions: OAI.LipschitzHilbert.affinity

theorem OAI.LipschitzHilbert.subprobability_event_deficit_sq line 98
Source documentation
The completed triple law may have mass less than one. Adjoining its missing mass at one point, where the independent law has mass zero, preserves affinity.
```
theorem subprobability_event_deficit_sq {ι : Type*} [Fintype ι]
    (p q : ι → ℝ) (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
    (hp1 : ∑ i, p i ≤ 1) (hq1 : ∑ i, q i = 1) (s : Finset ι) :
    (∑ i ∈ s, (q i - p i)) ^ 2 ≤ 1 - affinity p q ^ 2 := by
…
```
Mentions: OAI.LipschitzHilbert.affinity

theorem OAI.LipschitzHilbert.strict_gap_of_event_deficit line 132

Source documentation

A definite event deficit forces the strict fourth-moment gain. This is the last algebraic step of the manuscript's quantile-gap argument.

theorem strict_gap_of_event_deficit {ι : Type*} [Fintype ι]
    (p q : ι → ℝ) (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 ≤ q i)
    (hp1 : ∑ i, p i ≤ 1) (hq1 : ∑ i, q i = 1) (s : Finset ι)
    {Q g : ℝ} (hQ : 0 ≤ Q) (hg : 0 ≤ g)
    (hgain : Q ^ 2 ≤ affinity p q)
    (hdeficit : g ≤ ∑ i ∈ s, (q i - p i)) :
    Q ≤ 1 - g ^ 2 / 4 := by
…

Mentions: OAI.LipschitzHilbert.affinity