AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalization

- Source-facing canonical time: use the completed-energy localizer off the null bad-energy set and stop immediately on that exceptional set.

noncomputable def canonicalRawLocalizingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) (omega : Omega) : ℝ≥0 := by
  classical
  exact if omega ∈ badEnergySet eta then 0
    else canonicalLocalizingTime hUsual eta n omega

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

No declaration docstring.

@[simp] theorem canonicalRawLocalizingTime_of_bad
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) {omega : Omega} (homega : omega ∈ badEnergySet eta) :
    canonicalRawLocalizingTime hUsual eta n omega = 0 := by
  simp [canonicalRawLocalizingTime, homega]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:45published source at 7bcd37294df1

No declaration docstring.

@[simp] theorem canonicalRawLocalizingTime_of_good
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) {omega : Omega} (homega : omega ∉ badEnergySet eta) :
    canonicalRawLocalizingTime hUsual eta n omega =
      canonicalLocalizingTime hUsual eta n omega := by
  simp [canonicalRawLocalizingTime, homega]

/-- The raw localizers increase with the energy level. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:52published source at 7bcd37294df1

- The raw localizers increase with the energy level.

theorem canonicalRawLocalizingTime_mono
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T) :
    Monotone (fun n => canonicalRawLocalizingTime hUsual eta n) := by
  intro n k hnk omega
  classical
  by_cases hbad : omega ∈ badEnergySet eta
  · simp [canonicalRawLocalizingTime, hbad]
  · simpa [canonicalRawLocalizingTime, hbad] using
      (canonicalLocalizingTime_mono hUsual eta omega hnk)

/-- Fixed-time occurrence events for the raw localizer are measurable. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:61published source at 7bcd37294df1

- Fixed-time occurrence events for the raw localizer are measurable.

theorem measurableSet_canonicalRawLocalizingTime_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) (t : ℝ≥0) :
    MeasurableSet[filtration t]
      {omega | canonicalRawLocalizingTime hUsual eta n omega ≤ t} := by
  classical
  have hbad : MeasurableSet[filtration t] (badEnergySet eta) :=
    measurableSet_badEnergySet hUsual eta t
  have hcanonical : MeasurableSet[filtration t]
      {omega | canonicalLocalizingTime hUsual eta n omega ≤ t} := by
    simpa only [canonicalLocalizingTime] using
      (measurableSet_canonicalEnergyLocalizer_le hUsual eta
        (show 0 ≤ (n + 1 : ℝ) by positivity) t)
  have hset :
      {omega | canonicalRawLocalizingTime hUsual eta n omega ≤ t} =
        badEnergySet eta ∪
          {omega | canonicalLocalizingTime hUsual eta n omega ≤ t} := by
    ext omega
    by_cases homega : omega ∈ badEnergySet eta
    · simp [canonicalRawLocalizingTime, homega]
    · simp [canonicalRawLocalizingTime, homega]
  rw [hset]
  exact hbad.union hcanonical

/-- Each raw canonical localizer is a stopping time. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:73published source at 7bcd37294df1

- Each raw canonical localizer is a stopping time.

theorem canonicalRawLocalizingTime_isChewiStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    IsChewiStoppingTime filtration
      (fun omega =>
        (canonicalRawLocalizingTime hUsual eta n omega : WithTop ℝ≥0)) := by
  intro t
  simpa only [WithTop.coe_le_coe] using
    measurableSet_canonicalRawLocalizingTime_le hUsual eta n t

/-- Mathlib-native stopping-time version. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:99published source at 7bcd37294df1

- Mathlib-native stopping-time version.

theorem canonicalRawLocalizingTime_isStoppingTime
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    IsStoppingTime filtration
      (fun omega =>
        (canonicalRawLocalizingTime hUsual eta n omega : WithTop ℝ≥0)) :=
  canonicalRawLocalizingTime_isChewiStoppingTime hUsual eta n

/-- Outside the null bad-energy set, the raw localizer is eventually the
terminal horizon. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:111published source at 7bcd37294df1

- Outside the null bad-energy set, the raw localizer is eventually the terminal horizon.

theorem canonicalRawLocalizingTime_eventually_eq_terminal_of_good
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    {omega : Omega} (homega : omega ∉ badEnergySet eta) :
    ∀ᶠ n in atTop,
      canonicalRawLocalizingTime hUsual eta n omega = T := by
  filter_upwards
    [canonicalLocalizingTime_eventually_eq_terminal hUsual eta omega] with n hn
  simpa [canonicalRawLocalizingTime, homega] using hn

