AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime

- The canonical hitting time of any nonnegative energy level is a Chewi stopping time. Keeping this theorem level-generic lets later nested-stopping arguments use arbitrary `c ≤ d`, not only integer thresholds.

theorem canonicalEnergyLocalizer_isChewiStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {level : ℝ} (hlevel : 0 ≤ level) :
    IsChewiStoppingTime filtration
      (fun omega =>
        (canonicalEnergyLocalizer hUsual eta level omega : WithTop ℝ≥0)) := by
  intro t
  simpa only [WithTop.coe_le_coe] using
    measurableSet_canonicalEnergyLocalizer_le hUsual eta hlevel t

/-- Each canonical integer energy localizer is a stopping time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyStoppingTime.lean:24published source at 7bcd37294df1

- Each canonical integer energy localizer is a stopping time.

theorem canonicalLocalizingTime_isChewiStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    IsChewiStoppingTime filtration
      (fun omega => (canonicalLocalizingTime hUsual eta n omega : WithTop ℝ≥0)) := by
  simpa only [canonicalLocalizingTime] using
    canonicalEnergyLocalizer_isChewiStoppingTime hUsual eta
      (show 0 ≤ (n + 1 : ℝ) by positivity)

/-- The same statement at Mathlib's native stopping-time interface. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyStoppingTime.lean:36published source at 7bcd37294df1Open detailed card

- The same statement at Mathlib's native stopping-time interface.

theorem canonicalLocalizingTime_isStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    IsStoppingTime filtration
      (fun omega => (canonicalLocalizingTime hUsual eta n omega : WithTop ℝ≥0)) :=
  canonicalLocalizingTime_isChewiStoppingTime hUsual eta n

end CanonicalEnergyStoppingTime
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyStoppingTime.lean:47published source at 7bcd37294df1