← Mathematical handbook

The Laplace transform of a gamma law

Exponential tilting changes the rate of a gamma density. Normalizing the tilted density gives its Laplace transform without an interchange of improper integrals.

theorem ProbabilityTheory.gammaPDF_mul_exp_neg {a t : ℝ} (ha : 0 < a) (ht : 0 ≤ t) (x : ℝ) : gammaPDF a 1 x * ENNReal.ofReal (Real.exp (-(t * x))) = ENNReal.ofReal ((1 + t) ^ (-a)) * gammaPDF a (1 + t) x

Exponential tilting of a rate-one gamma density.

theorem ProbabilityTheory.lintegral_exp_neg_gammaMeasure {a t : ℝ} (ha : 0 < a) (ht : 0 ≤ t) : ∫⁻ (x : ℝ), ENNReal.ofReal (Real.exp (-(t * x))) ∂gammaMeasure a 1 = ENNReal.ofReal ((1 + t) ^ (-a))

The Laplace transform of a gamma variable with shape a and rate one.

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

Gamma variables with positive parameters are strictly positive almost surely.