Brownian motion relative to a filtration

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_FutureIndependence
import Definitions.Def_KLSModular_LevyStochCalc_Brownian_MartingaleCondExp
import Definitions.Def_KLSModular_LevyStochCalc_Probability_ComapTuple
import Definitions.Def_KLSModular_LevyStochCalc_Probability_IndepJoin
import Definitions.Def_KLSModular_LevyStochCalc_Probability_IndepLimit

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/Filtered.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory Filter Topology
namespace LevyStochCalc
namespace Brownian
universe u
variable {Ω : Type u} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
/-- `W` is a Brownian motion for the filtration `ℱ`: it is adapted, and for `0 ≤ s` the
σ-algebra `ℱ s` is independent of the σ-algebra generated by the increments `W t − W s`,
`t > s`. -/
structure IsBrownianFiltration (W : BrownianMotion P) (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) :
    Prop where
  measurable : ∀ t, Measurable[ℱ t] (W.W t)
  indep_future : ∀ ⦃s : ℝ⦄, 0 ≤ s →
    Indep (ℱ s) (⨆ t ∈ Set.Ioi s,
      MeasurableSpace.comap (fun ω => W.W t ω - W.W s ω) inferInstance) P
/-- The σ-algebra `ℱ s` is independent of a single increment `W t − W s`, `0 ≤ s < t`. -/
theorem IsBrownianFiltration.indep {W : BrownianMotion P}
    {ℱ : Filtration ℝ ‹MeasurableSpace Ω›} (h : IsBrownianFiltration W ℱ) :
    ∀ ⦃s t : ℝ⦄, 0 ≤ s → s < t →
      Indep (ℱ s) (MeasurableSpace.comap (fun ω => W.W t ω - W.W s ω) inferInstance) P :=
  fun _ t hs hst => indep_of_indep_of_le_right (h.indep_future hs)
    (le_iSup₂_of_le t (Set.mem_Ioi.mpr hst) le_rfl)
namespace IsBrownianFiltration
variable {W : BrownianMotion P} {ℱ : Filtration ℝ ‹MeasurableSpace Ω›}
/-- `W_t` is `ℱ t`-strongly measurable. -/
theorem stronglyMeasurable (h : IsBrownianFiltration W ℱ) (t : ℝ) :
    StronglyMeasurable[ℱ t] (W.W t) :=
  (h.measurable t).stronglyMeasurable
/-- The conditional expectation of the increment `W_t − W_s`, `0 ≤ s < t`, given `ℱ s`
vanishes. -/
theorem condExp_increment_eq_zero (h : IsBrownianFiltration W ℱ) {s t : ℝ} (hs : 0 ≤ s)
    (hst : s < t) : P[(fun ω => W.W t ω - W.W s ω) | ℱ s] =ᵐ[P] fun _ => 0 :=
  Martingale.condExp_increment_eq_zero_of_indep W ℱ hs hst (h.indep hs hst)
/-- The martingale identity `E[W_t | ℱ s] = W_s` for `0 ≤ s ≤ t`. -/
theorem condExp_eq (h : IsBrownianFiltration W ℱ) {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) :
    P[W.W t | ℱ s] =ᵐ[P] W.W s := by
  have h_int_s := Martingale.brownianMotion_integrable W s
  rcases hst.eq_or_lt with rfl | hlt
  · rw [condExp_of_stronglyMeasurable (ℱ.le s) (h.stronglyMeasurable s) h_int_s]
  · have h_int_t := Martingale.brownianMotion_integrable W t
    have h_decomp : (W.W t : Ω → ℝ) = W.W s + (W.W t - W.W s) := by
      funext ω; simp
    rw [h_decomp]
    filter_upwards [condExp_add h_int_s (h_int_t.sub h_int_s) (ℱ s),
      h.condExp_increment_eq_zero hs hlt] with ω h_add h_zero
    rw [h_add, Pi.add_apply,
      condExp_of_stronglyMeasurable (ℱ.le s) (h.stronglyMeasurable s) h_int_s]
    change W.W s ω + P[(fun ω => W.W t ω - W.W s ω) | ℱ s] ω = W.W s ω
    rw [h_zero, add_zero]
end IsBrownianFiltration
end Brownian
end LevyStochCalc