Density API for the Gamma distribution

This file connects the Gamma law to HasPDF, pdf, and the Radon--Nikodym derivative, allowing consumers to pass between distributional and density formulations.

theorem TauCeti.Probability.measurable_gammaPDF (a r : ℝ) : Measurable (ProbabilityTheory.gammaPDF a r)

The ℝ≥0∞-valued Gamma density is measurable.

theorem TauCeti.Probability.hasPDF_of_hasLaw_gammaMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {a r : ℝ} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A variable with a Gamma law has a density.

theorem TauCeti.Probability.pdf_eq_gammaPDF_of_hasLaw_gammaMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {a r : ℝ} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gammaMeasure a r) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.gammaPDF a r

The density of a Gamma law is gammaPDF.

theorem TauCeti.Probability.rnDeriv_gammaMeasure (a r : ℝ) : (ProbabilityTheory.gammaMeasure a r).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.gammaPDF a r

The Radon--Nikodym derivative of a Gamma law is gammaPDF.