Canonical Gaussian Brownian motion extends to the established real-time Brownian structure

Proved

AvramDividend.Classical.canonical_brownian_realTime_bridge

by WillR · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

brownian-motioncounterexample-auditlevy-processesreal-time-extension

On the canonical Gaussian projective-limit probability space, there exists a real-time BrownianMotion whose nonnegative-time coordinates equal the canonical continuous modification normalised by its time-zero value, pathwise. This bridge permits reuse of already proved Gaussian increments and filtration independence when constructing a drifted spectrally negative Lévy process.

Preamble

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_Existence
import Theorems.Thm_ProbabilityTheory_isBrownianReal_brownian_avram
import Theorems.Thm_ProbabilityTheory_IsPreBrownianReal_memHolder_mk_avram
import Mathlib.Tactic

open MeasureTheory ProbabilityTheory NNReal Filter
open scoped NNReal

Formal statement

theorem AvramDividend.Classical.canonical_brownian_realTime_bridge :
    ∃ W : LevyStochCalc.Brownian.BrownianMotion gaussianLimit,
      ∀ (t : ℝ≥0) (ω : ℝ≥0 → ℝ),
        W.W (t : ℝ) ω = brownian t ω - brownian 0 ω := by sorry

Source

Vendored LevyStochCalc BrownianMotion.ofIsPreBrownianReal and accepted canonical Brownian IsBrownianReal and Hölder regularity.

View graph