AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingBoundary

- At a sample point where the stopping value is zero, every coefficient of any refined elementary process stopped by that random time is exactly zero.

theorem stopRefined_coeff_eq_zero_of_stoppingValue_eq_zero
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (n : ℕ) (omega : Omega) (homega : tau omega = 0)
    (j : Fin (2 ^ stoppingLevel eta n)) :
    (stopElementary
        (refineDyadic eta (stoppingLevel eta n)
          (level_le_stoppingLevel eta n)).process
        (fun w => (tau w : WithTop ℝ≥0)) htau).coeff j omega = 0 := by
  let fine : ElementaryAdaptedProcess filtration (2 ^ stoppingLevel eta n) :=
    (refineDyadic eta (stoppingLevel eta n)
      (level_le_stoppingLevel eta n)).process
  change
    (stopElementary fine (fun w => (tau w : WithTop ℝ≥0)) htau).coeff j omega = 0
  have hstop := stopElementary_coeff
    fine (fun w => (tau w : WithTop ℝ≥0)) htau j omega
  rw [hstop, homega]
  split
  · rename_i hlt
    exact False.elim ((not_lt_of_ge bot_le) hlt)
  · rfl

/-- If the stopping value at the chosen sample point is zero, every refined
stopped elementary Ito sum is exactly zero. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingBoundary.lean:34published source at 77184245109a

- If the stopping value at the chosen sample point is zero, every refined stopped elementary Ito sum is exactly zero.

theorem stopRefined_elementaryItoIntegral_eq_zero_of_stoppingValue_eq_zero
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (n : ℕ) (B : ℝ≥0 → Omega → ℝ)
    (omega : Omega) (homega : tau omega = 0) :
    elementaryItoIntegral
        (stopElementary
          (refineDyadic eta (stoppingLevel eta n)
            (level_le_stoppingLevel eta n)).process
          (fun w => (tau w : WithTop ℝ≥0)) htau)
        B T omega = 0 := by
  unfold elementaryItoIntegral
  apply Finset.sum_eq_zero
  intro j _hj
  rw [stopRefined_coeff_eq_zero_of_stoppingValue_eq_zero
    eta tau htau n omega homega j, zero_mul]

/-- Pointwise stopped-Ito convergence for an elementary integrand and an
arbitrary bounded nonnegative stopping value.  At positive stopping values the
finite stopped sum is exactly evaluation at the dyadic right endpoint and path
continuity supplies the limit; at zero every stopped sum vanishes exactly. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingBoundary.lean:60published source at 77184245109a

- Pointwise stopped-Ito convergence for an elementary integrand and an arbitrary bounded nonnegative stopping value. At positive stopping values the finite stopped sum is exactly evaluation at the dyadic right endpoint and path continuity supplies the limit; at zero every stopped sum vanishes exactly.

theorem tendsto_stopRefined_elementaryItoIntegral
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (B : ℝ≥0 → Omega → ℝ) (omega : Omega)
    (hcont : ContinuousOn
      (fun t => elementaryItoIntegral eta.process B t omega)
      (Icc (0 : ℝ≥0) T)) :
    Tendsto
      (fun n =>
        elementaryItoIntegral
          (stopElementary
            (refineDyadic eta (stoppingLevel eta n)
              (level_le_stoppingLevel eta n)).process
            (fun w => (tau w : WithTop ℝ≥0)) htau)
          B T omega)
      atTop (𝓝 (elementaryItoIntegral eta.process B (tau omega) omega)) := by
  by_cases hzero : tau omega = 0
  · have hseq :
        (fun n =>
          elementaryItoIntegral
            (stopElementary
              (refineDyadic eta (stoppingLevel eta n)
                (level_le_stoppingLevel eta n)).process
              (fun w => (tau w : WithTop ℝ≥0)) htau)
            B T omega) = (fun _ : ℕ => (0 : ℝ)) := by
        funext n
        exact stopRefined_elementaryItoIntegral_eq_zero_of_stoppingValue_eq_zero
          eta tau htau n B omega hzero
    have htarget : elementaryItoIntegral eta.process B (tau omega) omega = 0 := by
      rw [hzero]
      simp [elementaryItoIntegral]
    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 =>
          elementaryItoIntegral
            (stopElementary
              (refineDyadic eta (stoppingLevel eta n)
                (level_le_stoppingLevel eta n)).process
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingBoundary.lean:83published source at 77184245109a

Excerpt truncated; the exact source link is authoritative.