Density API for the Pareto distribution

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

theorem TauCeti.Probability.measurable_paretoPDF (t r : ℝ) : Measurable (ProbabilityTheory.paretoPDF t r)

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

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

A variable with a Pareto law has a density.

theorem TauCeti.Probability.pdf_eq_paretoPDF_of_hasLaw_paretoMeasure {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t r : ℝ} (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.paretoMeasure t r) P) : MeasureTheory.pdf X P MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.paretoPDF t r

The density of a Pareto law is paretoPDF.

theorem TauCeti.Probability.rnDeriv_paretoMeasure (t r : ℝ) : (ProbabilityTheory.paretoMeasure t r).rnDeriv MeasureTheory.volume =ᵐ[MeasureTheory.volume] ProbabilityTheory.paretoPDF t r

The Radon--Nikodym derivative of a Pareto law is paretoPDF.