AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalStoppedItoIntegral

- The `n`-th globally square-integrable stopped Itô martingale.

noncomputable def canonicalStoppedItoProcess
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) : ℝ≥0 → Omega → ℝ :=
  itoIntegralProcess
    (canonicalStoppedProgressiveL2 hUsual eta n) hT hB hUsual

/-- The stopped Itô process is strongly adapted. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:32published source at 7bcd37294df1

- The stopped Itô process is strongly adapted.

theorem canonicalStoppedItoProcess_stronglyAdapted
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) :
    StronglyAdapted filtration
      (canonicalStoppedItoProcess hUsual eta hT hB n) :=
  itoIntegralProcess_stronglyAdapted
    (canonicalStoppedProgressiveL2 hUsual eta n) hT hB hUsual

/-- The stopped Itô process is a genuine martingale. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:42published source at 7bcd37294df1

- The stopped Itô process is a genuine martingale.

theorem canonicalStoppedItoProcess_martingale
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) :
    Martingale (canonicalStoppedItoProcess hUsual eta hT hB n)
      filtration mu :=
  itoIntegralProcess_martingale
    (canonicalStoppedProgressiveL2 hUsual eta n) hT hB hUsual

/-- The process has continuous paths on the construction horizon, including
on the completed exceptional set where it is patched by zero. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:54published source at 7bcd37294df1

- The process has continuous paths on the construction horizon, including on the completed exceptional set where it is patched by zero.

theorem canonicalStoppedItoProcess_continuousOn
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) (omega : Omega) :
    ContinuousOn
      (fun t => canonicalStoppedItoProcess hUsual eta hT hB n t omega)
      (Icc (0 : ℝ≥0) T) :=
  itoIntegralProcess_continuousOn
    (canonicalStoppedProgressiveL2 hUsual eta n) hT hB hUsual omega

/-- At every deterministic time, the stopped process represents the terminal
`L2` Itô integral of the correspondingly restricted stopped integrand. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:67published source at 7bcd37294df1

- At every deterministic time, the stopped process represents the terminal `L2` Itô integral of the correspondingly restricted stopped integrand.

theorem canonicalStoppedItoProcess_at_eq_terminal
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) {t : ℝ≥0} (htT : t ≤ T) :
    canonicalStoppedItoProcess hUsual eta hT hB n t =ᵐ[mu]
      (fun omega =>
        ItoTerminalCompletion.itoIntegralTerminal
          ((canonicalStoppedProgressiveL2 hUsual eta n).restrictAt t)
          hT hB omega) :=
  itoIntegralProcess_at_eq_terminal
    (canonicalStoppedProgressiveL2 hUsual eta n) hT hB hUsual htT

/-- Chewi display (1.1.14): every canonical energy truncation is fed into the
already-constructed global Itô map and yields an adapted continuous
martingale, with the exact deterministic-time restriction compatibility. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:81published source at 7bcd37294df1

- Chewi display (1.1.14): every canonical energy truncation is fed into the already-constructed global Itô map and yields an adapted continuous martingale, with the exact deterministic-time restriction compatibility.

theorem chewi_display_1_1_14
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : LocalProgressiveL2Integrand filtration mu T)
    (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (n : ℕ) :
    StronglyAdapted filtration
        (canonicalStoppedItoProcess hUsual eta hT hB n) ∧
      Martingale (canonicalStoppedItoProcess hUsual eta hT hB n)
        filtration mu ∧
      (∀ omega,
        ContinuousOn
          (fun t => canonicalStoppedItoProcess hUsual eta hT hB n t omega)
          (Icc (0 : ℝ≥0) T)) ∧
      (canonicalStoppedProgressiveL2 hUsual eta n).process =
        energyStoppedIntegrand hUsual eta (n + 1 : ℝ) ∧
      ∀ t : ℝ≥0, t ≤ T →
        canonicalStoppedItoProcess hUsual eta hT hB n t =ᵐ[mu]
          (fun omega =>
            ItoTerminalCompletion.itoIntegralTerminal
              ((canonicalStoppedProgressiveL2 hUsual eta n).restrictAt t)
              hT hB omega) := by
  refine ⟨canonicalStoppedItoProcess_stronglyAdapted hUsual eta hT hB n,
    canonicalStoppedItoProcess_martingale hUsual eta hT hB n,
    canonicalStoppedItoProcess_continuousOn hUsual eta hT hB n,
    canonicalStoppedProgressiveL2_process hUsual eta n, ?_⟩
  intro t htT
  exact canonicalStoppedItoProcess_at_eq_terminal hUsual eta hT hB n htT

end CanonicalStoppedItoIntegral
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean:98published source at 7bcd37294df1Open detailed card