AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiProposition1_1_16

Chewi, Proposition 1.1.16. Assume the filtration satisfies the usual conditions, `B` is Brownian motion with respect to that filtration, and `eta` is strongly progressive with finite pathwise square energy on every finite horizon. Then the canonically glued local Itô integral process is strongly adapted, has continuous paths, and is a local martingale. The first component is included explicitly for readers even though adaptedness is already part of `Localization.IsLocalMartingale`.

theorem chewi_proposition_1_1_16
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    StronglyAdapted filtration (globalItoProcess hUsual eta hB) ∧
      (∀ omega, Continuous (fun t => globalItoProcess hUsual eta hB t omega)) ∧
      Localization.IsLocalMartingale
        (globalItoProcess hUsual eta hB) filtration mu := by
  exact ⟨globalItoProcess_stronglyAdapted hUsual eta hB,
    globalItoProcess_continuous hUsual eta hB,
    globalItoProcess_isLocalMartingale hUsual eta hB⟩

/-- **Localized Itô representation for Proposition 1.1.16.**

For every canonical dyadic localizer `tau_k`, stopping the globally glued local
Itô process at `tau_k` recovers, almost surely and at every deterministic time
inside the matching horizon, the completed Itô process of the literal source
integrand `eta_s * 1_{s ≤ tau_k}`.  This is the formal certificate that the
process in `chewi_proposition_1_1_16` is Chewi's local stochastic integral, not
an unrelated local martingale with the same localization sequence. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiProposition1_1_16.lean:51published source at 7bcd37294df1Open detailed card

Localized Itô representation for Proposition 1.1.16. For every canonical dyadic localizer `tau_k`, stopping the globally glued local Itô process at `tau_k` recovers, almost surely and at every deterministic time inside the matching horizon, the completed Itô process of the literal source integrand `eta_s * 1_{s ≤ tau_k}`. This is the formal certificate that the process in `chewi_proposition_1_1_16` is Chewi's local stochastic integral, not an unrelated local martingale with the same localization sequence.

theorem chewi_proposition_1_1_16_stopped_integral_representation
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (k : ℕ) {t : ℝ≥0}
    (ht : t ≤ DyadicGlobalHorizon.dyadicHorizon k) :
    stoppedProcess (globalItoProcess hUsual eta hB)
        (fun omega =>
          (DyadicGlobalHorizon.dyadicGlobalLocalizingTime hUsual eta k omega :
            WithTop ℝ≥0)) t =ᵐ[mu]
      ItoIntegralProcess.itoIntegralProcess
        (GlobalStoppedProgressiveL2.globalStoppedProgressiveL2 hUsual eta k)
        (DyadicGlobalHorizon.dyadicHorizon_pos k) hB hUsual t := by
  have hglobal :=
    stopped_globalItoProcess_eq_stopped_globalStopped_ae
      hUsual eta hB k t
  have hself :=
    GlobalStoppedItoMartingale.globalStoppedItoProcess_overlap_pathwise_ae
      hUsual eta hB (k := k) (ell := k) le_rfl
  filter_upwards [hglobal, hself] with omega hglobalOmega hselfOmega
  have hselfAt := hselfOmega t ⟨bot_le, ht⟩
  have hcombined :
      stoppedProcess (globalItoProcess hUsual eta hB)
          (fun w =>
            (DyadicGlobalHorizon.dyadicGlobalLocalizingTime hUsual eta k w :
              WithTop ℝ≥0)) t omega =
        GlobalStoppedItoMartingale.globalStoppedItoProcess
          hUsual eta hB k t omega :=
    hglobalOmega.trans hselfAt.symm
  simpa only [GlobalStoppedItoMartingale.globalStoppedItoProcess] using hcombined

/-- Source-facing localization certificate accompanying Proposition 1.1.16:
the cofinal dyadic energy localizers are the concrete witness used by the
local-martingale proof. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiProposition1_1_16.lean:72published source at 7bcd37294df1

- Source-facing localization certificate accompanying Proposition 1.1.16: the cofinal dyadic energy localizers are the concrete witness used by the local-martingale proof.

theorem chewi_proposition_1_1_16_localizers
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    (∀ k, StoppingTime.IsChewiStoppingTime filtration
      (fun omega =>
        (DyadicGlobalHorizon.dyadicGlobalLocalizingTime hUsual eta k omega :
          WithTop ℝ≥0))) ∧
    Monotone
      (fun k omega =>
        (DyadicGlobalHorizon.dyadicGlobalLocalizingTime hUsual eta k omega :
          WithTop ℝ≥0)) ∧
    (∀ᵐ omega ∂mu,
      Filter.Tendsto
        (fun k =>
          (DyadicGlobalHorizon.dyadicGlobalLocalizingTime hUsual eta k omega :
            WithTop ℝ≥0))
        Filter.atTop (𝓝 (⊤ : WithTop ℝ≥0))) ∧
    ∀ k,
      Martingale
        (stoppedProcess (globalItoProcess hUsual eta hB)
          (fun omega =>
            (DyadicGlobalHorizon.dyadicGlobalLocalizingTime hUsual eta k omega :
              WithTop ℝ≥0)))
        filtration mu := by
  refine ⟨?_, ?_, ?_, ?_⟩
  · exact fun k =>
      DyadicGlobalHorizon.dyadicGlobalLocalizingTime_isChewiStoppingTime
        hUsual eta k
  · intro k ell hkell omega
    exact WithTop.coe_le_coe.mpr
      ((DyadicGlobalHorizon.dyadicGlobalLocalizingTime_mono hUsual eta)
        hkell omega)
  · exact DyadicGlobalHorizon.dyadicGlobalLocalizingTime_tendsto_top_ae
      hUsual eta
  · exact fun k => stopped_globalItoProcess_martingale hUsual eta hB k

end ChewiProposition1_1_16
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiProposition1_1_16.lean:107published source at 7bcd37294df1