AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingItoTerminal

- Product-space convergence of the stopped dyadic refinements transfers through the completed Ito isometry to terminal `L2(mu)` convergence.

theorem tendsto_stopRefinedDyadic_terminalToLp [IsFiniteMeasure mu]
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    Tendsto
      (fun n => terminalToLp (stopRefinedDyadic eta tau htau n) hB)
      atTop
      (𝓝 (itoIntegralTerminal
        (stoppedProgressiveL2 (mu := mu) eta tau htau htauT) hT hB)) := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let target := stoppedProgressiveL2 (mu := mu) eta tau htau htauT
  have hprocess :
      Tendsto
        (fun n => processToLp (stopRefinedDyadic eta tau htau n) hB)
        atTop (𝓝 (integrandToLp target hB)) := by
    change Tendsto
      (fun n => (stopRefinedDyadic eta tau htau n).toLp mu)
      atTop (𝓝 target.toLp)
    exact tendsto_stopRefinedDyadic_toLp eta tau htau htauT
  simpa only [target] using
    tendsto_terminal_of_tendsto_elementary target hT hB
      (fun n => stopRefinedDyadic eta tau htau n) hprocess

/-- **Elementary random-stopping consistency.**  The completed Ito integral of
Chewi's closed stopped elementary integrand is represented almost everywhere
by evaluating the original elementary Ito path at the bounded stopping time.

This is the first completed stochastic statement in the random-stopping chain:
finite-grid identities and product-space convergence have both already been
absorbed before this theorem is invoked. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingItoTerminal.lean:41published source at 7bcd37294df1

Elementary random-stopping consistency. The completed Ito integral of Chewi's closed stopped elementary integrand is represented almost everywhere by evaluating the original elementary Ito path at the bounded stopping time. This is the first completed stochastic statement in the random-stopping chain: finite-grid identities and product-space convergence have both already been absorbed before this theorem is invoked.

theorem itoIntegralTerminal_stopped_elementary_ae [IsFiniteMeasure mu]
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    (fun omega =>
      itoIntegralTerminal
        (stoppedProgressiveL2 (mu := mu) eta tau htau htauT) hT hB omega) =ᵐ[mu]
      (fun omega => elementaryItoIntegral eta.process B (tau omega) omega) := by
  let _ : IsProbabilityMeasure mu := hB.isProbabilityMeasure
  let target := stoppedProgressiveL2 (mu := mu) eta tau htau htauT
  let stopped : ℕ → DyadicElementaryProcess filtration T := fun n =>
    stopRefinedDyadic eta tau htau n
  let rawSum : ℕ → Omega → ℝ := fun n =>
    elementaryItoIntegral (stopped n).process B T
  have hterminal :
      Tendsto (fun n => terminalToLp (stopped n) hB) atTop
        (𝓝 (itoIntegralTerminal target hT hB)) := by
    simpa only [stopped, target] using
      tendsto_stopRefinedDyadic_terminalToLp eta tau htau htauT hT hB
  have hcompletionMeasure : TendstoInMeasure mu
      (fun n omega => terminalToLp (stopped n) hB omega) atTop
      (fun omega => itoIntegralTerminal target hT hB omega) :=
    tendstoInMeasure_of_tendsto_Lp hterminal
  have hterminalEq (n : ℕ) :
      (fun omega => terminalToLp (stopped n) hB omega) =ᵐ[mu]
        rawSum n := by
    have hcoe :=
      (elementaryItoIntegral_memLp_two (stopped n).process hB T).coeFn_toLp
    filter_upwards [hcoe] with omega homega
    exact homega
  have hcompletionMeasure' : TendstoInMeasure mu
      rawSum atTop (fun omega => itoIntegralTerminal target hT hB omega) :=
    hcompletionMeasure.congr hterminalEq Filter.EventuallyEq.rfl
  have haetendsto : ∀ᵐ omega ∂mu,
      Tendsto
        (fun n => rawSum n omega)
        atTop (𝓝 (elementaryItoIntegral eta.process B (tau omega) omega)) := by
    filter_upwards [elementaryItoProcess_continuous_ae eta.process hB T]
      with omega hcontinuous
    have hcont : ContinuousOn
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingItoTerminal.lean:75published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.