Natural filtration and Brownian integrability

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_Continuity
import Definitions.Def_KLSModular_LevyStochCalc_Martingale_RightCont
import Mathlib.Probability.Martingale.Basic
import Mathlib.Probability.ConditionalExpectation

/-
Copyright (c) 2026 Christian Garry. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Christian Garry
-/
-- Modified 2026-10-12 by the KLS formalization project: ported to Lean v4.33.0 and
-- Mathlib db584cd. The changes are listed in vendor/README.md and vendor/port.patch.
-- Vendored from https://github.com/cgarryZA/LevyStochCalc at commit 984dbf0b790031eac05d56fe5a84b65e15e1e932 (upstream path LevyStochCalc/Brownian/Martingale.lean; Apache-2.0; locally patched, see formalization/vendor/port.patch; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
open MeasureTheory ProbabilityTheory
open scoped NNReal ENNReal
namespace LevyStochCalc
namespace Brownian
namespace Martingale
universe u
section Moments
variable {Ω : Type u} [MeasurableSpace Ω]
/-- The *natural filtration* of a Brownian motion `W`. -/
noncomputable def naturalFiltration
    {P : Measure Ω} [IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P) :
    MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω› :=
  MeasureTheory.Filtration.natural W.W (fun t => (W.measurable_eval t).stronglyMeasurable)
/-- **Integrability of a Brownian-motion value at any `s : ℝ`.** Uses the
Gaussian distribution of `W_s` (for `s ≥ 0`) or the `negative_zero` extension
(for `s < 0`). -/
lemma brownianMotion_integrable
    {P : Measure Ω} [IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    (s : ℝ) :
    MeasureTheory.Integrable (W.W s) P := by
  by_cases hs_neg : s < 0
  · -- s < 0: W_s = 0 a.s.
    refine ⟨(W.measurable_eval s).aestronglyMeasurable, ?_⟩
    rw [MeasureTheory.hasFiniteIntegral_iff_enorm]
    have h_nn : ∀ᵐ ω ∂P, ‖W.W s ω‖ₑ = 0 := by
      filter_upwards [W.negative_zero s hs_neg] with ω hω
      rw [hω]; simp
    rw [MeasureTheory.lintegral_congr_ae h_nn]
    simp
  push Not at hs_neg
  -- s ≥ 0
  have hs := hs_neg
  by_cases hs_zero : s = 0
  · subst hs_zero
    refine ⟨(W.measurable_eval 0).aestronglyMeasurable, ?_⟩
    rw [MeasureTheory.hasFiniteIntegral_iff_enorm]
    have h_nn : ∀ᵐ ω ∂P, ‖W.W 0 ω‖ₑ = 0 := by
      filter_upwards [W.initial_zero] with ω hω
      rw [hω]; simp
    rw [MeasureTheory.lintegral_congr_ae h_nn]
    simp
  · have hs_pos : 0 < s := lt_of_le_of_ne hs (Ne.symm hs_zero)
    have h_eq : (fun ω => W.W s ω) =ᵐ[P] fun ω => W.W s ω - W.W 0 ω := by
      filter_upwards [W.initial_zero] with ω hω
      rw [hω]; ring
    have h_map : P.map (fun ω => W.W s ω)
        = ProbabilityTheory.gaussianReal 0 ⟨s, hs⟩ := by
      rw [MeasureTheory.Measure.map_congr h_eq]
      have := W.increment_gaussian (le_refl 0) hs_pos
      simpa using this
    have h_int_id : MeasureTheory.Integrable (id : ℝ → ℝ)
        (ProbabilityTheory.gaussianReal 0 ⟨s, hs⟩) :=
      MeasureTheory.memLp_one_iff_integrable.mp
        (ProbabilityTheory.memLp_id_gaussianReal' 1 (by simp))
    have := (MeasureTheory.integrable_map_measure (g := (id : ℝ → ℝ))
      (by fun_prop : MeasureTheory.AEStronglyMeasurable id _)
      (W.measurable_eval s).aemeasurable).mp (h_map ▸ h_int_id)
    simpa using this
end Moments
end Martingale
end Brownian
end LevyStochCalc