Brownian Natural Filtration Independent of Future Increments

This is the sigma-algebra form of the weak Markov property for Brownian motion.

Let $(\Omega,\mathcal F,P)$ be a probability space, let $W$ be a BrownianMotion, and let $s\in\mathbb R$ satisfy $0\le s$. Define the natural filtration at time $s$ by

and define the future-increment sigma-algebra by

Then

The statement includes the entire natural filtration, including the almost-surely constant negative-time part, and the sigma-algebra generated jointly by all increments after $s$. It is a reusable filtration-level strengthening of independence for individual Brownian increments.

Original Lean declaration header

Within namespace LevyStochCalc.Brownian.BrownianMotion. Shown in its original module context. Proof omitted.

theorem indep_naturalFiltration_future (W : BrownianMotion P) {s : ℝ} (hs : 0 ≤ s) :
    Indep (Martingale.naturalFiltration W s)
      (⨆ t ∈ Set.Ioi s, MeasurableSpace.comap (fun ω => W.W t ω - W.W s ω) inferInstance) P

Module navigation

Module: LevyStochCalc/Brownian/FutureIndependence.

Definition modules: LevyStochCalc/Brownian/Construction, LevyStochCalc/Brownian/Martingale.

Supporting theorems: hasIndepIncrements, hasLaw_eval, IsTrivialSigma.indep, indep_sup_left_of_indep, isTrivialSigma_comap_of_ae_const.

Source excerpt, lines 45–47 · Frozen source 408915f.