structure BrownianMotion.IsBrownianMotion {d : ℕ} {Ω : Type u_1} {m : MeasurableSpace Ω} (B : NNReal → Ω → EuclideanSpace ℝ (Fin d)) (ℱ : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) : Prop

IsBrownianMotion B ℱ μ asserts that the family B : ℝ≥0 → Ω → E is a d-dimensional Brownian motion under μ adapted to the filtration ℱ. It packages the standard defining properties: B 0 = 0 almost surely, independent increments with respect to the filtration, adaptedness, almost-sure continuous paths, and measurability of each increment.

• zero : ∀ᵐ (ω : Ω) ∂μ, B 0 ω = 0
• indep_increment (s t : NNReal) : s ≤ t → ProbabilityTheory.Indep (↑ℱ s) (MeasurableSpace.comap (fun (ω : Ω) => B t ω - B s ω) inferInstance) μ
• adapted (t : NNReal) : Measurable (B t)
• continuous_path : ∀ᵐ (ω : Ω) ∂μ, Continuous fun (t : NNReal) => B t ω
• meas_increment (s t : NNReal) : s ≤ t → Measurable fun (ω : Ω) => B t ω - B s ω

def BrownianMotion.shiftPath {d : ℕ} {Ω : Type u_1} (B : NNReal → Ω → EuclideanSpace ℝ (Fin d)) (s : NNReal) : Ω → NNReal → EuclideanSpace ℝ (Fin d)

The time-shifted path of a Brownian motion: shiftPath B s ω is the function t ↦ B (s + t) ω, i.e. the path of B starting from time s instead of 0.

noncomputable def BrownianMotion.shiftedPathLaw {d : ℕ} {Ω : Type u_1} {m : MeasurableSpace Ω} (B : NNReal → Ω → EuclideanSpace ℝ (Fin d)) (μ : MeasureTheory.Measure Ω) (s : NNReal) : MeasureTheory.Measure (NNReal → EuclideanSpace ℝ (Fin d))

The law on path space of the centered shifted path t ↦ B (s + t) ω - B s ω. By independence and stationarity of Brownian increments, this measure does not depend on s and equals the law of standard Brownian motion.

noncomputable def BrownianMotion.pathExpectation {d : ℕ} {Ω : Type u_1} {m : MeasurableSpace Ω} (B : NNReal → Ω → EuclideanSpace ℝ (Fin d)) (μ : MeasureTheory.Measure Ω) (s : NNReal) (Y : (NNReal → EuclideanSpace ℝ (Fin d)) → ℝ) (x : EuclideanSpace ℝ (Fin d)) : ℝ

The expectation of a path functional Y under the law of Brownian motion started from the point x ∈ E. Operationally, it integrates Y (t ↦ x + f t) against the law of the centered shifted path f. This is the function φ(x) = E_x Y that appears as the conditional expectation in the Markov property.

theorem BrownianMotion.setIntegral_shift_eq_pathExpectation {d : ℕ} {Ω : Type u_1} {m : MeasurableSpace Ω} {B : NNReal → Ω → EuclideanSpace ℝ (Fin d)} {ℱ : MeasureTheory.Filtration NNReal m} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hB : IsBrownianMotion B ℱ μ) (s : NNReal) (Y : (NNReal → EuclideanSpace ℝ (Fin d)) → ℝ) (hY_meas : Measurable Y) (hY_bdd : ∃ (C : ℝ), ∀ (f : NNReal → EuclideanSpace ℝ (Fin d)), |Y f| ≤ C) (A : Set Ω) (hA : MeasurableSet A) : ∫ (ω : Ω) in A, Y (shiftPath B s ω) ∂μ = ∫ (ω : Ω) in A, pathExpectation B μ s Y (B s ω) ∂μ

Set-integral form of the Markov property for Brownian motion: for any bounded measurable path functional Y and any event A ∈ ℱ s,

∫_A Y (shiftPath B s ω) dμ = ∫_A pathExpectation B μ s Y (B s ω) dμ.

theorem BrownianMotion.markov_property_condExp {d : ℕ} {Ω : Type u_1} {m : MeasurableSpace Ω} {B : NNReal → Ω → EuclideanSpace ℝ (Fin d)} {ℱ : MeasureTheory.Filtration NNReal m} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (hB : IsBrownianMotion B ℱ μ) (s : NNReal) (Y : (NNReal → EuclideanSpace ℝ (Fin d)) → ℝ) (hY_meas : Measurable Y) (hY_bdd : ∃ (C : ℝ), ∀ (f : NNReal → EuclideanSpace ℝ (Fin d)), |Y f| ≤ C) (hg_int : MeasureTheory.Integrable (fun (ω : Ω) => pathExpectation B μ s Y (B s ω)) μ) (hg_meas : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => pathExpectation B μ s Y (B s ω)) μ) : μ[fun (ω : Ω) => Y (shiftPath B s ω) | ↑ℱ s] =ᵐ[μ] fun (ω : Ω) => pathExpectation B μ s Y (B s ω)

Markov property for Brownian motion (conditional-expectation form). For any bounded measurable path functional Y and any s ≥ 0,

E[Y(shiftPath B s ·) | ℱ s] = E_{B s} Y μ-a.e.,

where E_x Y := pathExpectation B μ s Y x is the expectation of Y under Brownian motion started at x. This is the formalization of the textbook Markov property E_x(Y ∘ θ_s | ℱ_s⁺) = E_{B_s} Y.