AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGridStoppingIto

- A stopping time is grid-valued relative to a dyadic elementary process if we have chosen, for every sample point, the grid endpoint that represents its value. Keeping the witness explicit is useful in the finite-sum proof and avoids any measurable-selection issue at this discrete stage.

def IsGridValuedFor
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → WithTop ℝ≥0)
    (cutoff : Omega → Fin (2 ^ eta.level + 1)) : Prop :=
  ∀ omega,
    tau omega = (eta.process.times (cutoff omega) : WithTop ℝ≥0)

/-- On one sample point, the coefficient retained by random stopping agrees
with the deterministic coefficient cutoff at the selected grid index. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGridStoppingIto.lean:37published source at 7bcd37294df1

- On one sample point, the coefficient retained by random stopping agrees with the deterministic coefficient cutoff at the selected grid index.

theorem stopElementary_coeff_eq_gridCutoff
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau)
    (cutoff : Omega → Fin (2 ^ eta.level + 1))
    (hgrid : IsGridValuedFor eta tau cutoff)
    (j : Fin (2 ^ eta.level)) (omega : Omega) :
    (stopElementary eta.process tau htau).coeff j omega =
      if j.castSucc < cutoff omega then eta.process.coeff j omega else 0 := by
  rw [stopElementary_coeff, hgrid omega]
  simp only [WithTop.coe_lt_coe]
  by_cases hj : j.castSucc < cutoff omega
  · have htime :
        eta.process.times j.castSucc < eta.process.times (cutoff omega) :=
      eta.process.times_strictMono hj
    simp [hj, htime]
  · have htime :
        ¬ eta.process.times j.castSucc < eta.process.times (cutoff omega) := by
      intro hlt
      exact hj ((eta.process.times_strictMono.lt_iff_lt).mp hlt)
    simp [hj, htime]

/-- Exact finite-sum stopped-Itô identity for a dyadic grid-valued stopping
time.  This is pointwise in `omega`: no expectation, completion, or limiting
argument is hidden in the statement. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGridStoppingIto.lean:46published source at 7bcd37294df1

- Exact finite-sum stopped-Itô identity for a dyadic grid-valued stopping time. This is pointwise in `omega`: no expectation, completion, or limiting argument is hidden in the statement.

theorem elementaryItoIntegral_stop_gridValued
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau)
    (cutoff : Omega → Fin (2 ^ eta.level + 1))
    (hgrid : IsGridValuedFor eta tau cutoff)
    (B : ℝ≥0 → Omega → ℝ) (omega : Omega) :
    elementaryItoIntegral (stopElementary eta.process tau htau) B T omega =
      elementaryItoIntegral eta.process B
        (eta.process.times (cutoff omega)) omega := by
  unfold elementaryItoIntegral
  apply Finset.sum_congr rfl
  intro j _hj
  rw [stopElementary_coeff_eq_gridCutoff eta tau htau cutoff hgrid j omega]
  change
    (if j.castSucc < cutoff omega then eta.process.coeff j omega else 0) *
        (B (min (eta.process.times j.succ) T) omega -
          B (min (eta.process.times j.castSucc) T) omega) =
      eta.process.coeff j omega *
        (B (min (eta.process.times j.succ) (eta.process.times (cutoff omega))) omega -
          B (min (eta.process.times j.castSucc) (eta.process.times (cutoff omega))) omega)
  let grid := eta.process.times
  have hmono : StrictMono grid := eta.process.times_strictMono
  have hlast : grid (Fin.last (2 ^ eta.level)) = T := by
    change eta.process.times (Fin.last (2 ^ eta.level)) = T
    rw [congrFun eta.times_eq (Fin.last (2 ^ eta.level))]
    exact regularDyadic_last_time T eta.level
  have hrightT : grid j.succ ≤ T := by
    calc
      grid j.succ ≤ grid (Fin.last (2 ^ eta.level)) :=
        hmono.monotone (Fin.le_last j.succ)
      _ = T := hlast
  have hleftT : grid j.castSucc ≤ T :=
    (hmono.monotone (Fin.castSucc_le_succ j)).trans hrightT
  by_cases hj : j.castSucc < cutoff omega
  · have hrightCutoff : grid j.succ ≤ grid (cutoff omega) :=
      hmono.monotone (by
        exact_mod_cast (Nat.succ_le_iff.mpr hj))
    have hleftCutoff : grid j.castSucc ≤ grid (cutoff omega) :=
      (hmono.monotone (Fin.castSucc_le_succ j)).trans hrightCutoff
    simp [hj, grid,
      min_eq_left hrightT, min_eq_left hleftT,
      min_eq_left hrightCutoff, min_eq_left hleftCutoff]
  · have hcutoffLeft : grid (cutoff omega) ≤ grid j.castSucc :=
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGridStoppingIto.lean:71published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.