/-- The source-facing raw localizing times converge to `T` almost surely,
with the codomain exactly matching Definition 1.1.12. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:122published source at 7bcd37294df1

- The source-facing raw localizing times converge to `T` almost surely, with the codomain exactly matching Definition 1.1.12.

theorem canonicalRawLocalizingTime_tendsto_terminal_ae
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T) :
    ∀ᵐ omega ∂mu,
      Tendsto
        (fun n =>
          (canonicalRawLocalizingTime hUsual eta n omega : WithTop ℝ≥0))
        atTop (𝓝 (T : WithTop ℝ≥0)) := by
  have hgood : ∀ᵐ omega ∂mu, omega ∉ badEnergySet eta := by
    rw [ae_iff]
    simpa using measure_badEnergySet_zero eta
  filter_upwards [hgood] with omega homega
  have hev : ∀ᶠ n in atTop,
      (canonicalRawLocalizingTime hUsual eta n omega : WithTop ℝ≥0) =
        (T : WithTop ℝ≥0) := by
    filter_upwards
      [canonicalRawLocalizingTime_eventually_eq_terminal_of_good
        hUsual eta homega] with n hn
    exact congrArg (fun s : ℝ≥0 => (s : WithTop ℝ≥0)) hn
  exact (tendsto_congr' hev).2 tendsto_const_nhds

/-- For each sample path, the source-facing stopped raw integrand and the
completed energy-stopped representative agree almost everywhere in time. The
only possible pointwise discrepancy on a good path is the single hitting time;
terminal-time and initial-time endpoint conventions are also null. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:134published source at 7bcd37294df1

- For each sample path, the source-facing stopped raw integrand and the completed energy-stopped representative agree almost everywhere in time. The only possible pointwise discrepancy on a good path is the single hitting time; terminal-time and initial-time endpoint conventions are also null.

theorem stoppedIntegrand_ae_eq_energyStoppedIntegrand
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) (omega : Omega) :
    (fun t => Localization.stoppedIntegrand eta.process
        (fun w =>
          (canonicalRawLocalizingTime hUsual eta n w : WithTop ℝ≥0))
        t omega) =ᵐ[TimeMeasure.upTo T]
      (fun t => energyStoppedIntegrand hUsual eta (n + 1 : ℝ) t omega) := by
  classical
  have hterminal : ∀ᵐ t ∂TimeMeasure.upTo T, t ≠ T := by
    rw [ae_iff]
    simpa using TimeMeasure.upTo_singleton T T
  have hstop : ∀ᵐ t ∂TimeMeasure.upTo T,
      t ≠ canonicalRawLocalizingTime hUsual eta n omega := by
    rw [ae_iff]
    simpa using TimeMeasure.upTo_singleton T
      (canonicalRawLocalizingTime hUsual eta n omega)
  filter_upwards [TimeMeasure.ae_mem_Ioc_zero_upTo T, hterminal, hstop] with
      t htIoc htTne htstop
  have htT : t < T := lt_of_le_of_ne htIoc.2 htTne
  by_cases hbad : omega ∈ badEnergySet eta
  · have hnotle : ¬(t : WithTop ℝ≥0) ≤ (0 : ℝ≥0) := by
      intro h
      have ht0 : t ≤ (0 : ℝ≥0) := by exact_mod_cast h
      exact (not_le_of_gt htIoc.1) ht0
    change
      (if (t : WithTop ℝ≥0) ≤
          (canonicalRawLocalizingTime hUsual eta n omega : WithTop ℝ≥0)
        then eta.process t omega else 0) =
        energyStoppedIntegrand hUsual eta (n + 1 : ℝ) t omega
    rw [canonicalRawLocalizingTime_of_bad hUsual eta n hbad, if_neg hnotle]
    simp [energyStoppedIntegrand, completedEnergy, completedIntegrand, hbad]
  · have hraw : canonicalRawLocalizingTime hUsual eta n omega =
        canonicalLocalizingTime hUsual eta n omega :=
      canonicalRawLocalizingTime_of_good hUsual eta n hbad
    have hiff := completedEnergy_lt_iff_lt_canonicalEnergyLocalizer
      hUsual eta (show 0 ≤ (n + 1 : ℝ) by positivity) omega htT
    rw [hraw] at htstop
    rw [canonicalLocalizingTime] at htstop
    by_cases hbefore : t < canonicalEnergyLocalizer hUsual eta (n + 1 : ℝ) omega
    · have hbelow : completedEnergy hUsual eta t omega < (n + 1 : ℝ) :=
        hiff.mpr hbefore
      have hleCanonical : (t : WithTop ℝ≥0) ≤
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean:159published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.