theorem stieltjes_measure_construction (f : StieltjesFunction ℝ) (hf_bot : Filter.Tendsto (↑f) Filter.atBot (nhds 0)) (hf_top : Filter.Tendsto (↑f) Filter.atTop (nhds 1)) : MeasureTheory.IsProbabilityMeasure f.measure ∧ (∀ (a b : ℝ), a ≤ b → f.measure (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)) ∧ ∀ (ν : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure ν], (∀ (a b : ℝ), a ≤ b → ν (Set.Ioc a b) = ENNReal.ofReal (↑f b - ↑f a)) → ν = f.measure

Construction of measures on ℝ (Lecture 2, "How do we produce measures on R?"): for every right-continuous, non-decreasing function f : ℝ → ℝ (encoded here as a StieltjesFunction) tending to 0 at -∞ and to 1 at +∞, there is a unique Borel probability measure on ℝ assigning each half-open interval (a, b] the mass f b - f a. This packages existence (a probability measure), the interval-mass formula, and uniqueness as a single statement.