Isometry and right-continuity of the completed Brownian Itô integral

import Definitions.Def_KLSModular_LevyStochCalc_Brownian_ItoL2CompletionMaster

/-
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/ItoL2CompletionQuadVar.lean; Apache-2.0; provenance in formalization/vendor/vendor-lock.json of the KLS repository)
namespace LevyStochCalc
namespace Brownian
namespace Ito
open MeasureTheory
open scoped NNReal ENNReal
universe u
variable {Ω : Type u} [MeasurableSpace Ω]
section MasterSequence
variable
    {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
    (W : LevyStochCalc.Brownian.BrownianMotion P)
    (ℱ : Filtration ℝ ‹MeasurableSpace Ω›) (hℱ : IsBrownianFiltration W ℱ)
    (H : Ω → ℝ → ℝ) (h_meas : Measurable (Function.uncurry H))
    (h_progMeas : Probability.ProgressivelyMeasurable ℱ H)
    (h_sq_int_global : ∀ T, 0 < T →
      ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
        (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P < ⊤)
include hℱ in
/-- **Conjunct 3: the L²-isometry** `∫⁻‖F T‖² = ∫⁻∫⁻_{[0,T]}‖H‖²` for `T > 0`.
The squared `L²`-norm of `Iₙ(T)` equals `∫⁻∫⁻_{[0,T]}‖Gₙ.eval‖²` (intermediate
isometry), converges to `∫⁻‖F T‖²` (norm continuity of the `L²`-limit) and to
`∫⁻∫⁻_{[0,T]}‖H‖²` (`masterApprox_evalNorm_tendsto`); uniqueness of limits. -/
lemma isometry_stochasticIntegralBrownian {T : ℝ} (hT : 0 < T) :
    ∫⁻ ω, (‖stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas
      h_sq_int_global T ω‖₊ : ℝ≥0∞) ^ 2 ∂P
      = ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T, (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P := by
  haveI : Fact ((1 : ℝ≥0∞) ≤ 2) := ⟨by norm_num⟩
  set Flp := stochasticIntegralBrownianLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global T with hFlp
  have htend : Filter.Tendsto (fun n => masterLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global T n)
      Filter.atTop (nhds Flp) :=
    (masterLp_cauchySeq W ℱ hℱ H h_meas h_progMeas h_sq_int_global (le_of_lt hT)).tendsto_limUnder
  have hn := (htend.enorm).ennrpow_const 2
  simp only [MeasureTheory.Lp.enorm_def] at hn
  -- limit `eLpNorm ↑↑Flp ^ 2 = ∫⁻‖F T‖²`
  have hlim : MeasureTheory.eLpNorm (↑↑Flp : Ω → ℝ) 2 P ^ (2 : ℝ)
      = ∫⁻ ω, (‖stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas
        h_sq_int_global T ω‖₊ : ℝ≥0∞) ^ 2 ∂P := by
    rw [eLpNorm_sq_eq_lintegral_nnnorm_sq]
    refine lintegral_congr_ae ?_
    filter_upwards [stochasticIntegralBrownian_ae_eq W ℱ hℱ H h_meas h_progMeas h_sq_int_global T]
      with ω hF
    rw [hF]
  rw [hlim] at hn
  have h_a : Filter.Tendsto (fun n => ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) T,
        (‖(masterApprox ℱ H h_meas h_progMeas h_sq_int_global n).eval s ω‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)
      Filter.atTop
      (nhds (∫⁻ ω, (‖stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global T ω‖₊
        : ℝ≥0∞) ^ 2 ∂P)) := by
    refine hn.congr' ?_
    filter_upwards [Filter.eventually_ge_atTop ⌈T⌉₊] with n hn'
    have hcn : T ≤ (n : ℝ) + 1 := by
      have h1' : T ≤ (⌈T⌉₊ : ℝ) := Nat.le_ceil T
      have h2' : (⌈T⌉₊ : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn'
      linarith
    rw [MeasureTheory.eLpNorm_congr_ae
        (masterLp_coeFn W ℱ hℱ H h_meas h_progMeas h_sq_int_global n (le_of_lt hT) hcn),
      eLpNorm_sq_eq_lintegral_nnnorm_sq,
      simpleIntegral_intermediate_isometry W ℱ hℱ
        (masterApprox ℱ H h_meas h_progMeas h_sq_int_global n)
        (masterApprox_adapt ℱ H h_meas h_progMeas h_sq_int_global n) (le_of_lt hT)]
  exact tendsto_nhds_unique h_a
    (masterApprox_evalNorm_tendsto ℱ H h_meas h_progMeas h_sq_int_global hT)
include hℱ in
/-- `F t ∈ L²(P)`. -/
lemma stochasticIntegralBrownian_memLp (t : ℝ) :
    MeasureTheory.MemLp (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas
      h_sq_int_global t) 2 P :=
  (MeasureTheory.Lp.memLp _).ae_eq
    (stochasticIntegralBrownian_ae_eq W ℱ hℱ H h_meas h_progMeas h_sq_int_global t).symm
include hℱ in
/-- `F t =ᵐ 0` for `t ≤ 0`. -/
lemma stochasticIntegralBrownian_ae_zero_of_nonpos {t : ℝ} (ht : t ≤ 0) :
    stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global t =ᵐ[P] 0 := by
  rcases lt_or_eq_of_le ht with ht' | ht'
  · exact stochasticIntegralBrownian_ae_zero_of_neg W ℱ hℱ H h_meas h_progMeas h_sq_int_global ht'
  · subst ht'
    have h := masterApprox_tendsto_L2 W ℱ hℱ H h_meas h_progMeas h_sq_int_global (le_refl (0 : ℝ))
    have hconst : ∀ n, MeasureTheory.eLpNorm
        (fun ω => simpleIntegral W (masterApprox ℱ H h_meas h_progMeas h_sq_int_global n) 0 ω
          - stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global 0 ω) 2 P
        = MeasureTheory.eLpNorm
          (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global 0) 2 P := by
      intro n
      rw [← MeasureTheory.eLpNorm_neg
        (f := stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global 0)]
      refine MeasureTheory.eLpNorm_congr_ae ?_
      filter_upwards with ω
      simp [simpleIntegral_eq_zero_of_nonpos W _ (le_refl (0 : ℝ)) ω]
    simp only [hconst] at h
    have hz : MeasureTheory.eLpNorm
        (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global 0) 2 P = 0 :=
      tendsto_nhds_unique tendsto_const_nhds h
    rwa [MeasureTheory.eLpNorm_eq_zero_iff
      (stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global
        0).aestronglyMeasurable
      (by norm_num)] at hz
include hℱ in
/-- `∫⁻‖F t‖² = ∫⁻∫⁻_{[0,t]}‖H‖²` for all `t ≥ 0` (isometry, incl. `t = 0`). -/
lemma stochasticIntegralBrownian_lintegral_sq {t : ℝ} (ht : 0 ≤ t) :
    ∫⁻ ω, (‖stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas
      h_sq_int_global t ω‖₊ : ℝ≥0∞) ^ 2 ∂P
      = ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) t, (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P := by
  rcases lt_or_eq_of_le ht with ht' | ht'
  · exact isometry_stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global ht'
  · subst ht'
    rw [lintegral_congr_ae (by
      filter_upwards [stochasticIntegralBrownian_ae_zero_of_nonpos W ℱ hℱ H h_meas h_progMeas
        h_sq_int_global (le_refl (0:ℝ))] with ω hω; rw [hω]; simp : _ =ᵐ[P] fun _ => (0:ℝ≥0∞))]
    rw [MeasureTheory.lintegral_zero]
    symm
    rw [← MeasureTheory.lintegral_zero (μ := P)]
    refine lintegral_congr (fun ω => ?_)
    rw [MeasureTheory.setLIntegral_measure_zero _ _ (by simp)]
include h_meas in
omit [IsProbabilityMeasure P] in
/-- Additivity of the horizon integral: `[0,r] = [0,s] ⊎ (s,r]`. -/
lemma horizon_lintegral_add {s r : ℝ} (hs : 0 ≤ s) (hsr : s ≤ r) :
    ∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) r, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P
      = (∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)
        + ∫⁻ ω, ∫⁻ u in Set.Ioc s r, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P := by
  have hinner : ∀ ω, ∫⁻ u in Set.Icc (0 : ℝ) r, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume
      = ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume
        + ∫⁻ u in Set.Ioc s r, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume := by
    intro ω
    rw [← Set.Icc_union_Ioc_eq_Icc hs hsr,
        MeasureTheory.lintegral_union measurableSet_Ioc
          (Set.disjoint_left.mpr (fun x hx1 hx2 => absurd hx2.1 (not_lt.mpr hx1.2)))]
  rw [MeasureTheory.lintegral_congr hinner]
  exact MeasureTheory.lintegral_add_left'
    ((Measurable.lintegral_prod_right' (ν := volume.restrict (Set.Icc (0 : ℝ) s))
      (((h_meas.nnnorm).coe_nnreal_ennreal).pow_const 2)).aemeasurable) _
include h_meas h_sq_int_global in
/-- Right-continuity of the horizon integral `r ↦ ∫⁻∫⁻_{[0,r]}‖H‖²` at `s ≥ 0`. -/
lemma horizon_lintegral_right_tendsto {s : ℝ} (hs : 0 ≤ s) :
    Filter.Tendsto (fun r => ∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) r,
        (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)
      (nhdsWithin s (Set.Ioi s))
      (nhds (∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)) := by
  have hz : Filter.Tendsto (fun r => ∫⁻ ω, ∫⁻ u in Set.Ioc s r,
        (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P) (nhdsWithin s (Set.Ioi s)) (nhds 0) :=
    tendsto_setLIntegral_Ioc_prod_zero (fun ω u => (‖H ω u‖₊ : ℝ≥0∞) ^ 2)
      ((h_meas.nnnorm.coe_nnreal_ennreal).pow_const 2) hs (lt_add_one s)
      (h_sq_int_global (s + 1) (by linarith)).ne
  have ht := (tendsto_const_nhds (x := ∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s,
    (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P)).add hz
  rw [add_zero] at ht
  refine ht.congr' ?_
  filter_upwards [self_mem_nhdsWithin] with r hr
  exact (horizon_lintegral_add H h_meas hs (le_of_lt hr)).symm
include hℱ in
/-- **Right-`L²`-continuity of the Itô integral process.** `‖F r − F s‖_{L²} → 0` as
`r ↓ s`. The squared increment `∫⁻‖F r − F s‖²` equals `ofReal((∫⁻∫⁻_{[0,r]}).toReal −
(∫⁻∫⁻_{[0,s]}).toReal)` (orthogonality + isometry) and `→ 0` by horizon
right-continuity. -/
lemma stochasticIntegralBrownian_eLpNorm_two_right_tendsto (s : ℝ) :
    Filter.Tendsto (fun r => MeasureTheory.eLpNorm
        (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global r
          - stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global s) 2 P)
      (nhdsWithin s (Set.Ioi s)) (nhds 0) := by
  suffices hsq : Filter.Tendsto (fun r => ∫⁻ ω,
      (‖(stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global r
        - stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas
          h_sq_int_global s) ω‖₊ : ℝ≥0∞) ^ 2 ∂P)
      (nhdsWithin s (Set.Ioi s)) (nhds 0) by
    have h2 := hsq.ennrpow_const ((1 : ℝ) / 2)
    rw [ENNReal.zero_rpow_of_pos (by norm_num)] at h2
    refine h2.congr (fun r => ?_)
    rw [← eLpNorm_sq_eq_lintegral_nnnorm_sq, ← ENNReal.rpow_mul,
      show (2 : ℝ) * (1 / 2) = 1 from by norm_num, ENNReal.rpow_one]
  -- the squared increment
  rcases le_or_gt 0 s with hs | hs
  · -- s ≥ 0: orthogonality + isometry + horizon continuity
    have hFsq : ∀ {t : ℝ}, 0 ≤ t →
        ∫ ω, (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global t ω) ^ 2 ∂P
          = (∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) t, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P).toReal := by
      intro t ht
      have hb := lintegral_nnnorm_sq_eq_ofReal_integral
        (stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global t)
      rw [stochasticIntegralBrownian_lintegral_sq W ℱ hℱ H h_meas h_progMeas
        h_sq_int_global ht] at hb
      rw [hb, ENNReal.toReal_ofReal (integral_nonneg (fun ω => sq_nonneg _))]
    have hincr : ∀ {r : ℝ}, s ≤ r →
        ∫⁻ ω, (‖stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global r ω
          - stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas
            h_sq_int_global s ω‖₊ : ℝ≥0∞) ^ 2 ∂P
          = ENNReal.ofReal
            ((∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) r, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P).toReal
              - (∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P).toReal) := by
      intro r hsr
      rw [lintegral_nnnorm_sq_eq_ofReal_integral
        (g := fun ω => stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global r ω
          - stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global s ω)
        ((stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global r).sub
          (stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global s))]
      congr 1
      rw [integral_sq_increment_eq_of_martingale
        (martingale_stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global)
        (stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global s)
        (stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas h_sq_int_global r) hsr,
        hFsq (le_trans hs hsr), hFsq hs]
    -- the toReal-difference → 0
    have hcont : Filter.Tendsto (fun r =>
        ((∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) r, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P).toReal
          - (∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P).toReal))
        (nhdsWithin s (Set.Ioi s)) (nhds 0) := by
      have hfin_s : ∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P ≠ ⊤ :=
        ne_top_of_le_ne_top (h_sq_int_global (s + 1) (by linarith)).ne
          (MeasureTheory.lintegral_mono (fun ω =>
            lintegral_mono_set (Set.Icc_subset_Icc_right (by linarith))))
      have h0 := (ENNReal.tendsto_toReal hfin_s).comp
        (horizon_lintegral_right_tendsto H h_meas h_sq_int_global hs)
      have h1 := h0.sub_const
        ((∫⁻ ω, ∫⁻ u in Set.Icc (0 : ℝ) s, (‖H ω u‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P).toReal)
      rw [sub_self] at h1
      exact h1
    have hof := (ENNReal.continuous_ofReal.tendsto 0).comp hcont
    rw [ENNReal.ofReal_zero] at hof
    refine hof.congr' ?_
    filter_upwards [self_mem_nhdsWithin] with r hr
    exact (hincr (le_of_lt hr)).symm
  · -- s < 0: eventually zero
    refine Filter.Tendsto.congr' ?_ tendsto_const_nhds
    filter_upwards [Ioo_mem_nhdsGT hs] with r hr
    symm
    rw [← MeasureTheory.lintegral_zero (μ := P)]
    refine lintegral_congr_ae ?_
    filter_upwards [stochasticIntegralBrownian_ae_zero_of_neg W ℱ hℱ H h_meas h_progMeas
        h_sq_int_global hr.2,
      stochasticIntegralBrownian_ae_zero_of_neg W ℱ hℱ H h_meas h_progMeas h_sq_int_global hs]
      with ω hr0 hs0
    simp [hr0, hs0]
include hℱ in
/-- **Conjunct 1 on `rightCont`: `F` is a martingale wrt `ℱ.rightCont`.**
Right-`L²`-continuity of the slices (`stochasticIntegralBrownian_eLpNorm_two_right_tendsto`)
feeds `martingale_rightCont_of_tendsto_eLpNorm_one`. -/
lemma martingale_rightCont_stochasticIntegralBrownian :
    MeasureTheory.Martingale (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global)
      ℱ.rightCont P := by
  refine LevyStochCalc.Martingale.martingale_rightCont_of_tendsto_eLpNorm_one
    (martingale_stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global) (fun s => ?_)
  have hF_aesm : ∀ t, MeasureTheory.AEStronglyMeasurable
      (stochasticIntegralBrownian W ℱ hℱ H h_meas h_progMeas h_sq_int_global t) P :=
    fun t => (stochasticIntegralBrownian_memLp W ℱ hℱ H h_meas h_progMeas
      h_sq_int_global t).aestronglyMeasurable
  exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds
    (stochasticIntegralBrownian_eLpNorm_two_right_tendsto W ℱ hℱ H h_meas h_progMeas
      h_sq_int_global s)
    (Filter.Eventually.of_forall (fun r => bot_le))
    (Filter.Eventually.of_forall (fun r => MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le
      (by norm_num) ((hF_aesm r).sub (hF_aesm s))))
include h_meas h_sq_int_global in
omit [IsProbabilityMeasure P] in
/-- The `H`-compensator `A_t = ∫₀ᵗ H² ds` is finite in `L²(P ⊗ vol|_{[0,t]})`,
i.e. `(ω, u) ↦ H ω u` is square-integrable over the product. -/
lemma compensatorH_memLp_prod {t : ℝ} (ht : 0 < t) :
    MeasureTheory.MemLp (fun p : Ω × ℝ => H p.1 p.2) 2
      (P.prod (volume.restrict (Set.Icc (0 : ℝ) t))) := by
  refine ⟨h_meas.aestronglyMeasurable, ?_⟩
  rw [MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top
    (by norm_num : (2 : ℝ≥0∞) ≠ 0) (by simp : (2 : ℝ≥0∞) ≠ ⊤),
    show (2 : ℝ≥0∞).toReal = 2 from by simp]
  have hbridge : ∫⁻ p : Ω × ℝ, (‖H p.1 p.2‖ₑ) ^ (2 : ℝ)
        ∂(P.prod (volume.restrict (Set.Icc (0 : ℝ) t)))
      = ∫⁻ ω, ∫⁻ s in Set.Icc (0 : ℝ) t, (‖H ω s‖₊ : ℝ≥0∞) ^ 2 ∂volume ∂P := by
    rw [MeasureTheory.lintegral_prod _
      ((((h_meas.nnnorm).coe_nnreal_ennreal).pow_const 2).aemeasurable.congr
        (Filter.Eventually.of_forall (fun p => by
          rw [show (2 : ℝ) = ((2 : ℕ) : ℝ) from by norm_num, ENNReal.rpow_natCast]; rfl)))]
    refine lintegral_congr (fun ω => ?_)
    refine MeasureTheory.setLIntegral_congr_fun measurableSet_Icc (fun s _ => ?_)
    rw [show (2 : ℝ) = ((2 : ℕ) : ℝ) from by norm_num, ENNReal.rpow_natCast]; rfl
  rw [hbridge]; exact h_sq_int_global t ht
end MasterSequence
end Ito
end Brownian
end LevyStochCalc