Densities from laws presented as withDensity

Two bridges from a law given as μ.withDensity f to Mathlib's MeasureTheory.HasPDF and pdf, together with three bridges for a law presented by a nonnegative real-valued density: integrable_withDensity_ofReal_iff and integral_withDensity_ofReal reduce integrability and integration under such a law to the density-weighted function against the reference measure, and measureReal_withDensity_ofReal computes the real mass of a measurable set as the integral of the density over it.

Several of Mathlib's continuous scalar families can be presented as withDensity measures — some by definition, others only away from a degenerate parameter — and so can laws Tau Ceti builds on top of them, but none is connected to HasPDF. These theorems make that connection once, so no individual family has to repeat the hasPDF_of_map_eq_withDensity hX.aemeasurable … hX.map_eq plumbing, and the family files do not each re-prove the same density integral and mass identities.

The file is deliberately neutral: it mentions no particular distribution, so a module defining one family can import it without acquiring the others.

Main results

• hasPDF_of_hasLaw_withDensity — a law presented as μ.withDensity f gives HasPDF;
• pdf_eq_of_hasLaw_withDensity — and its density is f;
• integrable_withDensity_ofReal_iff — under a law μ.withDensity (ENNReal.ofReal ∘ f), a function is integrable iff f-weighted against the reference measure it is;
• integral_withDensity_ofReal — and its integral is the integral of the f-weighted integrand;
• measureReal_withDensity_ofReal — the real mass of a measurable set on which the density f is nonnegative and integrable is its integral over that set.

The density bridges are stated for an arbitrary codomain and codomain measure, since neither proof uses anything about ℝ or volume, and both ask only for AEMeasurable f μ.

theorem TauCeti.Probability.hasPDF_of_hasLaw_withDensity {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [MeasurableSpace E] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : Ω → E} {f : E → ENNReal} (hf : AEMeasurable f μ) (hX : ProbabilityTheory.HasLaw X (μ.withDensity f) P) : MeasureTheory.HasPDF X P μ

The shared bridge. A law presented as μ.withDensity f, with f a.e. measurable, gives HasPDF.

theorem TauCeti.Probability.pdf_eq_of_hasLaw_withDensity {Ω : Type u_1} {E : Type u_2} [MeasurableSpace Ω] [MeasurableSpace E] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E} {X : Ω → E} {f : E → ENNReal} [MeasureTheory.SigmaFinite μ] (hf : AEMeasurable f μ) (hX : ProbabilityTheory.HasLaw X (μ.withDensity f) P) : MeasureTheory.pdf X P μ =ᵐ[μ] f

The density supplied by hasPDF_of_hasLaw_withDensity is the one the law was presented with.

Needs [SigmaFinite μ] on the codomain measure — satisfied by volume — and nothing on the source measure.

theorem TauCeti.Probability.integrable_withDensity_ofReal_iff {α : Type u_3} {F : Type u_4} [MeasurableSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure α} {g : α → F} {ρ : α → ℝ} (hρ : AEMeasurable ρ μ) (hnn : 0 ≤ᵐ[μ] ρ) : MeasureTheory.Integrable g (μ.withDensity fun (x : α) => ENNReal.ofReal (ρ x)) ↔ MeasureTheory.Integrable (fun (x : α) => ρ x • g x) μ

Under a law presented by a real-valued density ρ, a function is integrable iff its scalar product with ρ is integrable against the reference measure. The density need only be nonnegative a.e.; the ℝ≥0∞-valued density used in the presentation is its ENNReal.ofReal lift.

theorem TauCeti.Probability.integral_withDensity_ofReal {α : Type u_3} {F : Type u_4} [MeasurableSpace α] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure α} {ρ : α → ℝ} (hρ : AEMeasurable ρ μ) (hnn : 0 ≤ᵐ[μ] ρ) (g : α → F) : (∫ (x : α), g x ∂μ.withDensity fun (x : α) => ENNReal.ofReal (ρ x)) = ∫ (x : α), ρ x • g x ∂μ

Under a law presented by a real-valued density ρ, integration is integration of the ρ-weighted integrand against the reference measure. This is the integral counterpart of TauCeti.Probability.integrable_withDensity_ofReal_iff, and it needs no integrability hypothesis: when the integrand is not integrable both sides are 0.

It specializes Mathlib's integral_withDensity_eq_integral_toReal_smul₀ to densities of the form ENNReal.ofReal ∘ ρ, where the toReal of the density reduces to ρ itself.

theorem TauCeti.Probability.measureReal_withDensity_ofReal {α : Type u_3} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ρ : α → ℝ} {s : Set α} (hnn : 0 ≤ᵐ[μ.restrict s] ρ) (hs : MeasurableSet s) (hint : MeasureTheory.IntegrableOn ρ s μ) : (μ.withDensity fun (x : α) => ENNReal.ofReal (ρ x)).real s = ∫ (x : α) in s, ρ x ∂μ

Integrating a density that is nonnegative and integrable on s computes the real mass of s under the law presented by that density. The nonnegativity hypothesis is only local to s.