AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheorem

- The globally square-integrable stopped integrand at the `n`-th canonical energy level.

noncomputable def canonicalStoppedProgressiveL2
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) : ProgressiveL2Integrand filtration mu T :=
  stoppedProgressiveL2 hUsual eta (level := (n + 1 : ℝ)) (by positivity)

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalLocalizationTheorem.lean:29published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem canonicalStoppedProgressiveL2_process
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    (canonicalStoppedProgressiveL2 hUsual eta n).process =
      energyStoppedIntegrand hUsual eta (n + 1 : ℝ) :=
  rfl

/-- Chewi, Proposition 1.1.13: the energy-level first-hitting times form a
canonical localizing sequence, and every stopped integrand is globally square
integrable with its exact pathwise energy bound. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalLocalizationTheorem.lean:36published source at 7bcd37294df1

- Chewi, Proposition 1.1.13: the energy-level first-hitting times form a canonical localizing sequence, and every stopped integrand is globally square integrable with its exact pathwise energy bound.

theorem chewi_proposition_1_1_13
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T) :
    (∀ n, IsChewiStoppingTime filtration
      (fun omega =>
        (canonicalLocalizingTime hUsual eta n omega : WithTop ℝ≥0))) ∧
    (∀ omega, Monotone
      (fun n => canonicalLocalizingTime hUsual eta n omega)) ∧
    (∀ omega, Tendsto
      (fun n => canonicalLocalizingTime hUsual eta n omega)
      atTop (𝓝 T)) ∧
    (∀ n omega,
      ∫ s,
        ((canonicalStoppedProgressiveL2 hUsual eta n).process s omega) ^ 2
          ∂(TimeMeasure.upTo T) ≤ (n + 1 : ℝ)) := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · exact fun n => canonicalLocalizingTime_isChewiStoppingTime hUsual eta n
  · exact fun omega => canonicalLocalizingTime_mono hUsual eta omega
  · exact fun omega => tendsto_canonicalLocalizingTime hUsual eta omega
  · intro n omega
    change ∫ s,
        (energyStoppedIntegrand hUsual eta (n + 1 : ℝ) s omega) ^ 2
          ∂(TimeMeasure.upTo T) ≤ (n + 1 : ℝ)
    exact integral_energyStoppedIntegrand_sq_le hUsual eta (by positivity) omega

end CanonicalLocalizationTheorem
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalLocalizationTheorem.lean:48published source at 7bcd37294df1Open detailed card