production module

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime`

3 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyStoppingTime.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyLocalizerAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime

Imported by

AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheoremAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalizationAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppingL2BridgeTests.CanonicalEnergyStoppingTime

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime.canonicalEnergyLocalizer_isChewiStoppingTime

Partial Not mapped

- 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 ed709a7f320d

theorem

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime.canonicalLocalizingTime_isChewiStoppingTime

Partial Not mapped

- 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 ed709a7f320dOpen detailed card

theorem

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime.canonicalLocalizingTime_isStoppingTime

Partial Not mapped

- 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 ed709a7f320d

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyStoppingTime.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyLocalizer
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime

/-!
# Stopping-time status of canonical energy localizers
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace StochasticProcesses
namespace CanonicalEnergyStoppingTime

open MeasureTheory
open scoped NNReal
open ProgressiveL2 LocalProgressiveL2 CanonicalEnergyLocalizer
open StoppingTime

variable {Omega : Type*} {mOmega : MeasurableSpace Omega}
  {filtration : Filtration ℝ≥0 mOmega} {mu : Measure Omega} {T : ℝ≥0}

/-- 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. -/
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. -/
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