Quantiles.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Finite quantiles for the fourth-moment gap

The lower and upper quantile choices in the proof of phase:quantile-gap, §7. Weights are listed in increasing frequency order. No uniform measure on the frequency list is assumed.

def OAI.LipschitzHilbert.prefixMass line 23
theorem OAI.LipschitzHilbert.prefixMass_succ line 25
theorem OAI.LipschitzHilbert.prefixMass_mono line 28
theorem OAI.LipschitzHilbert.exists_first_crossing line 36
Source documentation
The first cumulative crossing has an atom on its right and a strict inequality immediately to its left.
```
theorem exists_first_crossing (w : ℕ → ℝ) (N : ℕ) {t : ℝ}
    (ht : 0 < t) (htN : t ≤ prefixMass w N) :
    ∃ a < N, prefixMass w a < t ∧ t ≤ prefixMass w (a + 1) := by
…
```
Mentions: OAI.LipschitzHilbert.prefixMass

theorem OAI.LipschitzHilbert.exists_distinct_quantiles line 55

Source documentation

Nonconcentration of single atoms forces the two quarter-tail quantiles to be distinct. The inequalities also bound the mass outside their interval.

theorem exists_distinct_quantiles (w : ℕ → ℝ) (N : ℕ) {κ : ℝ}
    (hκ : 0 < κ) (hκ1 : κ < 1) (hw : ∀ i, 0 ≤ w i)
    (htotal : prefixMass w N = 1) (hatom : ∀ i < N, w i ≤ 1 - κ) :
    ∃ a b : ℕ, a < b ∧ b < N ∧
      prefixMass w a < κ / 4 ∧ κ / 4 ≤ prefixMass w (a + 1) ∧
      prefixMass w b < 1 - κ / 4 ∧ 1 - κ / 4 ≤ prefixMass w (b + 1) ∧
      1 - κ / 2 ≤ prefixMass w (b + 1) - prefixMass w a := by
…

Mentions: OAI.LipschitzHilbert.prefixMass

def OAI.LipschitzHilbert.intervalMass line 77

Source documentation

The mass of a closed frequency interval.

noncomputable def intervalMass {ι : Type*} [Fintype ι] (w frequency : ι → ℝ)
    (a b : ℝ) : ℝ := by
…

theorem OAI.LipschitzHilbert.intervalMass_le_halves line 84

Source documentation

The two closed halves cover the closed interval; midpoint atoms may be counted twice, which has the favorable sign.

theorem intervalMass_le_halves {ι : Type*} [Fintype ι]
    (w frequency : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (a b : ℝ) :
    intervalMass w frequency a b ≤ intervalMass w frequency a ((a + b) / 2) +
      intervalMass w frequency ((a + b) / 2) b := by
…

Mentions: OAI.LipschitzHilbert.intervalMass

theorem OAI.LipschitzHilbert.exists_heavy_half line 103

Source documentation

One half of a frequency interval carries at least half its mass.

theorem exists_heavy_half {ι : Type*} [Fintype ι]
    (w frequency : ι → ℝ) (hw : ∀ i, 0 ≤ w i) {a b m : ℝ}
    (hab : a ≤ b) (hm : m ≤ intervalMass w frequency a b) :
    ∃ e h : ℝ, a ≤ e ∧ e ≤ h ∧ h ≤ b ∧
      h - e = (b - a) / 2 ∧ m / 2 ≤ intervalMass w frequency e h := by
…

Mentions: OAI.LipschitzHilbert.intervalMass