AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingGeneralIto

- The stopped canonical elementary approximants converge to the generic closed stop of the completed integrand.

theorem tendsto_stoppedCanonical_toLp [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T) :
    Tendsto
      (fun n =>
        (stoppedProgressiveL2 (mu := mu)
          (canonicalElementaryApprox eta hT n) tau htau htauT).toLp)
      atTop
      (𝓝 (stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau).toLp) := by
  apply tendsto_stoppedCanonicalApprox_toLp eta
    (stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau)
    hT tau htau htauT
  exact Filter.Eventually.of_forall fun _ => rfl

/-- Ito isometry transfers stopped-integrand convergence to terminal `L²`
convergence. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingGeneralIto.lean:36published source at 77184245109a

- Ito isometry transfers stopped-integrand convergence to terminal `L²` convergence.

theorem tendsto_stoppedCanonical_terminal [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    Tendsto
      (fun n =>
        itoIntegralTerminal
          (stoppedProgressiveL2 (mu := mu)
            (canonicalElementaryApprox eta hT n) tau htau htauT)
          hT hB)
      atTop
      (𝓝 (itoIntegralTerminal
        (stop eta (fun omega => (tau omega : WithTop ℝ≥0)) htau)
        hT hB)) := by
  apply tendsto_iff_norm_sub_tendsto_zero.mpr
  have hstop := tendsto_stoppedCanonical_toLp eta hT tau htau htauT
  have hnorm := tendsto_iff_norm_sub_tendsto_zero.mp hstop
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  simpa only [itoIntegralTerminal_isometry_sub, integrandToLp] using hnorm

/-- **General bounded random-stopping identity.**

For `tau ≤ T`, the completed Ito integral of `eta_s 1_{s ≤ tau}` equals the
continuous Ito process of `eta` evaluated at `tau`, almost surely. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingGeneralIto.lean:55published source at 77184245109a

General bounded random-stopping identity. For `tau ≤ T`, the completed Ito integral of `eta_s 1_{s ≤ tau}` equals the continuous Ito process of `eta` evaluated at `tau`, almost surely.

theorem itoIntegralTerminal_stop_ae [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu) :
    (fun omega =>
      itoIntegralTerminal
        (stop eta (fun w => (tau w : WithTop ℝ≥0)) htau) hT hB omega) =ᵐ[mu]
      (fun omega => itoIntegralProcess eta hT hB hUsual (tau omega) omega) := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let q : ℕ → DyadicElementaryProcess filtration T :=
    fun n => canonicalElementaryApprox eta hT n
  let stoppedQ : ℕ → ProgressiveL2Integrand filtration mu T := fun n =>
    stoppedProgressiveL2 (mu := mu) (q n) tau htau htauT
  let target := stop eta (fun w => (tau w : WithTop ℝ≥0)) htau
  have hterminal :
      Tendsto (fun n => itoIntegralTerminal (stoppedQ n) hT hB) atTop
        (𝓝 (itoIntegralTerminal target hT hB)) := by
    simpa only [q, stoppedQ, target] using
      tendsto_stoppedCanonical_terminal eta hT tau htau htauT hB
  have hcompletion : TendstoInMeasure mu
      (fun n omega => itoIntegralTerminal (stoppedQ n) hT hB omega) atTop
      (fun omega => itoIntegralTerminal target hT hB omega) :=
    tendstoInMeasure_of_tendsto_Lp hterminal
  have hElem (n : ℕ) :
      (fun omega => itoIntegralTerminal (stoppedQ n) hT hB omega) =ᵐ[mu]
        (fun omega => elementaryItoIntegral (q n).process B (tau omega) omega) := by
    simpa only [q, stoppedQ] using
      itoIntegralTerminal_stopped_elementary_ae
        (q n) tau htau htauT hT hB
  have hcompletion' : TendstoInMeasure mu
      (fun n omega => elementaryItoIntegral (q n).process B (tau omega) omega)
      atTop (fun omega => itoIntegralTerminal target hT hB omega) :=
    hcompletion.congr hElem Filter.EventuallyEq.rfl
  have haetendsto : ∀ᵐ omega ∂mu,
      Tendsto
        (fun n => elementaryItoIntegral (q n).process B (tau omega) omega)
        atTop
        (𝓝 (itoIntegralProcess eta hT hB hUsual (tau omega) omega)) := by
    filter_upwards [uniformCauchyEvent_ae eta hT hB] with omega homega
    have hnot : omega ∉ uniformBadSet eta hT B := by
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingGeneralIto.lean:82published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.