def BrownianMotion.stoppedShiftedProcess {Ω : Type u_1} (B : NNReal → Ω → ℝ) (T : Ω → ENNReal) : NNReal → Ω → ℝ

The process obtained from B by shifting time by the stopping time T and recentering at B(T): t ↦ B(T + t) - B(T).

theorem strong_markov_property_bm {Ω : Type u_1} {m : MeasurableSpace Ω} {B : NNReal → Ω → ℝ} {ℱ : MeasureTheory.Filtration NNReal m} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hB_zero : ∀ᵐ (ω : Ω) ∂μ, B 0 ω = 0) (hB_indep : ∀ (s t : NNReal), s ≤ t → ProbabilityTheory.Indep (↑ℱ s) (MeasurableSpace.comap (fun (ω : Ω) => B t ω - B s ω) inferInstance) μ) (hB_cont : ∀ᵐ (ω : Ω) ∂μ, Continuous fun (t : NNReal) => B t ω) (T : Ω → ENNReal) (hT_stop : IsStoppingTimeContinuous ℱ T) (hT_fin : ∀ᵐ (ω : Ω) ∂μ, T ω < ⊤) : (∀ (t : NNReal), ProbabilityTheory.Indep (MeasureTheory.IsStoppingTime.measurableSpace hT_stop) (MeasurableSpace.comap (BrownianMotion.stoppedShiftedProcess B T t) inferInstance) μ) ∧ (∀ᵐ (ω : Ω) ∂μ, BrownianMotion.stoppedShiftedProcess B T 0 ω = 0) ∧ (∀ (s t : NNReal), s ≤ t → MeasureTheory.Measure.map (fun (ω : Ω) => BrownianMotion.stoppedShiftedProcess B T t ω - BrownianMotion.stoppedShiftedProcess B T s ω) μ = ProbabilityTheory.gaussianReal 0 (t - s)) ∧ ∀ᵐ (ω : Ω) ∂μ, Continuous fun (t : NNReal) => BrownianMotion.stoppedShiftedProcess B T t ω

Strong Markov property for Brownian motion (Lecture 39). Given a real-valued Brownian motion B adapted to ℱ with B 0 = 0, independent Gaussian increments and continuous paths, and an almost-surely finite stopping time T, the shifted/recentered process t ↦ B(T + t) - B(T) is independent of ℱ_T, starts at 0, has the same Gaussian increment distribution as B, and has continuous paths almost surely.