Regularity of the cdf of a real probability measure

Each regularity property of ProbabilityTheory.cdf μ is the image of a property of μ. The cdf is continuous at the points that are not atoms, strictly monotone when μ charges every nonempty open set, and satisfies the reflection formula cdf μ (-x) = 1 - cdf μ x when μ is invariant under negation. A measure with the first two properties has a cdf that is an order isomorphism from ℝ onto (0, 1), whose inverse is the quantile function. [UPSTREAM] candidate for Mathlib/Probability/CDF.lean.

Main definitions

• ProbabilityTheory.cdfOrderIso: the cdf as an order isomorphism ℝ ≃o Ioo 0 1.

Main results

• ProbabilityTheory.continuousAt_cdf_iff: the cdf is continuous at x iff μ {x} = 0.
• ProbabilityTheory.strictMono_cdf: the cdf of an open-positive measure is strictly monotone.
• ProbabilityTheory.cdf_neg: the reflection formula for a negation-invariant measure.
• ProbabilityTheory.range_cdf: the cdf of an atomless open-positive measure has range (0, 1).

Continuity

theorem ProbabilityTheory.continuousAt_cdf_iff (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] {x : ℝ} : ContinuousAt (↑(cdf μ)) x ↔ μ {x} = 0

The cdf is continuous at x iff x is not an atom.

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

The cdf of a measure without atoms is continuous.

Reflection

theorem ProbabilityTheory.cdf_neg (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] {x : ℝ} [μ.IsNegInvariant] (hx : μ {x} = 0) : ↑(cdf μ) (-x) = 1 - ↑(cdf μ) x

The reflection formula for the cdf of a negation-invariant measure, away from atoms.

theorem ProbabilityTheory.cdf_zero (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsNegInvariant] (h : μ {0} = 0) : ↑(cdf μ) 0 = 2⁻¹

A negation-invariant measure with no atom at 0 has median 0.

Strict monotonicity

theorem ProbabilityTheory.strictMono_cdf (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] : StrictMono ↑(cdf μ)

The cdf of a measure that charges every nonempty open set is strictly monotone.

theorem ProbabilityTheory.cdf_pos (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] (x : ℝ) : 0 < ↑(cdf μ) x

theorem ProbabilityTheory.cdf_lt_one (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] (x : ℝ) : ↑(cdf μ) x < 1

The cdf as an order isomorphism

noncomputable def ProbabilityTheory.cdfOrderIso (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] [MeasureTheory.NullSingletonClass μ] : ℝ ≃o ↑(Set.Ioo 0 1)

The cdf of an atomless open-positive probability measure as an order isomorphism between ℝ and (0, 1). Its inverse is the quantile function of μ.

Equations

• ProbabilityTheory.cdfOrderIso μ = StrictMono.orderIsoOfSurjective (Set.codRestrict (↑(ProbabilityTheory.cdf μ)) (Set.Ioo 0 1) ⋯) ⋯ ⋯

@[simp]

theorem ProbabilityTheory.coe_cdfOrderIso_apply (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] [MeasureTheory.NullSingletonClass μ] (x : ℝ) : ↑((cdfOrderIso μ) x) = ↑(cdf μ) x

@[simp]

theorem ProbabilityTheory.coe_comp_cdfOrderIso (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] [MeasureTheory.NullSingletonClass μ] : Subtype.val ∘ ⇑(cdfOrderIso μ) = ↑(cdf μ)

theorem ProbabilityTheory.range_cdf (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] [μ.IsOpenPosMeasure] [MeasureTheory.NullSingletonClass μ] : Set.range ↑(cdf μ) = Set.Ioo 0 1