AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalizationL2

- On each sample path, the literal source stopped integrand has nonnegative Lebesgue energy at most the canonical level `n+1`.

theorem rawStoppedTimeLintegral_le
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) (omega : Omega) :
    (∫⁻ t in Icc (0 : ℝ≥0) T,
      ENNReal.ofReal
        ((Localization.stoppedIntegrand eta.process
          (fun w =>
            (canonicalRawLocalizingTime hUsual eta n w : WithTop ℝ≥0))
          t omega) ^ 2)
        ∂TimeMeasure.nnrealLebesgue) ≤ ENNReal.ofReal (n + 1 : ℝ) := by
  change
    (∫⁻ t,
      ENNReal.ofReal
        ((Localization.stoppedIntegrand eta.process
          (fun w =>
            (canonicalRawLocalizingTime hUsual eta n w : WithTop ℝ≥0))
          t omega) ^ 2)
        ∂(TimeMeasure.nnrealLebesgue.restrict (Icc (0 : ℝ≥0) T))) ≤
      ENNReal.ofReal (n + 1 : ℝ)
  rw [← TimeMeasure.upTo_eq_restrict_nnrealLebesgue T]
  have hae := stoppedIntegrand_ae_eq_energyStoppedIntegrand
    hUsual eta n omega
  have hsq :
      (fun t => ENNReal.ofReal
        ((Localization.stoppedIntegrand eta.process
          (fun w =>
            (canonicalRawLocalizingTime hUsual eta n w : WithTop ℝ≥0))
          t omega) ^ 2)) =ᵐ[TimeMeasure.upTo T]
      (fun t => ENNReal.ofReal
        ((energyStoppedIntegrand hUsual eta (n + 1 : ℝ) t omega) ^ 2)) := by
    filter_upwards [hae] with t ht
    rw [ht]
  rw [lintegral_congr_ae hsq]
  rw [← ofReal_integral_eq_lintegral_ofReal
    (sectionSquare_integrable hUsual eta (n + 1 : ℝ) omega)
    (ae_of_all _ fun _ => sq_nonneg _)]
  exact ENNReal.ofReal_le_ofReal
    (integral_energyStoppedIntegrand_sq_le hUsual eta (by positivity) omega)

/-- Integrating the pathwise `n+1` bound over a probability space gives the
finite expected stopped energy required by Definition 1.1.12. -/

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

- Integrating the pathwise `n+1` bound over a probability space gives the finite expected stopped energy required by Definition 1.1.12.

theorem rawStoppedProductEnergy_lt_top
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (n : ℕ) :
    (∫⁻ omega, ∫⁻ t in Icc (0 : ℝ≥0) T,
      ENNReal.ofReal
        ((Localization.stoppedIntegrand eta.process
          (fun w =>
            (canonicalRawLocalizingTime hUsual eta n w : WithTop ℝ≥0))
          t omega) ^ 2)
        ∂TimeMeasure.nnrealLebesgue ∂mu) < ∞ := by
  calc
    (∫⁻ omega, ∫⁻ t in Icc (0 : ℝ≥0) T,
      ENNReal.ofReal
        ((Localization.stoppedIntegrand eta.process
          (fun w =>
            (canonicalRawLocalizingTime hUsual eta n w : WithTop ℝ≥0))
          t omega) ^ 2)
        ∂TimeMeasure.nnrealLebesgue ∂mu) ≤
        ∫⁻ _omega, ENNReal.ofReal (n + 1 : ℝ) ∂mu := by
      apply lintegral_mono
      intro omega
      exact rawStoppedTimeLintegral_le hUsual eta n omega
    _ = ENNReal.ofReal (n + 1 : ℝ) := by simp
    _ < ∞ := ENNReal.ofReal_lt_top

/-- Chewi Proposition 1.1.13 in the exact repository-native source contract:
the canonical raw times form a `Localization.IsLocalizingSequence` for the
original progressive locally square-integrable integrand. -/

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

- Chewi Proposition 1.1.13 in the exact repository-native source contract: the canonical raw times form a `Localization.IsLocalizingSequence` for the original progressive locally square-integrable integrand.

theorem canonicalRaw_isLocalizingSequence
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T) :
    Localization.IsLocalizingSequence eta.process filtration mu T
      (fun n omega =>
        (canonicalRawLocalizingTime hUsual eta n omega : WithTop ℝ≥0)) := by
  refine ⟨eta.progressive, ?_, ?_, ?_, ?_⟩
  · intro n
    exact canonicalRawLocalizingTime_isStoppingTime hUsual eta n
  · intro n k hnk omega
    simpa only [WithTop.coe_le_coe] using
      ((canonicalRawLocalizingTime_mono hUsual eta) hnk omega)
  · intro n
    exact rawStoppedProductEnergy_lt_top hUsual eta n
  · exact canonicalRawLocalizingTime_tendsto_terminal_ae hUsual eta

end CanonicalRawLocalizationL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalizationL2.lean:101published source at 7bcd37294df1