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

IsBrownianMotion d B 𝓕 μ x says that B : NNReal → Ω → (Fin d → ℝ) is a d-dimensional Brownian motion started at x under the probability measure μ, adapted to the filtration 𝓕. The defining properties are: μ is a probability measure, B 0 = x a.s., B t is 𝓕 t-measurable in each coordinate, increments B t - B s (for s ≤ t) are independent of 𝓕 s and Gaussian with variance t - s, and the paths t ↦ B t ω are a.s. continuous.

• isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure μ
• start : ∀ᵐ (ω : Ω) ∂μ, B 0 ω = x
• adapted (t : NNReal) (i : Fin d) : Measurable fun (ω : Ω) => B t ω i
• indep_incr (s t : NNReal) : s ≤ t → ProbabilityTheory.Indep (MeasurableSpace.comap (fun (ω : Ω) => B t ω - B s ω) inferInstance) (↑𝓕 s) μ
• gaussian_incr (s t : NNReal) (h : s ≤ t) (i : Fin d) : MeasureTheory.Measure.map (fun (ω : Ω) => B t ω i - B s ω i) μ = ProbabilityTheory.gaussianReal 0 ⟨↑t - ↑s, ⋯⟩
• continuous_path : ∀ᵐ (ω : Ω) ∂μ, Continuous fun (t : NNReal) => B t ω

theorem BrownianFiltration.brownian_condExp_equivalence {Ω : Type u_2} {m : MeasurableSpace Ω} {d : ℕ} (B : NNReal → Ω → Fin d → ℝ) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : Fin d → ℝ) (_hBM : IsBrownianMotion d B 𝓕 μ x) (Z : Ω → ℝ) (s : NNReal) (hZ_meas : Measurable Z) (hZ_bdd : ∃ (C : ℝ), ∀ (ω : Ω), |Z ω| ≤ C) : μ[Z | ↑𝓕.rightCont s] =ᵐ[μ] μ[Z | ↑𝓕 s]

Expectation equivalence theorem (Brownian-motion version). For a Brownian motion B with filtration 𝓕, bounded measurable conditional expectations against the right-continuous augmentation 𝓕.rightCont s agree a.s. with those against 𝓕 s: μ[Z | 𝓕.rightCont s] =ᵐ[μ] μ[Z | 𝓕 s].

theorem BrownianFiltration.brownian_filtration_rightCont {Ω : Type u_2} {m : MeasurableSpace Ω} {d : ℕ} (B : NNReal → Ω → Fin d → ℝ) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : Fin d → ℝ) (_hBM : IsBrownianMotion d B 𝓕 μ x) : 𝓕.IsRightContinuous

The filtration generated by a Brownian motion is right-continuous, i.e. 𝓕 s = ⋂_{t > s} 𝓕 t.

theorem condExp_rightCont_eq_condExp {Ω : Type u_1} {m : MeasurableSpace Ω} {d : ℕ} (B : NNReal → Ω → Fin d → ℝ) (𝓕 : MeasureTheory.Filtration NNReal m) (μ : MeasureTheory.Measure Ω) (x : Fin d → ℝ) (hBM : BrownianFiltration.IsBrownianMotion d B 𝓕 μ x) (Z : Ω → ℝ) (s : NNReal) (hZ_meas : Measurable Z) (hZ_bdd : ∃ (C : ℝ), ∀ (ω : Ω), |Z ω| ≤ C) : μ[Z | ↑𝓕.rightCont s] =ᵐ[μ] μ[Z | ↑𝓕 s]

Expectation equivalence theorem. For a bounded measurable Z and a Brownian motion B with filtration 𝓕, the conditional expectation with respect to the right-continuous augmented filtration coincides almost surely with the conditional expectation with respect to 𝓕 s: E_x(Z | 𝓕.rightCont s) =ᵐ[μ] E_x(Z | 𝓕 s).