AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedItoOverlap

- The `k`-th globally localized Itô martingale.

noncomputable def globalStoppedItoProcess
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (k : ℕ) : ℝ≥0 → Omega → ℝ :=
  itoIntegralProcess (globalStoppedProgressiveL2 hUsual eta k)
    (dyadicHorizon_pos k) hB hUsual

/-- Each localized process is strongly adapted. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:47published source at 7bcd37294df1

- Each localized process is strongly adapted.

theorem globalStoppedItoProcess_stronglyAdapted
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (k : ℕ) :
    StronglyAdapted filtration (globalStoppedItoProcess hUsual eta hB k) := by
  simpa only [globalStoppedItoProcess] using
    itoIntegralProcess_stronglyAdapted
      (globalStoppedProgressiveL2 hUsual eta k)
      (dyadicHorizon_pos k) hB hUsual

/-- Each localized process is a true martingale. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:57published source at 7bcd37294df1

- Each localized process is a true martingale.

theorem globalStoppedItoProcess_martingale
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (k : ℕ) :
    Martingale (globalStoppedItoProcess hUsual eta hB k) filtration mu := by
  simpa only [globalStoppedItoProcess] using
    itoIntegralProcess_martingale
      (globalStoppedProgressiveL2 hUsual eta k)
      (dyadicHorizon_pos k) hB hUsual

/-- Every localized process has a continuous path on the whole nonnegative
axis, not only on its construction horizon. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:70published source at 7bcd37294df1

- Every localized process has a continuous path on the whole nonnegative axis, not only on its construction horizon.

theorem globalStoppedItoProcess_continuous
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (k : ℕ) (omega : Omega) :
    Continuous (fun t => globalStoppedItoProcess hUsual eta hB k t omega) := by
  simpa only [globalStoppedItoProcess] using
    itoIntegralProcess_continuous
      (globalStoppedProgressiveL2 hUsual eta k)
      (dyadicHorizon_pos k) hB hUsual omega

/-- Every localized Itô process starts from zero. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:84published source at 7bcd37294df1

- Every localized Itô process starts from zero.

theorem globalStoppedItoProcess_zero
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (k : ℕ) :
    globalStoppedItoProcess hUsual eta hB k 0 = 0 := by
  simpa only [globalStoppedItoProcess] using
    itoIntegralProcess_at_zero
      (globalStoppedProgressiveL2 hUsual eta k)
      (dyadicHorizon_pos k) hB hUsual

/-- For a finite-valued stopping time, Mathlib's `WithTop` stopped-process
notation is the ordinary `NNReal` minimum. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:97published source at 7bcd37294df1

- For a finite-valued stopping time, Mathlib's `WithTop` stopped-process notation is the ordinary `NNReal` minimum.

theorem stoppedProcess_coe_eq_min
    {beta : Type*} (u : ℝ≥0 → Omega → beta)
    (tau : Omega → ℝ≥0) (t : ℝ≥0) (omega : Omega) :
    stoppedProcess u (fun w => (tau w : WithTop ℝ≥0)) t omega =
      u (min t (tau omega)) omega := by
  unfold stoppedProcess
  by_cases ht : t ≤ tau omega
  · have htTop : (t : WithTop ℝ≥0) ≤ (tau omega : WithTop ℝ≥0) :=
      WithTop.coe_le_coe.mpr ht
    rw [min_eq_left htTop, min_eq_left ht]
    rfl
  · have htau : tau omega ≤ t := le_of_not_ge ht
    have htauTop : (tau omega : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) :=
      WithTop.coe_le_coe.mpr htau
    rw [min_eq_right htauTop, min_eq_right htau]
    rfl

/-- The stopped larger martingale has continuous paths. -/

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

- The stopped larger martingale has continuous paths.

