Independent Gamma variables and the Beta distribution

This file studies the coordinate change

(x, y) ↦ (x / (x + y), x + y)

on the positive quadrant. Its inverse sends (u, s) to (u * s, (1 - u) * s) and has Jacobian determinant s. Applied to two independent Gamma laws with a common rate, the change of variables separates their ratio from their sum: the ratio is Beta-distributed, the sum is Gamma-distributed, and the two are independent.

Main result

• TauCeti.Probability.map_div_add_prod_gammaMeasure identifies the joint pushforward with the product of a Beta law and a Gamma law.
• TauCeti.Probability.map_div_add_gammaMeasure gives the Beta marginal.
• MeasureTheory.Measure.map_prod_prod_gammaMeasure_div_add carries the Beta marginal, for the ratio y / (y + x), along an independent factor.
• TauCeti.Probability.indepFun_div_add_gammaMeasure proves independence under the product Gamma law.
• TauCeti.Probability.hasLaw_div_add_prod_gammaMeasure_of_indepFun, TauCeti.Probability.hasLaw_div_add_gammaMeasure_of_indepFun, and TauCeti.Probability.indepFun_div_add_of_hasLaw_gammaMeasure transfer the conclusions to independent random variables.

References

• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 2, 2nd ed., Wiley, 1995.

The Gamma--Beta coordinate change

def TauCeti.Probability.gammaBetaSource : Set (ℝ × ℝ)

The positive quadrant on which the Gamma--Beta coordinate change is bijective.

def TauCeti.Probability.gammaBetaTarget : Set (ℝ × ℝ)

The product of the open unit interval and the positive half-line.

noncomputable def TauCeti.Probability.gammaBetaMap (z : ℝ × ℝ) : ℝ × ℝ

The ratio-and-sum coordinate map.

def TauCeti.Probability.betaGammaMap (z : ℝ × ℝ) : ℝ × ℝ

The inverse of the ratio-and-sum coordinate map.

theorem TauCeti.Probability.measurable_gammaBetaMap : Measurable gammaBetaMap

The ratio-and-sum coordinate map is measurable.

theorem TauCeti.Probability.measurable_betaGammaMap : Measurable betaGammaMap

The inverse Gamma--Beta coordinate map is measurable.

theorem TauCeti.Probability.betaGammaMap_mem_source {z : ℝ × ℝ} (hz : z ∈ gammaBetaTarget) : betaGammaMap z ∈ gammaBetaSource

The inverse coordinate map sends the target region into the positive quadrant.

theorem TauCeti.Probability.gammaBetaMap_mem_target {z : ℝ × ℝ} (hz : z ∈ gammaBetaSource) : gammaBetaMap z ∈ gammaBetaTarget

The ratio-and-sum coordinate map sends the positive quadrant into its target region.

theorem TauCeti.Probability.gammaBetaMap_betaGammaMap {z : ℝ × ℝ} (hz : z ∈ gammaBetaTarget) : gammaBetaMap (betaGammaMap z) = z

The ratio-and-sum map is a left inverse to the inverse coordinate map on the target region.

theorem TauCeti.Probability.betaGammaMap_gammaBetaMap {z : ℝ × ℝ} (hz : z ∈ gammaBetaSource) : betaGammaMap (gammaBetaMap z) = z

The inverse coordinate map is a left inverse to the ratio-and-sum map on the source region.

theorem TauCeti.Probability.betaGammaMap_image_target : betaGammaMap '' gammaBetaTarget = gammaBetaSource

The inverse coordinate map sends the target region onto the positive quadrant.

theorem TauCeti.Probability.betaGammaMap_injOn : Set.InjOn betaGammaMap gammaBetaTarget

The inverse coordinate map is injective on the target region.

noncomputable def TauCeti.Probability.fderivBetaGammaMap (z : ℝ × ℝ) : ℝ × ℝ →L[ℝ] ℝ × ℝ

The derivative of the inverse Gamma--Beta coordinate map.

theorem TauCeti.Probability.hasFDerivAt_betaGammaMap (z : ℝ × ℝ) : HasFDerivAt betaGammaMap (fderivBetaGammaMap z) z

The stated continuous linear map is the derivative of the inverse coordinate map.

theorem TauCeti.Probability.det_fderivBetaGammaMap (z : ℝ × ℝ) : (fderivBetaGammaMap z).det = z.2

The Jacobian determinant of the inverse Gamma--Beta coordinate map is its second coordinate.

