Categorical distributions

A probability vector p : Convexity.StdSimplex ℝ≥0 ι determines the categorical law on ι by assigning mass p.weights i to each category i. This file gives the measure-level definition, its singleton masses and finite-sum integration formula, and measurability in the probability vector.

With the coordinate topology on the finite simplex, the categorical law is weakly continuous on the full simplex, including zero weights.

Categorical laws are functorial in the category type: mapping categories along f : ι → κ adds the weights over the fibres of f, exactly as Convexity.StdSimplex.map does. Encoding a category i by the one-hot count vector Pi.single i 1 identifies the categorical law with the one-trial multinomial law. These facts make categorical measures usable as finite mixing laws and connect them to the existing multinomial API.

For labels in a measurable space, measurable-set masses sum the weights over the corresponding fibres, including repeated labels. With measurable singletons, the positive-weight labels form a finite carrying set, each of whose points has nonzero mass. For real labels, the cdf gives the corresponding cumulative sum. Quantile formulas and endpoint limits are in TauCeti.Probability.Distributions.Categorical.Quantile.

Main results

• TauCeti.Probability.categoricalMeasure is the weighted sum of Dirac measures;
• TauCeti.Probability.categoricalMeasure_singleton gives its masses;
• TauCeti.Probability.integral_categoricalMeasure evaluates integrals as finite weighted sums;
• TauCeti.Probability.measurable_categoricalMeasure proves parameter measurability;
• TauCeti.Probability.continuous_categoricalMeasure proves weak continuity on the full simplex, including zero weights;
• TauCeti.Probability.map_categoricalMeasure aggregates categories;
• TauCeti.Probability.map_piSingle_categoricalMeasure identifies one-hot encoding with a one-trial multinomial law;
• Convexity.StdSimplex.cdf_map_categoricalMeasure gives cumulative label weights;
• Convexity.StdSimplex.ae_mem_image_support_map_categoricalMeasure gives a finite carrying set.

References

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

noncomputable def TauCeti.Probability.categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] (p : Convexity.StdSimplex NNReal I) : MeasureTheory.Measure I

The categorical law with probability vector p is the corresponding finite weighted sum of Dirac measures.

theorem TauCeti.Probability.categoricalMeasure_def {I : Type u_1} [Fintype I] [MeasurableSpace I] (p : Convexity.StdSimplex NNReal I) : categoricalMeasure p = ∑ i : I, ↑(p.weights i) • MeasureTheory.Measure.dirac i

The categorical law as its defining weighted sum of Dirac measures.

instance TauCeti.Probability.isProbabilityMeasure_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] (p : Convexity.StdSimplex NNReal I) : MeasureTheory.IsProbabilityMeasure (categoricalMeasure p)

A categorical law is a probability measure.

@[simp]

theorem TauCeti.Probability.categoricalMeasure_singleton {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : Convexity.StdSimplex NNReal I) (i : I) : (categoricalMeasure p) {i} = ↑(p.weights i)

The mass of a category under its categorical law is its simplex weight.

theorem MeasureTheory.Measure.exists_categoricalMeasure_eq {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (μ : Measure I) [IsProbabilityMeasure μ] : ∃ (p : Convexity.StdSimplex NNReal I), TauCeti.Probability.categoricalMeasure p = μ

Every probability measure on a finite type with measurable singletons is categorical.

@[simp]

theorem TauCeti.Probability.categoricalMeasure_real_singleton {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : Convexity.StdSimplex NNReal I) (i : I) : (categoricalMeasure p).real {i} = ↑(p.weights i)

The real mass of a category under its categorical law is its simplex weight.

theorem TauCeti.Probability.integral_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (g : I → E) (p : Convexity.StdSimplex NNReal I) : ∫ (i : I), g i ∂categoricalMeasure p = ∑ i : I, ↑(p.weights i) • g i

Integration against a categorical law is the probability-weighted finite sum.

theorem TauCeti.Probability.measurable_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] : Measurable fun (p : Convexity.StdSimplex NNReal I) => categoricalMeasure p

The categorical law is measurable in its probability vector.

theorem TauCeti.Probability.continuous_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] [TopologicalSpace I] [OpensMeasurableSpace I] : Continuous fun (p : Convexity.StdSimplex NNReal I) => (categoricalMeasure p).toProbabilityMeasure

