AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingIntegrandLimit

- The randomly stopped dyadic refinements converge at every time/sample pair to the closed stopped integrand used in Chewi's localization definition. The endpoint `s = tau omega` is included: every dyadic right endpoint lies at or to the right of `tau omega`, so the approximants retain `eta_s` there. The case `tau omega = 0` is separated because the elementary process itself vanishes at the left grid endpoint.

theorem tendsto_stopRefinedDyadic_value_stoppedIntegrand
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (s : ℝ≥0) (omega : Omega) :
    Tendsto
      (fun n => (stopRefinedDyadic eta tau htau n).process.value s omega)
      atTop
      (𝓝 (Localization.stoppedIntegrand eta.process.value
        (fun w => (tau w : WithTop ℝ≥0)) s omega)) := by
  by_cases hzero : tau omega = 0
  · have hseq :
        (fun n => (stopRefinedDyadic eta tau htau n).process.value s omega) =
          (fun _ : ℕ => (0 : ℝ)) := by
      funext n
      exact stopRefinedDyadic_value_eq_zero_of_stoppingValue_eq_zero
        eta tau htau n omega hzero s
    have htarget :
        Localization.stoppedIntegrand eta.process.value
          (fun w => (tau w : WithTop ℝ≥0)) s omega = 0 := by
      by_cases hs0 : s = 0
      · subst s
        have hvalue0 : eta.process.value 0 omega = 0 :=
          ElementaryAdaptedProcess.value_eq_zero_of_le_first
            eta.process bot_le omega
        rw [Localization.stoppedIntegrand, hzero]
        simp [hvalue0]
      · have hspos : 0 < s := lt_of_le_of_ne bot_le (Ne.symm hs0)
        have hnot :
            ¬ ((s : WithTop ℝ≥0) ≤ (tau omega : WithTop ℝ≥0)) := by
          rw [hzero]
          simpa only [WithTop.coe_le_coe] using (not_le_of_gt hspos)
        rw [Localization.stoppedIntegrand, if_neg hnot]
    rw [hseq, htarget]
    exact tendsto_const_nhds
  · have homega : 0 < tau omega :=
      lt_of_le_of_ne bot_le (Ne.symm hzero)
    have hseq :
        (fun n => (stopRefinedDyadic eta tau htau n).process.value s omega) =
          (fun n =>
            (stopAtRightApprox eta (DyadicElementaryProcess.horizon_pos eta)
              homega (htauT omega) n).process.value s omega) := by
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingIntegrandLimit.lean:42published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.