Real normalized Dirichlet measure on the standard simplex

The multivariate Dirichlet measure [KBJ00, Ch 49] is defined on the standard simplex in symmetric variables, i.e. Convexity.StdSimplex.coordinateSet ℝ ι, or $E^{k-1}$ embedded in $ℝ^k$ where k = card ι.

This file constructs the density and the probability measure, and records permutation invariance and vector-valued integration against the density. The real monomial integral theory is in Dirichlet.Integral.Real; moments, aggregation, and the beta marginal are in Dirichlet.Moments. No complex Dirichlet integral or parameter continuation is imported.

The construction uses the standard-simplex coordinate measure and integral API exported by StdSimplexMeasure.Measure and StdSimplexMeasure.Integral. The coordinate constructions are provided transitively by StdSimplexMeasure.Coordinates.

References

[KBJ00] Kotz, Samuel, Narayanaswamy Balakrishnan, and Norman L. Johnson. "Continuous multivariate distributions, Volume 1: Models and applications." John Wiley & Sons, 2000. Online: https://dx.doi.org/10.1002/0471722065.

noncomputable def ProbabilityTheory.dirichletPdfReal {ι : Type u_1} [Fintype ι] (b u : ι → ℝ) : ℝ

The real-valued Dirichlet PDF with parameters b. This PDF is supported on stdSimplexInterior ι.

Equations

• ProbabilityTheory.dirichletPdfReal b u = 1 / ProbabilityTheory.mvRealBeta b * ProbabilityTheory.stdSimplexInterior.indicator (fun (u : ι → ℝ) => ∏ i : ι, u i ^ (b i - 1)) u

noncomputable def ProbabilityTheory.dirichletPdf {ι : Type u_1} [Fintype ι] (b u : ι → ℝ) : ENNReal

The ENNReal-valued Dirichlet PDF.

Equations

• ProbabilityTheory.dirichletPdf b u = ENNReal.ofReal (ProbabilityTheory.dirichletPdfReal b u)

