Cumulative distribution functions of laws with densities

This file connects a density presentation of a real probability law to its cumulative distribution function. The cdf is an indefinite integral of the density, so it is absolutely continuous on compact intervals, differentiable almost everywhere, and differentiable at every continuity point of the density.

Main results

• TauCeti.Probability.cdf_sub_cdf_eq_integral_of_eq_withDensity identifies cdf increments with density integrals;
• TauCeti.Probability.strictMono_cdf_of_eq_withDensity proves strict increase for an everywhere positive density;
• TauCeti.Probability.absolutelyContinuousOnInterval_cdf_of_eq_withDensity proves absolute continuity of the cdf;
• TauCeti.Probability.ae_hasDerivAt_cdf_of_eq_withDensity identifies its derivative almost everywhere;
• TauCeti.Probability.hasDerivAt_cdf_of_eq_withDensity identifies its derivative where the density is continuous.

theorem TauCeti.Probability.cdf_sub_cdf_eq_integral_of_eq_withDensity {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ = MeasureTheory.volume.withDensity fun (t : ℝ) => ENNReal.ofReal (f t)) (hfm : AEMeasurable f MeasureTheory.volume) (hnn : 0 ≤ᵐ[MeasureTheory.volume] f) (a b : ℝ) : ↑(ProbabilityTheory.cdf μ) b - ↑(ProbabilityTheory.cdf μ) a = ∫ (t : ℝ) in a..b, f t

The cdf increment of a law with a density. For a law with nonnegative density f, the increment of the cdf over a..b is the integral of the density over a..b.

theorem TauCeti.Probability.strictMono_cdf_of_eq_withDensity {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ = MeasureTheory.volume.withDensity fun (t : ℝ) => ENNReal.ofReal (f t)) (hfm : AEMeasurable f MeasureTheory.volume) (hpos : ∀ (t : ℝ), 0 < f t) : StrictMono ↑(ProbabilityTheory.cdf μ)

A real probability law with an everywhere positive density has a strictly increasing cdf.

theorem TauCeti.Probability.absolutelyContinuousOnInterval_cdf_of_eq_withDensity {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ = MeasureTheory.volume.withDensity fun (t : ℝ) => ENNReal.ofReal (f t)) (hfm : AEMeasurable f MeasureTheory.volume) (hnn : 0 ≤ᵐ[MeasureTheory.volume] f) (a b : ℝ) : AbsolutelyContinuousOnInterval (↑(ProbabilityTheory.cdf μ)) a b

The cdf of a law with a nonnegative density is absolutely continuous on every compact interval.

theorem TauCeti.Probability.ae_hasDerivAt_cdf_of_eq_withDensity {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ = MeasureTheory.volume.withDensity fun (t : ℝ) => ENNReal.ofReal (f t)) (hfm : AEMeasurable f MeasureTheory.volume) (hnn : 0 ≤ᵐ[MeasureTheory.volume] f) : ∀ᵐ (t : ℝ), HasDerivAt (↑(ProbabilityTheory.cdf μ)) (f t) t

Lebesgue differentiation of the cdf. The cdf of a law with a nonnegative density f has derivative f t at almost every point t.

theorem TauCeti.Probability.hasDerivAt_cdf_of_eq_withDensity {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ = MeasureTheory.volume.withDensity fun (t : ℝ) => ENNReal.ofReal (f t)) (hfm : AEMeasurable f MeasureTheory.volume) (hnn : 0 ≤ᵐ[MeasureTheory.volume] f) {t : ℝ} (hft : ContinuousAt f t) : HasDerivAt (↑(ProbabilityTheory.cdf μ)) (f t) t

The cdf of a law with a nonnegative density f has derivative f t at every point t where the density is continuous.