Quantiles of finite labelled laws

A probability measure on a finite type becomes a finitely supported real law after assigning a real label to every outcome. This file characterizes its quantiles directly from the mass below and at a proposed label. The characterization automatically sorts the distinct labels and aggregates outcomes carrying equal labels.

For any real probability law carried by a finite set, an interior quantile belongs to that set and is its least cumulative crossing. A finite minimum therefore computes it. The lower (upper) endpoint limit is the smallest (largest) candidate whenever that candidate has positive mass.

Main results

• MeasureTheory.Measure.quantile_eq_min'_of_ae_mem_finset computes a quantile by a finite minimum over a carrying set;

• MeasureTheory.Measure.tendsto_quantile_nhdsGT_zero_of_ae_mem_finset and MeasureTheory.Measure.tendsto_quantile_nhdsLT_one_of_ae_mem_finset give its endpoint limits;

• MeasureTheory.Measure.quantile_map_finite_eq_iff characterizes the quantile by the strict cumulative crossing below a label and the weak crossing at it;

• MeasureTheory.Measure.tendsto_quantile_map_finite_nhdsGT_zero and MeasureTheory.Measure.tendsto_quantile_map_finite_nhdsLT_one give the endpoint limits at the least and greatest labels of positive mass.

theorem MeasureTheory.Measure.quantile_mem_finset (μ : Measure ℝ) [IsProbabilityMeasure μ] {s : Finset ℝ} {u : ℝ} (hs : ∀ᵐ (y : ℝ) ∂μ, y ∈ s) (hu : u ∈ Set.Ioo 0 1) : μ.quantile u ∈ s

An interior quantile of a law carried by a finite set belongs to that set. The set may include points of zero mass.

theorem MeasureTheory.Measure.quantile_eq_iff_of_ae_mem_finset (μ : Measure ℝ) [IsProbabilityMeasure μ] {s : Finset ℝ} {u x : ℝ} (hs : ∀ᵐ (y : ℝ) ∂μ, y ∈ s) (hu : u ∈ Set.Ioo 0 1) : μ.quantile u = x ↔ IsLeast {y : ℝ | y ∈ s ∧ u ≤ ↑(ProbabilityTheory.cdf μ) y} x

The quantile is characterized by the least cumulative crossing among a finite set carrying the law, including levels equal to a cumulative mass.

theorem MeasureTheory.Measure.nonempty_filter_le_cdf (μ : Measure ℝ) [IsProbabilityMeasure μ] {s : Finset ℝ} {u : ℝ} (hs : ∀ᵐ (y : ℝ) ∂μ, y ∈ s) (hu : u ∈ Set.Ioo 0 1) : {y ∈ s | u ≤ ↑(ProbabilityTheory.cdf μ) y}.Nonempty

The finite set of cumulative crossings at an interior level is nonempty.

theorem MeasureTheory.Measure.quantile_eq_min'_of_ae_mem_finset (μ : Measure ℝ) [IsProbabilityMeasure μ] {s : Finset ℝ} {u : ℝ} (hs : ∀ᵐ (y : ℝ) ∂μ, y ∈ s) (hu : u ∈ Set.Ioo 0 1) : μ.quantile u = {y ∈ s | u ≤ ↑(ProbabilityTheory.cdf μ) y}.min' ⋯

A finite minimum computes an interior quantile.

theorem MeasureTheory.Measure.tendsto_quantile_nhdsGT_zero_of_ae_mem_finset (μ : Measure ℝ) [IsProbabilityMeasure μ] {s : Finset ℝ} (hs : ∀ᵐ (y : ℝ) ∂μ, y ∈ s) (hne : s.Nonempty) (hpos : μ {s.min' hne} ≠ 0) : Filter.Tendsto (fun (u : ℝ) => ↑(μ.quantile u)) (nhdsWithin 0 (Set.Ioi 0)) (nhds ↑(s.min' hne))

For a finite carrying set whose smallest point has positive mass, the lower endpoint limit is that point.

theorem MeasureTheory.Measure.tendsto_quantile_nhdsLT_one_of_ae_mem_finset (μ : Measure ℝ) [IsProbabilityMeasure μ] {s : Finset ℝ} (hs : ∀ᵐ (y : ℝ) ∂μ, y ∈ s) (hne : s.Nonempty) (hpos : μ {s.max' hne} ≠ 0) : Filter.Tendsto (fun (u : ℝ) => ↑(μ.quantile u)) (nhdsWithin 1 (Set.Iio 1)) (nhds ↑(s.max' hne))

For a finite carrying set whose largest point has positive mass, the upper endpoint limit is that point.

@[simp]

theorem MeasureTheory.Measure.quantile_map_finite_eq_iff {I : Type u_1} [Finite I] [MeasurableSpace I] [MeasurableSingletonClass I] (μ : Measure I) [IsProbabilityMeasure μ] (label : I → ℝ) {u x : ℝ} (hu : u ∈ Set.Ioo 0 1) : (map label μ).quantile u = x ↔ μ.real (label ⁻¹' Set.Iio x) < u ∧ u ≤ μ.real (label ⁻¹' Set.Iic x)

A real number is the interior quantile of a probability measure on a finite labelled type exactly when the level lies strictly above the mass below that label and at most the mass at or below it. In particular, the strict inequality forces the answer to be one of the supplied labels with positive total mass.

theorem MeasureTheory.Measure.tendsto_quantile_map_finite_nhdsGT_zero {I : Type u_1} [Finite I] [MeasurableSpace I] [MeasurableSingletonClass I] (μ : Measure I) [IsProbabilityMeasure μ] (label : I → ℝ) (i : I) (hi : 0 < μ.real {i}) (hmin : ∀ (j : I), 0 < μ.real {j} → label i ≤ label j) : Filter.Tendsto (map label μ).quantile (nhdsWithin 0 (Set.Ioi 0)) (nhds (label i))

For a finite labelled law, quantiles tend to any least label of positive mass as the level tends to zero from above. Labels of zero mass do not affect the endpoint.

theorem MeasureTheory.Measure.tendsto_quantile_map_finite_nhdsLT_one {I : Type u_1} [Finite I] [MeasurableSpace I] (μ : Measure I) [IsProbabilityMeasure μ] [MeasurableSingletonClass I] (label : I → ℝ) (i : I) (hi : 0 < μ.real {i}) (hmax : ∀ (j : I), 0 < μ.real {j} → label j ≤ label i) : Filter.Tendsto (map label μ).quantile (nhdsWithin 1 (Set.Iio 1)) (nhds (label i))

For a finite labelled law, quantiles tend to any greatest label of positive mass as the level tends to one from below. Labels of zero mass do not affect the endpoint.