AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessAfterHorizon

- Every canonical elementary Itô approximant is exactly constant after the construction horizon.

theorem canonicalItoProcess_eq_terminal_of_le
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (B : ℝ≥0 → Omega → ℝ) (n : ℕ)
    {t : ℝ≥0} (hTt : T ≤ t) :
    canonicalItoProcess eta hT B n t =
      canonicalItoProcess eta hT B n T := by
  funext omega
  simp [canonicalItoProcess, elementaryItoProcess, min_eq_right hTt]

/-- The pointwise complete-space path limit is constant after the horizon. -/

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

- The pointwise complete-space path limit is constant after the horizon.

theorem canonicalPathLimit_eq_terminal_of_le
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (B : ℝ≥0 → Omega → ℝ) (omega : Omega)
    {t : ℝ≥0} (hTt : T ≤ t) :
    canonicalPathLimit eta hT B t omega =
      canonicalPathLimit eta hT B T omega := by
  unfold canonicalPathLimit
  congr 1
  funext n
  exact congrFun
    (canonicalItoProcess_eq_terminal_of_le eta hT B n hTt) omega

/-- The patched continuous Itô process is exactly constant after its finite
construction horizon, on every sample path including the null-set patch. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessAfterHorizon.lean:43published source at 7bcd37294df1

- The patched continuous Itô process is exactly constant after its finite construction horizon, on every sample path including the null-set patch.

theorem itoIntegralProcess_eq_terminal_of_le
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    {t : ℝ≥0} (hTt : T ≤ t) :
    itoIntegralProcess eta hT hB hUsual t =
      itoIntegralProcess eta hT hB hUsual T := by
  funext omega
  classical
  by_cases hbad : omega ∈ uniformBadSet eta hT B
  · simp [itoIntegralProcess, hbad]
  · simp only [itoIntegralProcess, hbad, if_false]
    exact canonicalPathLimit_eq_terminal_of_le eta hT B omega hTt

/-- A finite-horizon completed Itô version is in fact continuous on the whole
nonnegative time axis: it is continuous on `[0,T]` and exactly constant on
`[T,∞)`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessAfterHorizon.lean:58published source at 7bcd37294df1

- A finite-horizon completed Itô version is in fact continuous on the whole nonnegative time axis: it is continuous on `[0,T]` and exactly constant on `[T,∞)`.

theorem itoIntegralProcess_continuous
    [IsFiniteMeasure mu]
    (eta : ProgressiveL2Integrand filtration mu T) (hT : 0 < T)
    (hB : IsBrownianMotionWithFiltration B filtration mu)
    (hUsual : SatisfiesUsualConditions filtration mu)
    (omega : Omega) :
    Continuous (fun t => itoIntegralProcess eta hT hB hUsual t omega) := by
  rw [← continuousOn_univ]
  have huniv : (Set.univ : Set ℝ≥0) = Set.Iic T ∪ Set.Ici T := by
    ext t
    simp only [Set.mem_univ, Set.mem_union, Set.mem_Iic, Set.mem_Ici, true_iff]
    exact le_total t T
  rw [huniv]
  apply ContinuousOn.union_of_isClosed
  · have hleft := itoIntegralProcess_continuousOn eta hT hB hUsual omega
    have hset : Set.Icc (0 : ℝ≥0) T = Set.Iic T := by
      ext t
      simp
    rw [hset] at hleft
    exact hleft
  · have hconst : ContinuousOn
        (fun _ : ℝ≥0 => itoIntegralProcess eta hT hB hUsual T omega)
        (Set.Ici T) := continuousOn_const
    apply hconst.congr
    intro t ht
    exact congrFun
      (itoIntegralProcess_eq_terminal_of_le eta hT hB hUsual ht) omega
  · exact isClosed_Iic
  · exact isClosed_Ici

/-- If a stopping time is pointwise bounded by `T`, its stopped process is
exactly constant after `T`, independently of any stochastic assumptions. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessAfterHorizon.lean:76published source at 7bcd37294df1

- If a stopping time is pointwise bounded by `T`, its stopped process is exactly constant after `T`, independently of any stochastic assumptions.

theorem stoppedProcess_eq_terminal_of_le
    {beta : Type*} (u : ℝ≥0 → Omega → beta)
    (tau : Omega → WithTop ℝ≥0)
    (htauT : ∀ omega, tau omega ≤ (T : WithTop ℝ≥0))
    {t : ℝ≥0} (hTt : T ≤ t) :
    stoppedProcess u tau t = stoppedProcess u tau T := by
  funext omega
  unfold stoppedProcess
  have htau_t : tau omega ≤ (t : WithTop ℝ≥0) :=
    (htauT omega).trans (WithTop.coe_le_coe.mpr hTt)
  rw [min_eq_right htau_t, min_eq_right (htauT omega)]

end ItoIntegralProcessAfterHorizon
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessAfterHorizon.lean:108published source at 7bcd37294df1