Lower tails of a finite distribution

A lower tail of mass δ contains every point strictly below its cutoff and no point strictly above it. Fractional inclusion of the points at the cutoff gives exactly the requested mass, even when the distribution has atoms or unequal probabilities.

The cutoff is an analysis witness. Existence does not assert that a program can compute a distribution's quantile, and it supplies no computational advice.

Main results

• Cslib.Probability.PMF.exists_quantile: bracket a prescribed mass by a score cutoff.
• Cslib.Probability.PMF.exists_lowerTail: fill the cutoff level fractionally to attain that mass.

References

[Hol05], Lemma 2.4 and Claim 2.15, uses the lower tail in hard-core boosting. Fractional boundary weights extend prescribed-cardinality subsets to arbitrary finite distributions. Adapted from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Probability.PMF.exists_quantile {α : Type u_1} [Fintype α] (source : PMF α) (score : α → ℝ) {δ : ℝ} (hδ : 0 ≤ δ) (hδone : δ ≤ 1) : ∃ cutoff ∈ Set.range score, (∑ x : α, if score x < cutoff then (source x).toReal else 0) ≤ δ ∧ δ ≤ ∑ x : α, if score x ≤ cutoff then (source x).toReal else 0

A finite score distribution has a cutoff bracketing every probability level.

theorem Cslib.Probability.PMF.exists_lowerTail {α : Type u_1} [Fintype α] (source : PMF α) (score : α → ℝ) {δ : ℝ} (hδ : 0 ≤ δ) (hδone : δ ≤ 1) : ∃ cutoff ∈ Set.range score, ∃ (softSet : α → ℝ), (∀ (x : α), softSet x ∈ Set.Icc 0 1) ∧ (∀ (x : α), score x < cutoff → softSet x = 1) ∧ (∀ (x : α), cutoff < score x → softSet x = 0) ∧ ∑ x : α, (source x).toReal * softSet x = δ

A lower tail has the prescribed mass, filling only the boundary level fractionally.