Probability measures from distribution functions

TheoremConstruction of measures on ℝ#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be a Stieltjes function, that is, non-decreasing and right-continuous, with \(f(x) \to 0\) as \(x \to -\infty\) and \(f(x) \to 1\) as \(x \to \infty\), and let \(\mu_f\) be its Stieltjes measure on \(\mathbb{R}\). Then \(\mu_f\) is a probability measure, \(\mu_f((a, b]) = f(b) - f(a)\) for all real \(a \le b\), and every finite measure \(\nu\) on \(\mathbb{R}\) with \(\nu((a, b]) = f(b) - f(a)\) for all real \(a \le b\) equals \(\mu_f\).

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

Used by 1

Used byConstruction of measures on ℝ, as unique existence

TheoremConstruction of measures on ℝ, as unique existence#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{R}\) be a Stieltjes function, that is, non-decreasing and right-continuous, with \(f(x) \to 0\) as \(x \to -\infty\) and \(f(x) \to 1\) as \(x \to \infty\). Then there is exactly one measure \(\mu\) on \(\mathbb{R}\) that is a probability measure and satisfies \(\mu((a, b]) = f(b) - f(a)\) for all real \(a \le b\).

theorem exists_unique_probabilityMeasure_of_stieltjes (f : StieltjesFunction ℝ)
    (hf_bot : Tendsto f atBot (𝓝 0)) (hf_top : Tendsto f atTop (𝓝 1)) :
    ∃! μ : Measure ℝ, IsProbabilityMeasure μ ∧
      ∀ a b : ℝ, a ≤ b → μ (Ioc a b) = ENNReal.ofReal (f b - f a)

Uses 1

Proof usesConstruction of measures on ℝ

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.