Gamma normalization and the Dirichlet distribution

Independent Gamma variables with positive shapes and a common positive rate are normalized by their sum. The sum and the normalized vector have a product law: Gamma with the total shape, and Dirichlet with the original shapes.

The main random-variable results are iIndepFun.hasLaw_dirichlet_of_gamma, iIndepFun.hasLaw_sum_gamma, and iIndepFun.indepFun_sum_simplexNormalize_gamma. Their common source is map_sum_simplexNormalize_pi_gammaMeasure.

The index type is finite and nonempty; the singleton case is included. Empty families are excluded because their total is zero and the project's empty-index Dirichlet measure is not a probability measure. The normalization denominator is almost surely positive.

The proof uses the elementary radial integration formula from StdSimplexMeasure.Radial; neither complex Dirichlet measures nor analytic continuation is involved.

theorem ProbabilityTheory.pi_gammaMeasure_eq_withDensity {ι : Type u_1} [Fintype ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) {r : ℝ} (hr : 0 < r) : (MeasureTheory.Measure.pi fun (i : ι) => gammaMeasure (b i) r) = MeasureTheory.volume.withDensity fun (x : ι → ℝ) => ∏ i : ι, gammaPDF (b i) r (x i)

The finite product of Gamma measures has the product of their densities.

theorem ProbabilityTheory.gammaPDFReal_radial {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) {r t : ℝ} (hr : 0 < r) (ht : 0 < t) {u : ι → ℝ} (hu : u ∈ stdSimplexInterior) : t ^ (Fintype.card ι - 1) * ∏ i : ι, gammaPDFReal (b i) r (t * u i) = gammaPDFReal (∑ i : ι, b i) r t * dirichletPdfReal b u

The density factorization in radial coordinates. The Jacobian is the coordinate-simplex factor t^(card ι - 1), not an ambient Euclidean surface-area factor.

noncomputable def ProbabilityTheory.simplexNormalize {ι : Type u_1} [Fintype ι] (x : ι → ℝ) : ι → ℝ

Normalize a vector by its coordinate sum. At sum zero this is the zero vector, following Lean's convention for division by zero.

Equations

• ProbabilityTheory.simplexNormalize x i = x i / ∑ j : ι, x j

theorem ProbabilityTheory.measurable_simplexNormalize {ι : Type u_1} [Fintype ι] : Measurable simplexNormalize

theorem ProbabilityTheory.sum_simplexNormalize_smul {ι : Type u_1} [Fintype ι] {t : ℝ} (ht : 0 < t) {u : ι → ℝ} (hu : u ∈ Convexity.StdSimplex.coordinateSet ℝ ι) : (∑ i : ι, (t • u) i, simplexNormalize (t • u)) = (t, u)

Radial coordinates recover a simplex point and its positive scale.

theorem ProbabilityTheory.ae_pos_gammaMeasure (a r : ℝ) : ∀ᵐ (t : ℝ) ∂gammaMeasure a r, 0 < t

Gamma measure is concentrated on strictly positive values.

theorem ProbabilityTheory.gammaPDF_radial {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) {r t : ℝ} (hr : 0 < r) (ht : 0 < t) {u : ι → ℝ} (hu : u ∈ stdSimplexInterior) : ENNReal.ofReal (t ^ (Fintype.card ι - 1)) * ∏ i : ι, gammaPDF (b i) r (t * u i) = gammaPDF (∑ i : ι, b i) r t * dirichletPdf b u

Nonnegative density factorization in radial coordinates.

theorem ProbabilityTheory.map_sum_simplexNormalize_pi_gammaMeasure {ι : Type u_1} [Fintype ι] [Nonempty ι] {b : ι → ℝ} (hb : b ∈ mvRealBetaDomain) {r : ℝ} (hr : 0 < r) : MeasureTheory.Measure.map (fun (x : ι → ℝ) => (∑ i : ι, x i, simplexNormalize x)) (MeasureTheory.Measure.pi fun (i : ι) => gammaMeasure (b i) r) = (gammaMeasure (∑ i : ι, b i) r).prod (dirichletMeasure b)

The joint law of the total and normalized coordinates under a product of Gamma measures.

theorem ProbabilityTheory.iIndepFun.hasLaw_sum_simplexNormalize_gamma {ι : Type u_1} [Fintype ι] [Nonempty ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {b : ι → ℝ} {r : ℝ} (h : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (gammaMeasure (b i) r) P) (hb : b ∈ mvRealBetaDomain) (hr : 0 < r) : HasLaw (fun (ω : Ω) => (∑ i : ι, X i ω, simplexNormalize fun (i : ι) => X i ω)) ((gammaMeasure (∑ i : ι, b i) r).prod (dirichletMeasure b)) P

Independent Gamma variables with a common rate have independent total and normalized vector, with the indicated Gamma and Dirichlet laws.

theorem ProbabilityTheory.iIndepFun.hasLaw_sum_gamma {ι : Type u_1} [Fintype ι] [Nonempty ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {b : ι → ℝ} {r : ℝ} (h : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (gammaMeasure (b i) r) P) (hb : b ∈ mvRealBetaDomain) (hr : 0 < r) : HasLaw (fun (ω : Ω) => ∑ i : ι, X i ω) (gammaMeasure (∑ i : ι, b i) r) P

The sum of independent Gamma variables with a common rate is Gamma-distributed, with shape the sum of the shapes.

theorem ProbabilityTheory.iIndepFun.hasLaw_dirichlet_of_gamma {ι : Type u_1} [Fintype ι] [Nonempty ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {b : ι → ℝ} {r : ℝ} (h : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (gammaMeasure (b i) r) P) (hb : b ∈ mvRealBetaDomain) (hr : 0 < r) : HasLaw (fun (ω : Ω) (i : ι) => X i ω / ∑ j : ι, X j ω) (dirichletMeasure b) P

Gamma normalization constructs a Dirichlet random vector. In particular, take r = 1 for the unit-rate Gamma-ratio characterization.

theorem ProbabilityTheory.iIndepFun.indepFun_sum_simplexNormalize_gamma {ι : Type u_1} [Fintype ι] [Nonempty ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {b : ι → ℝ} {r : ℝ} (h : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (gammaMeasure (b i) r) P) (hb : b ∈ mvRealBetaDomain) (hr : 0 < r) : IndepFun (fun (ω : Ω) => ∑ i : ι, X i ω) (fun (ω : Ω) (i : ι) => X i ω / ∑ j : ι, X j ω) P

The total of independent Gamma variables is independent of their ratios to that total.

theorem ProbabilityTheory.iIndepFun.ae_pos_sum_gamma {ι : Type u_1} [Fintype ι] [Nonempty ι] {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {b : ι → ℝ} {r : ℝ} (h : iIndepFun X P) (hX : ∀ (i : ι), HasLaw (X i) (gammaMeasure (b i) r) P) (hb : b ∈ mvRealBetaDomain) (hr : 0 < r) : ∀ᵐ (ω : Ω) ∂P, 0 < ∑ i : ι, X i ω

The denominator in the Gamma-ratio construction is almost surely strictly positive.