AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDisplay1_1_18

- Source-faithful meaning of Chewi display (1.1.18). The notation `dX_t = b_t dt + sigma_t dB_t` means exactly that the source finite-dimensional Itô process satisfies the vector integral equation from Definition 1.1.17 at every deterministic time, almost surely.

theorem chewi_display_1_1_18_integral_meaning
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : ChewiItoProcess.SourceData
      (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    {B : ℝ≥0 → Omega → EuclideanSpace ℝ kappa}
    (hB : BrownianMotion.IsStandardBrownianMotionWithFiltration B filtration mu)
    (t : ℝ≥0) :
    ChewiItoProcess.process hUsual data hB t =ᵐ[mu] fun omega =>
      data.initial omega +
        (∫ s, data.drift s omega ∂(TimeMeasure.upTo t)) +
        ChewiDefinition1_1_17.stochasticIntegral hUsual data hB t omega :=
  ChewiDefinition1_1_17.definition_1_1_17_vector_display hUsual data hB t

end ChewiDisplay1_1_18
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiDisplay1_1_18.lean:38published source at 7bcd37294df1