AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessGlobalContinuity

- The completed finite-horizon Itô process is globally continuous because it is constant after the construction horizon.

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
  let f : ℝ≥0 → ℝ := fun t => itoIntegralProcess eta hT hB hUsual t omega
  have hleft : ContinuousOn f (Iic T) := by
    apply (itoIntegralProcess_continuousOn eta hT hB hUsual omega).mono
    intro t ht
    exact ⟨zero_le t, ht⟩
  have hright : ContinuousOn f (Ici T) := by
    have hconst : ContinuousOn (fun _ : ℝ≥0 => f T) (Ici T) :=
      continuousOn_const
    apply hconst.congr
    intro t ht
    symm
    simpa only [f] using
      itoIntegralProcess_eq_terminal_of_le eta hT hB hUsual ht
  have hclosed : ContinuousOn f (Iic T ∪ Ici T) :=
    hleft.union_of_isClosed hright isClosed_Iic isClosed_Ici
  have huniv : Iic T ∪ Ici T = (Set.univ : Set ℝ≥0) := by
    ext t
    simp only [mem_union, mem_Iic, mem_Ici, mem_univ, iff_true]
    exact le_total t T
  rw [huniv, continuousOn_univ] at hclosed
  exact hclosed

end ItoIntegralProcessGlobalContinuity
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessGlobalContinuity.lean:29published source at 77184245109a