Skip to content

Continuous mapping theorem

2 fully proved

Probability Theory

TheoremContinuous mapping theorem, integral form#✓fully proved

Let \(\mu_n\) (\(n \in \mathbb{N}\)) and \(\mu\) be probability measures on \(\mathbb{R}\), let \(g : \mathbb{R} \to \mathbb{R}\) be a measurable function whose set of discontinuity points has \(\mu\)-measure zero, and write \(\nu \circ g^{-1}\) for the pushforward of a measure \(\nu\) on \(\mathbb{R}\) under \(g\). If \(\int f \, d\mu_n \to \int f \, d\mu\) as \(n \to \infty\) for every bounded continuous function \(f : \mathbb{R} \to \mathbb{R}\), then \(\int f \, d(\mu_n \circ g^{-1}) \to \int f \, d(\mu \circ g^{-1})\) as \(n \to \infty\) for every bounded continuous function \(f : \mathbb{R} \to \mathbb{R}\).

theorem continuous_mapping
    (μs : ℕ → Measure ℝ) [∀ n, IsProbabilityMeasure (μs n)]
    (μ : Measure ℝ) [IsProbabilityMeasure μ]
    (g : ℝ → ℝ) (hg_meas : Measurable g)
    (hg_ae : μ {x | ¬ContinuousAt g x} = 0)
    (hconv : ∀ f : ℝ →ᵇ ℝ,
      Tendsto (fun n ↦ ∫ x, f x ∂(μs n)) atTop (𝓝 (∫ x, f x ∂μ))) :
    ∀ f : ℝ →ᵇ ℝ,
      Tendsto (fun n ↦ ∫ x, f x ∂((μs n).map g)) atTop
        (𝓝 (∫ x, f x ∂(μ.map g)))
Sources
  • Lecture 12, continuous mapping theorem.
Used by 1
Used byContinuous mapping theorem for weak convergence of probability measures

Measure Theory

TheoremContinuous mapping theorem for weak convergence of probability measures#✓fully proved

Let \(\mu_n\) (\(n \in \mathbb{N}\)) and \(\mu\) be probability measures on \(\mathbb{R}\), and let \(g : \mathbb{R} \to \mathbb{R}\) be a measurable function whose set of discontinuity points has \(\mu\)-measure zero. If \(\mu_n\) converges weakly to \(\mu\) as \(n \to \infty\), then the pushforward probability measures \(\mu_n \circ g^{-1}\) converge weakly to \(\mu \circ g^{-1}\).

This generalizes the case where \(g\) is continuous everywhere, which is already in Mathlib.

theorem ProbabilityMeasure.tendsto_map_of_tendsto_of_ae_continuous
    {μs : ℕ → ProbabilityMeasure ℝ} {μ : ProbabilityMeasure ℝ}
    {g : ℝ → ℝ} (hg_meas : Measurable g)
    (hg_ae : (μ : Measure ℝ) {x | ¬ContinuousAt g x} = 0)
    (hconv : Tendsto μs atTop (𝓝 μ)) :
    Tendsto (fun n ↦ (μs n).map g) atTop (𝓝 (μ.map g))
Sources
  • Lecture 12, continuous mapping theorem.
Uses 1
Proof usesContinuous mapping theorem, integral form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.