FrequencyQuantiles.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Quarter-tail quantiles in a finite ordered frequency list.

def OAI.LipschitzHilbert.extendWeights line 16
Source documentation
Extend finite weights by zero, only to use natural-number prefix sums.
```
def extendWeights {N : ℕ} (x : Fin N → ℝ) (i : ℕ) : ℝ :=
…
```
theorem OAI.LipschitzHilbert.extendWeights_nonneg line 19
theorem OAI.LipschitzHilbert.prefixMass_extend line 25

theorem OAI.LipschitzHilbert.finite_frequency_quantiles line 43

Source documentation

Quarter-tail quantiles for strictly ordered frequencies.

theorem finite_frequency_quantiles {N : ℕ} (x frequency : Fin N → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1)
    (hfrequency : StrictMono frequency) {κ : ℝ}
    (hκ : 0 < κ) (hκ1 : κ < 1) (hatom : ∀ i, x i ≤ 1 - κ) :
    ∃ a b : Fin N, a < b ∧
      κ / 4 ≤ (∑ i, if frequency i ≤ frequency a then x i else 0) ∧
      κ / 4 ≤ (∑ i, if frequency b ≤ frequency i then x i else 0) ∧
      1 - κ / 2 ≤ intervalMass x frequency (frequency a) (frequency b) := by
…

Mentions: OAI.LipschitzHilbert.intervalMass

theorem OAI.LipschitzHilbert.frequency_quantiles line 108

Source documentation

Sorting by the injective frequency map removes the ordering hypothesis from the finite quantile construction.

theorem frequency_quantiles {ι : Type*} [Fintype ι] (x frequency : ι → ℝ)
    (hx : ∀ i, 0 ≤ x i) (hsum : ∑ i, x i = 1)
    (hinj : Function.Injective frequency) {κ : ℝ}
    (hκ : 0 < κ) (hκ1 : κ < 1) (hatom : ∀ i, x i ≤ 1 - κ) :
    ∃ a b : ι, frequency a < frequency b ∧
      κ / 4 ≤ (∑ i, if frequency i ≤ frequency a then x i else 0) ∧
      κ / 4 ≤ (∑ i, if frequency b ≤ frequency i then x i else 0) ∧
      1 - κ / 2 ≤ intervalMass x frequency (frequency a) (frequency b) := by
…

Mentions: OAI.LipschitzHilbert.intervalMass