Conditional expectations and Gaussian second moments of Brownian increments

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_Martingale

/-
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/MartingaleCondExp.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 ConditionalExpectations
variable {Ω : Type u} [MeasurableSpace Ω]
/-- The conditional expectation of a Brownian increment `W_t − W_s`, `0 ≤ s < t`, given a
σ-algebra `ℱ s` independent of it vanishes. -/
lemma condExp_increment_eq_zero_of_indep
    {P : Measure Ω} [IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : MeasureTheory.Filtration ℝ ‹MeasurableSpace Ω›)
    {s t : ℝ} (hs : 0 ≤ s) (hst : s < t)
    (hind : ProbabilityTheory.Indep (ℱ s)
      (MeasurableSpace.comap (fun ω => W.W t ω - W.W s ω) inferInstance) P) :
    P[(fun ω => W.W t ω - W.W s ω) | ℱ s] =ᵐ[P] fun _ => 0 := by
  have h_meas_diff : Measurable (fun ω => W.W t ω - W.W s ω) :=
    (W.measurable_eval t).sub (W.measurable_eval s)
  -- Integrability via Gaussian increment law.
  have h_int_id : MeasureTheory.Integrable (id : ℝ → ℝ)
      (ProbabilityTheory.gaussianReal 0 ⟨t - s, by linarith⟩) :=
    MeasureTheory.memLp_one_iff_integrable.mp
      (ProbabilityTheory.memLp_id_gaussianReal' 1 (by simp))
  have h_int : MeasureTheory.Integrable (fun ω => W.W t ω - W.W s ω) P := by
    have h_map := W.increment_gaussian hs hst
    have := (MeasureTheory.integrable_map_measure (g := (id : ℝ → ℝ))
      (by fun_prop : MeasureTheory.AEStronglyMeasurable id _)
      h_meas_diff.aemeasurable).mp (h_map ▸ h_int_id)
    simpa using this
  -- Mean zero via Gaussian mean.
  have h_mean : ∫ ω, (W.W t ω - W.W s ω) ∂P = 0 := by
    rw [show ∫ ω, (W.W t ω - W.W s ω) ∂P
          = ∫ x, x ∂(P.map (fun ω => W.W t ω - W.W s ω)) from
      (MeasureTheory.integral_map h_meas_diff.aemeasurable
        (by fun_prop : MeasureTheory.AEStronglyMeasurable (id : ℝ → ℝ) _)).symm]
    rw [W.increment_gaussian hs hst]
    exact ProbabilityTheory.integral_id_gaussianReal
  have hle₁ : MeasurableSpace.comap (fun ω => W.W t ω - W.W s ω) inferInstance
      ≤ ‹MeasurableSpace Ω› := by
    intro u ⟨v, hv, hvu⟩
    rw [← hvu]
    exact h_meas_diff hv
  have hf_sm : @MeasureTheory.StronglyMeasurable Ω ℝ _
      (MeasurableSpace.comap (fun ω => W.W t ω - W.W s ω) inferInstance)
      (fun ω => W.W t ω - W.W s ω) := by
    apply Measurable.stronglyMeasurable
    exact Measurable.of_comap_le le_rfl
  have h := MeasureTheory.condExp_indep_eq hle₁ (ℱ.le s) hf_sm hind.symm
  filter_upwards [h] with ω hω
  rw [hω]
  exact h_mean
/-- **Gaussian second moment.** `∫ x² ∂(gaussianReal 0 v) = v`. -/
lemma gaussianReal_second_moment (v : NNReal) :
    ∫ x : ℝ, x^2 ∂(ProbabilityTheory.gaussianReal 0 v) = v := by
  have h_var : ProbabilityTheory.variance (fun x : ℝ => x)
      (ProbabilityTheory.gaussianReal 0 v) = v :=
    ProbabilityTheory.variance_fun_id_gaussianReal
  rw [ProbabilityTheory.variance_eq_integral measurable_id'.aemeasurable] at h_var
  simp only [ProbabilityTheory.integral_id_gaussianReal, sub_zero] at h_var
  exact h_var
end ConditionalExpectations
end Martingale
end Brownian
end LevyStochCalc