Density API for the Beta distribution

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

theorem TauCeti.Probability.measurable_betaPDF (α β : ℝ) : Measurable (ProbabilityTheory.betaPDF α β)

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

theorem TauCeti.Probability.hasPDF_of_hasLaw_betaMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {α β : ℝ} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.betaMeasure α β) P) : MeasureTheory.HasPDF X P MeasureTheory.volume

A variable with a Beta law has a density.

theorem TauCeti.Probability.pdf_eq_betaPDF_of_hasLaw_betaMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {α β : ℝ} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.betaMeasure α β) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.betaPDF α β

The density of a Beta law is betaPDF.

theorem TauCeti.Probability.rnDeriv_betaMeasure (α β : ℝ) : (ProbabilityTheory.betaMeasure α β).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.betaPDF α β

The Radon--Nikodym derivative of a Beta law is betaPDF.