theorem stopped_globalStoppedItoProcess_continuous
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (ell k : ℕ) (omega : Omega) :
    Continuous (fun t =>
      stoppedProcess (globalStoppedItoProcess hUsual eta hB ell)
        (fun w =>
          (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
        t omega) := by
  rw [show (fun t =>
      stoppedProcess (globalStoppedItoProcess hUsual eta hB ell)
        (fun w =>
          (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
        t omega) =
      (fun t => globalStoppedItoProcess hUsual eta hB ell
        (min t (dyadicGlobalLocalizingTime hUsual eta k omega)) omega) by
    funext t
    exact stoppedProcess_coe_eq_min
      (globalStoppedItoProcess hUsual eta hB ell)
      (dyadicGlobalLocalizingTime hUsual eta k) t omega]
  exact (globalStoppedItoProcess_continuous hUsual eta hB ell omega).comp
    (continuous_id.min continuous_const)

/-- On the larger finite horizon, completed random stopping identifies the
stopped larger path with the Itô process of the twice-stopped integrand,
simultaneously for every time on one full-measure event. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:129published source at 7bcd37294df1

- On the larger finite horizon, completed random stopping identifies the stopped larger path with the Itô process of the twice-stopped integrand, simultaneously for every time on one full-measure event.

theorem stopped_large_eq_ito_stop_pathwise_ae
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {k ell : ℕ} (hkell : k ≤ ell) :
    ∀ᵐ omega ∂mu, ∀ t ∈ Icc (0 : ℝ≥0) (dyadicHorizon ell),
      stoppedProcess (globalStoppedItoProcess hUsual eta hB ell)
          (fun w =>
            (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
          t omega =
        itoIntegralProcess
          (stop (globalStoppedProgressiveL2 hUsual eta ell)
            (fun w =>
              (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
            (dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k))
          (dyadicHorizon_pos ell) hB hUsual t omega := by
  let tauNN : Omega → ℝ≥0 := dyadicGlobalLocalizingTime hUsual eta k
  let tau : Omega → WithTop ℝ≥0 := fun omega => (tauNN omega : WithTop ℝ≥0)
  let Gell := globalStoppedProgressiveL2 hUsual eta ell
  let Gstop := stop Gell tau
    (dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k)
  let J : ℝ≥0 → Omega → ℝ :=
    stoppedProcess (globalStoppedItoProcess hUsual eta hB ell) tau
  have htau : IsChewiStoppingTime filtration tau := by
    simpa only [tau, tauNN] using
      dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k
  have htau' : MeasureTheory.IsStoppingTime filtration tau := htau
  have htauHell : ∀ omega, tauNN omega ≤ dyadicHorizon ell := by
    intro omega
    exact (dyadicGlobalLocalizingTime_le_horizon hUsual eta k omega).trans
      (DyadicHorizonExtension.dyadicHorizon_mono hkell)
  have hJadapted : StronglyAdapted filtration J := by
    have hM := globalStoppedItoProcess_stronglyAdapted hUsual eta hB ell
    have hcont : ∀ omega, Continuous fun t =>
        globalStoppedItoProcess hUsual eta hB ell t omega :=
      globalStoppedItoProcess_continuous hUsual eta hB ell
    simpa only [J, tau] using hM.stoppedProcess hcont htau'
  have hJcontinuous : ∀ᵐ omega ∂mu,
      ContinuousOn (fun t => J t omega)
        (Icc (0 : ℝ≥0) (dyadicHorizon ell)) := by
    filter_upwards [] with omega
    exact (by
      simpa only [J, tau, tauNN] using
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:157published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.

Global pairwise coherence. If `k <= ell`, then on one full-measure event the `k`-th localized martingale is exactly the `ell`-th martingale stopped at `tau_k`, simultaneously for every nonnegative time.

theorem globalStoppedItoProcess_overlap_pathwise_ae
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2.GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    {k ell : ℕ} (hkell : k ≤ ell) :
    ∀ᵐ omega ∂mu, ∀ t : ℝ≥0,
      globalStoppedItoProcess hUsual eta hB k t omega =
        stoppedProcess (globalStoppedItoProcess hUsual eta hB ell)
          (fun w =>
            (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0))
          t omega := by
  let Gk := globalStoppedProgressiveL2 hUsual eta k
  let Gell := globalStoppedProgressiveL2 hUsual eta ell
  let tau : Omega → WithTop ℝ≥0 := fun w =>
    (dyadicGlobalLocalizingTime hUsual eta k w : WithTop ℝ≥0)
  let Gstop := stop Gell tau
    (dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k)
  let Gext := extendByZero Gk (DyadicHorizonExtension.dyadicHorizon_mono hkell)
  have hLp : Gstop.toLp = Gext.toLp := by
    simpa only [Gstop, Gell, Gk, Gext, tau] using
      stop_globalStopped_toLp_eq_extendByZero hUsual eta hkell
  have hstopPath := stopped_large_eq_ito_stop_pathwise_ae
    hUsual eta hB hkell
  have hcongr := itoIntegralProcess_congr_toLp_pathwise_ae
    Gstop Gext (dyadicHorizon_pos ell) hB hUsual hLp
  have hcross := itoIntegralProcess_extendByZero_pathwise_ae
    hkell Gk hB hUsual
  filter_upwards [hstopPath, hcongr, hcross] with omega hstop hcg hcr
  intro t
  by_cases ht : t ≤ dyadicHorizon k
  · have htK : t ∈ Icc (0 : ℝ≥0) (dyadicHorizon k) := ⟨zero_le t, ht⟩
    have htL : t ∈ Icc (0 : ℝ≥0) (dyadicHorizon ell) :=
      ⟨zero_le t, ht.trans (DyadicHorizonExtension.dyadicHorizon_mono hkell)⟩
    calc
      globalStoppedItoProcess hUsual eta hB k t omega =
          itoIntegralProcess Gext (dyadicHorizon_pos ell) hB hUsual t omega := by
            symm
            simpa only [Gext, Gk, globalStoppedItoProcess] using hcr t htK
      _ = itoIntegralProcess Gstop (dyadicHorizon_pos ell) hB hUsual t omega := by
            exact (hcg t htL).symm
      _ = stoppedProcess (globalStoppedItoProcess hUsual eta hB ell) tau
            t omega := by
            exact (hstop t htL).symm
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean:220published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.