← Copula mathematical handbook

The probability integral transform for continuous CDFs

Continuity, rather than strict monotonicity, suffices. In particular, this result allows gaps in the support of a distribution.

noncomputable def ProbabilityTheory.cdfUnit (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ↑unitInterval

A real CDF bundled with its values in the unit interval.

Equations

• ProbabilityTheory.cdfUnit μ x = ⟨↑(ProbabilityTheory.cdf μ) x, ⋯⟩

@[simp]

theorem ProbabilityTheory.coe_cdfUnit (μ : MeasureTheory.Measure ℝ) (x : ℝ) : ↑(cdfUnit μ x) = ↑(cdf μ) x

theorem ProbabilityTheory.measurable_cdfUnit (μ : MeasureTheory.Measure ℝ) : Measurable (cdfUnit μ)

theorem ProbabilityTheory.exists_cdf_eq_of_continuous (μ : MeasureTheory.Measure ℝ) (hc : Continuous ↑(cdf μ)) {t : ℝ} (ht0 : 0 < t) (ht1 : t < 1) : ∃ (x : ℝ), ↑(cdf μ) x = t

theorem ProbabilityTheory.continuous_cdf_of_atomless (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.NullSingletonClass μ] : Continuous ↑(cdf μ)

An atomless real probability measure has a continuous CDF.

theorem ProbabilityTheory.map_cdfUnit (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hc : Continuous ↑(cdf μ)) : MeasureTheory.Measure.map (cdfUnit μ) μ = MeasureTheory.volume

Applying a continuous CDF to a variable with that law gives a uniform variable.

theorem ProbabilityTheory.measurePreserving_cdfUnit (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hc : Continuous ↑(cdf μ)) : MeasureTheory.MeasurePreserving (cdfUnit μ) μ MeasureTheory.volume

The CDF transform is measure preserving when its CDF is continuous.