noncomputable def ProbabilityTheory.dirichletMeasure {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : MeasureTheory.Measure (ι → ℝ)

The Dirichlet measure on the standard simplex.

Equations

• ProbabilityTheory.dirichletMeasure b = MeasureTheory.Measure.stdSimplexMeasure.withDensity (ProbabilityTheory.dirichletPdf b)

theorem ProbabilityTheory.measurable_dirichletPdfReal {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : Measurable (dirichletPdfReal b)

The real-valued Dirichlet density is a measurable function.

theorem ProbabilityTheory.measurable_dirichletPdf {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : Measurable (dirichletPdf b)

The (ENNReal) Dirichlet density is a measurable function.

theorem ProbabilityTheory.rnDeriv_dirichletMeasure {ι : Type u_1} [Fintype ι] {b : ι → ℝ} : b ∈ mvRealBetaDomain → (dirichletMeasure b).rnDeriv MeasureTheory.Measure.stdSimplexMeasure =ᵐ[MeasureTheory.Measure.stdSimplexMeasure] dirichletPdf b

The Radon-Nikodym derivative of the Dirichlet measure is almost everywhere equal to the Dirichlet PDF.

theorem ProbabilityTheory.dirichletPdfReal_nonneg {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (u : ι → ℝ) : 0 ≤ dirichletPdfReal b u

The real-valued Dirichlet density is nonnegative.

theorem ProbabilityTheory.integral_dirichletMeasure_smul {ι : Type u_1} [Fintype ι] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (f : (ι → ℝ) → E) : ∫ (u : ι → ℝ), f u ∂dirichletMeasure b = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, dirichletPdfReal b u • f u ∂MeasureTheory.Measure.stdSimplexMeasure

Unwraps an integral against the Dirichlet measure into an integral against the standard simplex measure, explicitly multiplying the function by the Dirichlet density.

theorem ProbabilityTheory.integral_dirichletMeasure {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (f : (ι → ℝ) → ℝ) : ∫ (u : ι → ℝ), f u ∂dirichletMeasure b = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, f u * dirichletPdfReal b u ∂MeasureTheory.Measure.stdSimplexMeasure

Real-valued integration against the Dirichlet probability measure is integration against its density on the simplex.

theorem ProbabilityTheory.dirichletMeasure_stdSimplex {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : (dirichletMeasure b) (Convexity.StdSimplex.coordinateSet ℝ ι) = 1

The measure of the standard simplex under the Dirichlet measure equals 1.

theorem ProbabilityTheory.dirichletPdf_eq_zero_of_not_mem_stdSimplex {ι : Type u_1} [Fintype ι] (b : ι → ℝ) {u : ι → ℝ} (hu : u ∉ Convexity.StdSimplex.coordinateSet ℝ ι) : dirichletPdf b u = 0

The Dirichlet density vanishes outside Convexity.StdSimplex.coordinateSet ℝ ι.

theorem ProbabilityTheory.dirichletMeasure_restrict {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : (dirichletMeasure b).restrict (Convexity.StdSimplex.coordinateSet ℝ ι) = dirichletMeasure b

The Dirichlet measure is restricted to the standard simplex.

theorem ProbabilityTheory.isProbabilityMeasure_dirichletMeasure {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : MeasureTheory.IsProbabilityMeasure (dirichletMeasure b)

The Dirichlet measure satisfies isProbabilityMeasure.

theorem ProbabilityTheory.memLp_dirichletMeasure_coordinate {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) (i : ι) (p : ENNReal) : MeasureTheory.MemLp (fun (u : ι → ℝ) => u i) p (dirichletMeasure b)

Every Dirichlet coordinate belongs to every Lᵖ space on the positive parameter domain.

theorem ProbabilityTheory.integral_dirichletMeasure_one {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) : ∫ (x : ι → ℝ), 1 ∂dirichletMeasure b = 1

The total mass / integral of the constant function 1 with respect to the Dirichlet measure is 1.

theorem ProbabilityTheory.absolutelyContinuous_dirichletMeasure {ι : Type u_1} [Fintype ι] (b : ι → ℝ) : (dirichletMeasure b).AbsolutelyContinuous MeasureTheory.Measure.stdSimplexMeasure

The Dirichlet measure is absolutely continuous with respect to stdSimplexMeasure.

noncomputable def ProbabilityTheory.dirichletMeasureUniform {ι : Type u_1} [Fintype ι] (α : ℝ) : MeasureTheory.Measure (ι → ℝ)

Defining the Dirichlet measure for the case of all b parameters equal.

Equations

• ProbabilityTheory.dirichletMeasureUniform α = ProbabilityTheory.dirichletMeasure fun (x : ι) => α

theorem ProbabilityTheory.dirichletMeasureUniform_one {ι : Type u_1} [Fintype ι] : dirichletMeasureUniform 1 = (1 / MeasureTheory.Measure.stdSimplexMeasure (Convexity.StdSimplex.coordinateSet ℝ ι)) • MeasureTheory.Measure.stdSimplexMeasure.restrict (Convexity.StdSimplex.coordinateSet ℝ ι)

The case of all b parameters equal to 1 reduces to scaled Lebesgue measure.

theorem ProbabilityTheory.dirichletPdf_perm {ι : Type u_1} [Fintype ι] (b : ι → ℝ) (σ : Equiv.Perm ι) (u : ι → ℝ) : dirichletPdf (b ∘ ⇑σ) (u ∘ ⇑σ) = dirichletPdf b u

Simultaneously permuting the parameters and coordinates leaves the Dirichlet density unchanged.

theorem ProbabilityTheory.measurePreserving_dirichletMeasure_perm {ι : Type u_1} [Fintype ι] (b : ι → ℝ) (σ : Equiv.Perm ι) : MeasureTheory.MeasurePreserving (fun (x : ι → ℝ) => x ∘ ⇑σ) (dirichletMeasure b) (dirichletMeasure (b ∘ ⇑σ))

Permuting coordinates together with parameters is a measure-preserving transformation of dirichletMeasure.

theorem DirichletTransform.integral_dirichletMeasure_complex {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ ProbabilityTheory.mvRealBetaDomain) (f : (ι → ℝ) → ℂ) : ∫ (u : ι → ℝ), f u ∂ProbabilityTheory.dirichletMeasure b = ∫ (u : ι → ℝ) in Convexity.StdSimplex.coordinateSet ℝ ι, ↑(ProbabilityTheory.dirichletPdfReal b u) * f u ∂MeasureTheory.Measure.stdSimplexMeasure

A complex-valued integral against a real Dirichlet measure can be written using its real density and the standard-simplex measure.