AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiItoProcessProgressive
import Mathlib.MeasureTheory.SpecificCodomains.WithLp

/-!
# Chewi Definition 1.1.17: vector-valued completion

This module is the source-facing closure theorem for Definition 1.1.17.
It deliberately keeps the textbook's finite-dimensional vector equation rather
than exposing only the scalar coordinate ABI used to construct the integral.

The drift hypothesis in the source is pathwise local integrability only almost
surely.  Consequently the vector integral equation is asserted almost surely
for each deterministic time; no stronger pointwise integrability assumption is
silently introduced.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace StochasticProcesses
namespace ChewiDefinition1_1_17

open MeasureTheory
open scoped NNReal RealInnerProductSpace

open BrownianMotion
open EuclideanBrownianCoordinates
open FiniteDimensionalItoProcess
open ProgressiveL2
open ChewiItoProcess

variable {Omega iota kappa : Type*} [MeasurableSpace Omega]
  [Fintype iota] [DecidableEq iota]
  [Fintype kappa] [DecidableEq kappa]
  {m : MeasurableSpace Omega}
  {filtration : Filtration ℝ≥0 m} {mu : Measure Omega}

/-- 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. -/
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. -/
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`. -/
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. -/
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