@[reducible, inline]

abbrev StrongMarkovBMGoal98.Rd (d : ℕ) : Type

Abbreviation for d-dimensional Euclidean space ℝ^d, represented as functions Fin d → ℝ.

structure StrongMarkovBMGoal98.IsBrownianMotion {Ω : Type u_1} {m : MeasurableSpace Ω} {d : ℕ} (B : NNReal → Ω → Rd d) (ℱ : MeasureTheory.Filtration NNReal m) (P : Rd d → MeasureTheory.Measure Ω) : Prop

Predicate bundling the defining properties of a d-dimensional Brownian motion B with respect to a filtration ℱ and a family P : Rd d → Measure Ω of starting-point laws. The fields encode: starting at x under P x, Gaussian increments with the correct variance, independence of increments from the past, adaptedness to ℱ, that each P x is a probability measure, measurability in the starting point, and almost-sure continuity of sample paths.

• start (x : Rd d) : ∀ᵐ (ω : Ω) ∂P x, B 0 ω = x
• increment_dist (x : Rd d) (i : Fin d) (s t : NNReal) : s ≤ t → MeasureTheory.Measure.map (fun (ω : Ω) => B t ω i - B s ω i) (P x) = ProbabilityTheory.gaussianReal 0 (t - s)
• indep_increment (x : Rd d) (i : Fin d) (s t : NNReal) : s ≤ t → ProbabilityTheory.Indep (↑ℱ s) (MeasurableSpace.comap (fun (ω : Ω) => B t ω i - B s ω i) inferInstance) (P x)
• adapted (t : NNReal) : Measurable (B t)
• isProbMeasure (x : Rd d) : MeasureTheory.IsProbabilityMeasure (P x)
• measurable_P : Measurable P
• continuous_path (x : Rd d) : ∀ᵐ (ω : Ω) ∂P x, ∀ (i : Fin d), Continuous fun (t : NNReal) => B t ω i

def StrongMarkovBMGoal98.pathShiftAtStopping {Ω : Type u_1} {d : ℕ} (B : NNReal → Ω → Rd d) (S : Ω → ENNReal) (ω : Ω) : NNReal → Rd d

The path of B shifted by the (possibly infinite) stopping time S: at sample ω returns the path t ↦ B (S ω + t) ω.

noncomputable def StrongMarkovBMGoal98.bmExpectation {Ω : Type u_1} {m : MeasurableSpace Ω} {d : ℕ} (B : NNReal → Ω → Rd d) (P : Rd d → MeasureTheory.Measure Ω) (Y : NNReal → (NNReal → Rd d) → ℝ) (t : NNReal) (x : Rd d) : ℝ

The function (t, x) ↦ E_x[Y t (B_·)]: integrating the time-indexed path functional Y against the Brownian motion law started from x.

theorem StrongMarkovBMGoal98.strong_markov_setIntegral_eq {Ω : Type u_2} {m : MeasurableSpace Ω} {d : ℕ} {B : NNReal → Ω → Rd d} {ℱ : MeasureTheory.Filtration NNReal m} {P : Rd d → MeasureTheory.Measure Ω} (hBM : IsBrownianMotion B ℱ P) (x : Rd d) [MeasureTheory.IsProbabilityMeasure (P x)] (S : Ω → ENNReal) (hS_stop : MeasureTheory.IsStoppingTime ℱ S) (Y : NNReal → (NNReal → Rd d) → ℝ) (hY_meas : Measurable fun (p : NNReal × (NNReal → Rd d)) => Y p.1 p.2) (hY_bdd : ∃ (C : ℝ), ∀ (t : NNReal) (f : NNReal → Rd d), |Y t f| ≤ C) (A : Set Ω) (hA : MeasurableSet A) (hA_finite : (P x) A < ⊤) : ∫ (ω : Ω) in A, Y (S ω).toNNReal (pathShiftAtStopping B S ω) ∂P x = ∫ (ω : Ω) in A, bmExpectation B P Y (S ω).toNNReal (B (S ω).toNNReal ω) ∂P x

Strong Markov property for Brownian motion, set-integral form (Lecture 39). For any event A in the stopping-time σ-algebra ℱ_S, the integral over A of the bounded measurable path functional Y evaluated on the shifted path equals the integral over A of E_{B(S)} Y evaluated at the current state, expressing E_x(Y_S ∘ θ_S | ℱ_S) = E_{B(S)} Y_S on {S < ∞} in integrated form.

theorem StrongMarkovBMGoal98.bmExpectation_measurable {Ω : Type u_2} {m : MeasurableSpace Ω} {d : ℕ} {B : NNReal → Ω → Rd d} {ℱ : MeasureTheory.Filtration NNReal m} {P : Rd d → MeasureTheory.Measure Ω} (hBM : IsBrownianMotion B ℱ P) (Y : NNReal → (NNReal → Rd d) → ℝ) (hY_meas : Measurable fun (p : NNReal × (NNReal → Rd d)) => Y p.1 p.2) (_hY_bdd : ∃ (C : ℝ), ∀ (t : NNReal) (f : NNReal → Rd d), |Y t f| ≤ C) : Measurable fun (p : NNReal × Rd d) => bmExpectation B P Y p.1 p.2

Helper measurability lemma: the map (t, x) ↦ E_x[Y t (B_·)] is jointly measurable in time and starting point, given that Y is bounded measurable and P is measurable in x.

theorem StrongMarkovBMGoal98.adapted_process_stoppingTime_measurable {Ω : Type u_2} {m : MeasurableSpace Ω} {d : ℕ} {B : NNReal → Ω → Rd d} {ℱ : MeasureTheory.Filtration NNReal m} {P : Rd d → MeasureTheory.Measure Ω} (hBM : IsBrownianMotion B ℱ P) (S : Ω → ENNReal) (hS_stop : MeasureTheory.IsStoppingTime ℱ S) : Measurable fun (ω : Ω) => B (S ω).toNNReal ω

For an adapted process B (here a Brownian motion) and a stopping time S, the random variable ω ↦ B (S ω) ω is measurable with respect to the stopping-time σ-algebra ℱ_S.

theorem StrongMarkovBMGoal98.stopping_time_pair_measurable {Ω : Type u_2} {m : MeasurableSpace Ω} {d : ℕ} {B : NNReal → Ω → Rd d} {ℱ : MeasureTheory.Filtration NNReal m} {P : Rd d → MeasureTheory.Measure Ω} (hBM : IsBrownianMotion B ℱ P) (S : Ω → ENNReal) (hS_stop : MeasureTheory.IsStoppingTime ℱ S) : Measurable fun (ω : Ω) => ((S ω).toNNReal, B (S ω).toNNReal ω)

The pair ω ↦ (S ω, B (S ω) ω) consisting of the stopping time and the position of the Brownian motion at the stopping time is measurable with respect to ℱ_S.