Categorical laws vary weakly continuously with all their weights, including zero weights.

theorem Continuous.categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] [TopologicalSpace I] [OpensMeasurableSpace I] {X : Type u_3} [TopologicalSpace X] {p : X → Convexity.StdSimplex NNReal I} (hp : Continuous p) : Continuous fun (x : X) => (TauCeti.Probability.categoricalMeasure (p x)).toProbabilityMeasure

A continuous probability vector gives a weakly continuous categorical family.

@[simp]

theorem TauCeti.Probability.map_categoricalMeasure {I : Type u_1} {J : Type u_2} [Fintype I] [Fintype J] [MeasurableSpace I] [MeasurableSpace J] [MeasurableSingletonClass I] (f : I → J) (p : Convexity.StdSimplex NNReal I) : MeasureTheory.Measure.map f (categoricalMeasure p) = categoricalMeasure (Convexity.StdSimplex.map f p)

Mapping a categorical law along a map of category types adds weights over its fibres.

@[simp]

theorem TauCeti.Probability.map_piSingle_categoricalMeasure {I : Type u_1} [Fintype I] [DecidableEq I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : Convexity.StdSimplex NNReal I) : MeasureTheory.Measure.map (fun (i : I) => Pi.single i 1) (categoricalMeasure p) = multinomialMeasure 1 p

Encoding a categorical outcome as the one-hot vector Pi.single i 1 gives the multinomial law with one trial.

theorem TauCeti.Probability.hasLaw_piSingle_categoricalMeasure {I : Type u_1} [Fintype I] [DecidableEq I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : Convexity.StdSimplex NNReal I) : ProbabilityTheory.HasLaw (fun (i : I) => Pi.single i 1) (multinomialMeasure 1 p) (categoricalMeasure p)

The one-hot encoding of a categorical outcome has the one-trial multinomial law.

theorem Convexity.StdSimplex.measureReal_map_categoricalMeasure_apply {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] {β : Type u_2} [MeasurableSpace β] (p : StdSimplex NNReal I) (f : I → β) {s : Set β} (hs : MeasurableSet s) : (MeasureTheory.Measure.map f (TauCeti.Probability.categoricalMeasure p)).real s = ∑ i : I with f i ∈ s, ↑(p.weights i)

The mass of a measurable set of labels is the sum of all category weights with a label in that set. In particular, repeated labels have their weights added.

theorem Convexity.StdSimplex.ae_mem_image_support_map_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] {β : Type u_2} [MeasurableSpace β] [MeasurableSingletonClass β] (p : StdSimplex NNReal I) (f : I → β) : ∀ᵐ (x : β) ∂MeasureTheory.Measure.map f (TauCeti.Probability.categoricalMeasure p), x ∈ Finset.image f p.support

A labeled categorical law is carried by the image of its positive-weight categories.

theorem Convexity.StdSimplex.map_categoricalMeasure_singleton_ne_zero {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] {β : Type u_2} [MeasurableSpace β] (p : StdSimplex NNReal I) (f : I → β) {x : β} (hx : x ∈ Finset.image f p.support) : (MeasureTheory.Measure.map f (TauCeti.Probability.categoricalMeasure p)) {x} ≠ 0

Every positive-weight label has nonzero mass, even when several categories share it.

theorem Convexity.StdSimplex.map_categoricalMeasure_real_Iio {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : StdSimplex NNReal I) (label : I → ℝ) (x : ℝ) : (MeasureTheory.Measure.map label (TauCeti.Probability.categoricalMeasure p)).real (Set.Iio x) = ∑ i : I with label i < x, ↑(p.weights i)

The real mass below a cutoff after assigning real labels to categorical outcomes is the sum of the weights of all categories whose labels lie below that cutoff. Equal labels are therefore aggregated automatically.

theorem Convexity.StdSimplex.cdf_map_categoricalMeasure {I : Type u_1} [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I] (p : StdSimplex NNReal I) (label : I → ℝ) (x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map label (TauCeti.Probability.categoricalMeasure p))) x = ∑ i : I with label i ≤ x, ↑(p.weights i)

The cdf after assigning real labels to categorical outcomes is the sum of the weights of all categories whose labels are at most the cutoff. Equal labels are aggregated automatically.