AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17

- The vector stochastic term in Chewi Definition 1.1.17. Each state coordinate is the finite sum of scalar Itô integrals against the coordinates of one and the same Euclidean Brownian motion.

noncomputable def stochasticIntegral
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    {B : ℝ≥0 → Omega → EuclideanSpace ℝ kappa}
    (hB : IsStandardBrownianMotionWithFiltration B filtration mu)
    (t : ℝ≥0) (omega : Omega) : EuclideanSpace ℝ iota :=
  WithLp.toLp 2 (fun i =>
    ∑ j,
      GlobalItoProcessGluing.globalItoProcess hUsual
        ((data.toCoordinateItoData).diffusion i j)
        ((coordinateFamily hB).isBrownian j) t omega)

/-- The `i`-th coordinate of the vector stochastic integral is exactly the
finite coordinate sum used by the scalar construction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiDefinition1_1_17.lean:41published source at 7bcd37294df1

- The `i`-th coordinate of the vector stochastic integral is exactly the finite coordinate sum used by the scalar construction.

theorem stochasticIntegral_coordinate
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    {B : ℝ≥0 → Omega → EuclideanSpace ℝ kappa}
    (hB : IsStandardBrownianMotionWithFiltration B filtration mu)
    (t : ℝ≥0) (omega : Omega) (i : iota) :
    stochasticIntegral hUsual data hB t omega i =
      ∑ j,
        GlobalItoProcessGluing.globalItoProcess hUsual
          ((data.toCoordinateItoData).diffusion i j)
          ((coordinateFamily hB).isBrownian j) t omega := by
  rfl

/-- A Bochner integral of the Euclidean drift evaluates coordinatewise.

This is the finite-dimensional bridge needed to turn the already-compiled
coordinate identities into the literal vector equation in the textbook. -/

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

- A Bochner integral of the Euclidean drift evaluates coordinatewise. This is the finite-dimensional bridge needed to turn the already-compiled coordinate identities into the literal vector equation in the textbook.

theorem drift_integral_coordinate
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    {t : ℝ≥0} {omega : Omega}
    (homega : Integrable (fun s => data.drift s omega) (TimeMeasure.upTo t))
    (i : iota) :
    (∫ s, data.drift s omega ∂(TimeMeasure.upTo t)) i =
      ∫ s, data.drift s omega i ∂(TimeMeasure.upTo t) := by
  exact MeasureTheory.eval_integral_piLp (fun j => homega.eval_piLp j) i

/-- Literal vector form of Chewi Definition 1.1.17.

For every deterministic time `t`, the source-facing process satisfies

`X_t = X_0 + ∫_0^t b_s ds + ∫_0^t σ_s dB_s`

almost surely.  The last term is `stochasticIntegral`, whose coordinates are
proved above to be the finite sums of scalar Itô integrals generated by the
single Euclidean Brownian driver `B`. -/

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

- Literal vector form of Chewi Definition 1.1.17. For every deterministic time `t`, the source-facing process satisfies `X_t = X_0 + ∫_0^t b_s ds + ∫_0^t σ_s dB_s` almost surely. The last term is `stochasticIntegral`, whose coordinates are proved above to be the finite sums of scalar Itô integrals generated by the single Euclidean Brownian driver `B`.

theorem definition_1_1_17_vector_display
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    {B : ℝ≥0 → Omega → EuclideanSpace ℝ kappa}
    (hB : IsStandardBrownianMotionWithFiltration B filtration mu)
    (t : ℝ≥0) :
    process hUsual data hB t =ᵐ[mu] fun omega =>
      data.initial omega +
        (∫ s, data.drift s omega ∂(TimeMeasure.upTo t)) +
        stochasticIntegral hUsual data hB t omega := by
  filter_upwards [data.driftIntegrable t] with omega homega
  ext i
  change
    process hUsual data hB t omega i =
      data.initial omega i +
        (∫ s, data.drift s omega ∂(TimeMeasure.upTo t)) i +
        stochasticIntegral hUsual data hB t omega i
  rw [ChewiItoProcess.definition_1_1_17_coordinate_display]
  rw [drift_integral_coordinate data homega i]
  rfl

/-- Source-complete formalization of Chewi Definition 1.1.17.

The theorem records both facts stated around the definition in the textbook:
the vector process is progressive, and it satisfies the finite-dimensional Itô
integral equation under the source hypotheses. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiDefinition1_1_17.lean:95published source at 7bcd37294df1

- Source-complete formalization of Chewi Definition 1.1.17. The theorem records both facts stated around the definition in the textbook: the vector process is progressive, and it satisfies the finite-dimensional Itô integral equation under the source hypotheses.

theorem chewi_definition_1_1_17
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    {B : ℝ≥0 → Omega → EuclideanSpace ℝ kappa}
    (hB : IsStandardBrownianMotionWithFiltration B filtration mu) :
    IsStronglyProgressive filtration (process hUsual data hB) ∧
      ∀ t : ℝ≥0,
        process hUsual data hB t =ᵐ[mu] fun omega =>
          data.initial omega +
            (∫ s, data.drift s omega ∂(TimeMeasure.upTo t)) +
            stochasticIntegral hUsual data hB t omega := by
  exact ⟨ChewiItoProcessProgressive.process_stronglyProgressive
      hUsual data hB,
    fun t => definition_1_1_17_vector_display hUsual data hB t⟩

end ChewiDefinition1_1_17
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiDefinition1_1_17.lean:123published source at 7bcd37294df1