theorem TauCeti.Probability.map_betaGammaMap_withDensity : MeasureTheory.Measure.map betaGammaMap ((MeasureTheory.volume.restrict gammaBetaTarget).withDensity fun (z : ℝ × ℝ) => ENNReal.ofReal z.2) = MeasureTheory.volume.restrict gammaBetaSource

The Jacobian formula for the inverse coordinate change, expressed as an equality of restricted Lebesgue measures.

Independent Gamma variables

theorem TauCeti.Probability.map_div_add_prod_gammaMeasure {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) : MeasureTheory.Measure.map (fun (z : ℝ × ℝ) => (z.1 / (z.1 + z.2), z.1 + z.2)) ((ProbabilityTheory.gammaMeasure a r).prod (ProbabilityTheory.gammaMeasure b r)) = (ProbabilityTheory.betaMeasure a b).prod (ProbabilityTheory.gammaMeasure (a + b) r)

The ratio and sum of two independent Gamma variables with the same positive rate have the product law betaMeasure a b ⊗ gammaMeasure (a + b) r. In particular, the ratio and sum are independent. The denominator-zero branch of the ratio is irrelevant because both Gamma variables are strictly positive almost surely.

theorem TauCeti.Probability.map_div_add_gammaMeasure {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) : MeasureTheory.Measure.map (fun (z : ℝ × ℝ) => z.1 / (z.1 + z.2)) ((ProbabilityTheory.gammaMeasure a r).prod (ProbabilityTheory.gammaMeasure b r)) = ProbabilityTheory.betaMeasure a b

The ratio of two independent Gamma variables with a common positive rate has a Beta law.

theorem MeasureTheory.Measure.map_prod_prod_gammaMeasure_div_add {α : Type u_1} [MeasurableSpace α] (δ : Measure α) [SFinite δ] {p q r : ℝ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) : map (fun (z : (α × ℝ) × ℝ) => (z.2 / (z.2 + z.1.2), z.1.1)) ((δ.prod (ProbabilityTheory.gammaMeasure q r)).prod (ProbabilityTheory.gammaMeasure p r)) = (ProbabilityTheory.betaMeasure p q).prod δ

The Gamma–Beta ratio law, carried along an independent factor: for independent Gamma totals t ~ Γ(q, r) and s ~ Γ(p, r) and an independent w ~ δ, the pair (s / (s + t), w) has law Beta(p, q) ⊗ δ.

theorem TauCeti.Probability.indepFun_div_add_gammaMeasure {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) : ProbabilityTheory.IndepFun (fun (z : ℝ × ℝ) => z.1 / (z.1 + z.2)) (fun (z : ℝ × ℝ) => z.1 + z.2) ((ProbabilityTheory.gammaMeasure a r).prod (ProbabilityTheory.gammaMeasure b r))

Under the product of two Gamma laws with a common positive rate, the ratio is independent of the sum.

theorem TauCeti.Probability.hasLaw_div_add_prod_gammaMeasure_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) (hXY : ProbabilityTheory.IndepFun X Y P) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) (hY : ProbabilityTheory.HasLaw Y (ProbabilityTheory.gammaMeasure b r) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => (X ω / (X ω + Y ω), X ω + Y ω)) ((ProbabilityTheory.betaMeasure a b).prod (ProbabilityTheory.gammaMeasure (a + b) r)) P

For independent Gamma variables with a common positive rate, the pair consisting of their ratio and their sum has the product of a Beta law and a Gamma law.

theorem TauCeti.Probability.hasLaw_div_add_gammaMeasure_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) (hXY : ProbabilityTheory.IndepFun X Y P) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) (hY : ProbabilityTheory.HasLaw Y (ProbabilityTheory.gammaMeasure b r) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => X ω / (X ω + Y ω)) (ProbabilityTheory.betaMeasure a b) P

The ratio of independent Gamma random variables with a common positive rate has a Beta law.

theorem TauCeti.Probability.indepFun_div_add_of_hasLaw_gammaMeasure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {a b r : ℝ} (ha : 0 < a) (hb : 0 < b) (hr : 0 < r) (hXY : ProbabilityTheory.IndepFun X Y P) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) (hY : ProbabilityTheory.HasLaw Y (ProbabilityTheory.gammaMeasure b r) P) : ProbabilityTheory.IndepFun (fun (ω : Ω) => X ω / (X ω + Y ω)) (fun (ω : Ω) => X ω + Y ω) P

The ratio and sum of independent Gamma random variables with a common positive rate are independent.