Quantiles of labeled categorical laws

Real labels need neither be distinct nor respect an order on categories. The mass of a label adds all the weights in its fibre. Quantiles are finite cumulative crossings among the distinct positive-weight labels, and their endpoint limits are the smallest and largest such labels.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Discrete Multivariate Distributions, Wiley, 1997, Chapter 35.

theorem Convexity.StdSimplex.quantile_map_categoricalMeasure_eq_iff {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : StdSimplex NNReal I) (label : I → ℝ) {u x : ℝ} (hu : u ∈ Set.Ioo 0 1) : (MeasureTheory.Measure.map label (TauCeti.Probability.categoricalMeasure p)).quantile u = x ↔ ∑ i : I with label i < x, ↑(p.weights i) < u ∧ u ≤ ∑ i : I with label i ≤ x, ↑(p.weights i)

A real number is the quantile of a categorical law with supplied real labels exactly when the level strictly exceeds the total weight of smaller labels and is at most the total weight of labels no larger than it. This sorts distinct labels and aggregates equal labels automatically.

theorem Convexity.StdSimplex.tendsto_quantile_map_categoricalMeasure_nhdsGT_zero {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : StdSimplex NNReal I) (label : I → ℝ) (i : I) (hi : 0 < ↑(p.weights i)) (hmin : ∀ (j : I), 0 < ↑(p.weights j) → label i ≤ label j) : Filter.Tendsto (MeasureTheory.Measure.map label (TauCeti.Probability.categoricalMeasure p)).quantile (nhdsWithin 0 (Set.Ioi 0)) (nhds (label i))

As the level tends to zero from above, categorical quantiles tend to any least label whose category has positive weight. Zero-weight categories do not affect the endpoint.

theorem Convexity.StdSimplex.tendsto_quantile_map_categoricalMeasure_nhdsLT_one {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : StdSimplex NNReal I) (label : I → ℝ) (i : I) (hi : 0 < ↑(p.weights i)) (hmax : ∀ (j : I), 0 < ↑(p.weights j) → label j ≤ label i) : Filter.Tendsto (MeasureTheory.Measure.map label (TauCeti.Probability.categoricalMeasure p)).quantile (nhdsWithin 1 (Set.Iio 1)) (nhds (label i))

As the level tends to one from below, categorical quantiles tend to any greatest label whose category has positive weight. Zero-weight categories do not affect the endpoint.

theorem Convexity.StdSimplex.quantile_map_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : StdSimplex NNReal I) (f : I → ℝ) {u : ℝ} (hu : u ∈ Set.Ioo 0 1) : (MeasureTheory.Measure.map f (TauCeti.Probability.categoricalMeasure p)).quantile u = {y ∈ Finset.image f p.support | u ≤ ∑ i : I with f i ≤ y, ↑(p.weights i)}.min' ⋯

Compute a categorical quantile by taking the minimum of the distinct positive-weight labels whose cumulative weight reaches the level.