Weak convergence in the space of continuous functions

TheoremContinuous-path laws are determined by finite-dimensional marginals#✓fully proved

Probability measures on continuous real paths over [0, T] are determined by all of their finite evaluation pushforwards. The empty Finset is included, and repeated coordinates are identified by Finset.

theorem continuousPath_measure_ext_of_finset_eval (T : ℝ)
    (μ ν : ProbabilityMeasure C(Set.Icc (0 : ℝ) T, ℝ))
    (h : ∀ I : Finset (Set.Icc (0 : ℝ) T),
      μ.map (fun f => I.restrict (fun t => f t)) =
        ν.map (fun f => I.restrict (fun t => f t))) :
    μ = ν

Used by 2

Used byFinite-dimensional distributions determine laws on \(C((0,1))\) · Tightness plus finite-dimensional convergence gives weak convergence

TheoremTightness plus finite-dimensional convergence gives weak convergence#✓fully proved

Let T > 0. A tight sequence of probability laws on C(Set.Icc 0 T, ℝ) converges weakly to μ in the uniform topology if every finite evaluation pushforward converges weakly to the corresponding pushforward of μ.

This is a condition-to-convergence criterion, not a process convergence theorem: applications must separately prove tightness and all finite-dimensional convergences for their constructed laws.

MathlibExt.Probability.ContinuousPathConvergence.tendsto_continuousPath_of_tight_of_finset_eval · 16 lines

theorem tendsto_continuousPath_of_tight_of_finset_eval (T : ℝ) (_hT : 0 < T)
    (μs : ℕ → ProbabilityMeasure C(Set.Icc (0 : ℝ) T, ℝ))
    (μ : ProbabilityMeasure C(Set.Icc (0 : ℝ) T, ℝ))
    (htight : IsTightMeasureSet
      {((ν : ProbabilityMeasure C(Set.Icc (0 : ℝ) T, ℝ)) :
        Measure C(Set.Icc (0 : ℝ) T, ℝ)) | ν ∈ Set.range μs})
    (hfdd : ∀ I : Finset (Set.Icc (0 : ℝ) T),
      Tendsto
        (fun n => (μs n).map
          (fun f : C(Set.Icc (0 : ℝ) T, ℝ) =>
            I.restrict (fun t => f t)))
        atTop
        (𝓝 (μ.map
          (fun f : C(Set.Icc (0 : ℝ) T, ℝ) =>
            I.restrict (fun t => f t))))) :
    Tendsto μs atTop (𝓝 μ)

Uses 1 · Used by 1

Proof usesContinuous-path laws are determined by finite-dimensional marginals

Used byDonsker's invariance principle

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.