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

If the CDF of a probability measure μ is continuous at x, then μ assigns zero mass to the singleton {x}. Continuity of the CDF at x corresponds to absence of an atom at x.

theorem ProbabilityTheory.cdf_continuousAt_frontier_Iic_null (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (x : ℝ) (hx : ContinuousAt (↑(cdf μ)) x) : μ (frontier (Set.Iic x)) = 0

If the CDF of a probability measure μ is continuous at x, then the boundary frontier (Iic x) = {x} is μ-null. This is the form needed for the Portmanteau theorem.

theorem ProbabilityTheory.probMeasure_Ioc_eq_toNNReal_cdf (ν : MeasureTheory.ProbabilityMeasure ℝ) (a b : ℝ) : ν (Set.Ioc a b) = (↑(cdf ↑ν) b - ↑(cdf ↑ν) a).toNNReal

For a probability measure ν on ℝ, the mass of a half-open interval (a, b] equals F(b) - F(a) (cast to ℝ≥0), where F is the CDF of ν.

theorem ProbabilityTheory.dense_cdf_continuityPoints (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] : Dense {x : ℝ | ContinuousAt (↑(cdf μ)) x}

The set of continuity points of the CDF of a probability measure is dense in ℝ. This follows from the fact that a monotone function has only countably many discontinuities.

theorem ProbabilityTheory.weakConvergence_iff_bounded_continuous (μs : ℕ → MeasureTheory.ProbabilityMeasure ℝ) (μ : MeasureTheory.ProbabilityMeasure ℝ) : Filter.Tendsto μs Filter.atTop (nhds μ) ↔ ∀ (f : BoundedContinuousFunction ℝ ℝ), Filter.Tendsto (fun (n : ℕ) => ∫ (x : ℝ), f x ∂↑(μs n)) Filter.atTop (nhds (∫ (x : ℝ), f x ∂↑μ))

Portmanteau theorem (weak convergence via bounded continuous functions). A sequence of probability measures μₙ on ℝ converges weakly to μ if and only if ∫ f dμₙ → ∫ f dμ for every bounded continuous function f : ℝ →ᵇ ℝ.