Theorems · Theorem · probability

ProbabilityTheory.IsPreBrownianReal.shift

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.IsPreBrownianReal B P →
    ∀ (t₀ : NNReal), ProbabilityTheory.IsPreBrownianReal (fun t ω => B (t₀ + t) ω - B t₀ ω) P

Weak Markov property: If B is a pre-Brownian motion, then t ↦ B (t₀ + t) - B t₀ is a pre-Brownian motion which is independent from (B t, t ≤ t₀). This is the proof that it is pre-Brownian, see IsPreBrownianReal.indepFun_shift for independence.

Defined in

Mathlib.Probability.BrownianMotion.Basic

Cited by

1 results in Mathlib

Foundations

Depth 324 from the axioms · uses propext, Classical.choice, Quot.sound