AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiItoProcess

- Source-shaped coefficient data for Chewi Definition 1.1.17. `driftIntegrable` is the Bochner formulation of the textbook's condition `∫ ‖b_s‖ ds < ∞`: for a progressive finite-dimensional process it records strong measurability together with local integrability of the norm. The diffusion condition is kept literally as the squared Euclidean/Frobenius norm through `MatrixLocallySquareIntegrableNormOn`.

structure SourceData where
  initial : Omega → EuclideanSpace ℝ iota
  initialStronglyMeasurable : StronglyMeasurable[filtration 0] initial
  drift : ℝ≥0 → Omega → EuclideanSpace ℝ iota
  driftProgressive : IsStronglyProgressive filtration drift
  driftIntegrable : ∀ T : ℝ≥0,
    ∀ᵐ omega ∂mu,
      Integrable (fun t => drift t omega) (TimeMeasure.upTo T)
  diffusion : ℝ≥0 → Omega → iota → kappa → ℝ
  diffusionProgressive :
    IsStronglyProgressive filtration
      (fun t omega => matrixAsEuclidean (diffusion t omega))
  diffusionSquareIntegrable : ∀ T : ℝ≥0,
    MatrixLocallySquareIntegrableNormOn diffusion mu T

/-- Initial-value measurability descends from the Euclidean vector to each
coordinate by the norm-one continuous coordinate functional. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:52published source at 7bcd37294df1

- Initial-value measurability descends from the Euclidean vector to each coordinate by the norm-one continuous coordinate functional.

theorem SourceData.initial_coordinate_stronglyMeasurable
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    (i : iota) :
    StronglyMeasurable[filtration 0] (fun omega => data.initial omega i) := by
  simpa only [coordinateDual_apply] using
    (coordinateDual i).continuous.comp_stronglyMeasurable
      data.initialStronglyMeasurable

/-- Progressive measurability of the vector drift descends to each scalar
coordinate. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:69published source at 7bcd37294df1

- Progressive measurability of the vector drift descends to each scalar coordinate.

theorem SourceData.drift_coordinate_progressive
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    (i : iota) :
    IsStronglyProgressive filtration (fun t omega => data.drift t omega i) := by
  intro T
  simpa only [coordinateDual_apply] using
    (coordinateDual i).continuous.comp_stronglyMeasurable
      (data.driftProgressive T)

/-- Local Bochner integrability of the vector drift implies local integrability
of every scalar coordinate. This is a continuous-linear-map consequence, not
an additional coordinatewise assumption. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:80published source at 7bcd37294df1

- Local Bochner integrability of the vector drift implies local integrability of every scalar coordinate. This is a continuous-linear-map consequence, not an additional coordinatewise assumption.

theorem SourceData.drift_coordinate_integrable
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    (i : iota) (T : ℝ≥0) :
    ∀ᵐ omega ∂mu,
      Integrable (fun t => data.drift t omega i) (TimeMeasure.upTo T) := by
  filter_upwards [data.driftIntegrable T] with omega hOmega
  simpa only [coordinateDual_apply] using
    (coordinateDual i).integrable_comp hOmega

/-- Progressive measurability of the flattened matrix process descends to each
matrix entry. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:93published source at 7bcd37294df1

- Progressive measurability of the flattened matrix process descends to each matrix entry.

theorem SourceData.diffusion_entry_progressive
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu))
    (i : iota) (j : kappa) :
    IsStronglyProgressive filtration
      (fun t omega => data.diffusion t omega i j) := by
  intro T
  have h :=
    (coordinateDual (i, j)).continuous.comp_stronglyMeasurable
      (data.diffusionProgressive T)
  simpa [matrixAsEuclidean, coordinateDual_apply] using h

/-- Compile Chewi's vector/matrix source coefficients into the scalar
coordinate ABI used by the Chapter 1 Itô integral. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:105published source at 7bcd37294df1

- Compile Chewi's vector/matrix source coefficients into the scalar coordinate ABI used by the Chapter 1 Itô integral.

noncomputable def SourceData.toCoordinateItoData
    (data : SourceData (Omega := Omega) (iota := iota) (kappa := kappa)
      (filtration := filtration) (mu := mu)) :
    CoordinateItoData (filtration := filtration) (mu := mu) iota kappa where
  initial omega i := data.initial omega i
  initialStronglyMeasurable i := data.initial_coordinate_stronglyMeasurable i
  drift i t omega := data.drift t omega i
  driftProgressive i := data.drift_coordinate_progressive i
  driftIntegrable i T := data.drift_coordinate_integrable i T
  diffusion i j :=
    entryGlobalLocalProgressiveL2
      (fun i' j' => data.diffusion_entry_progressive i' j')
      data.diffusionSquareIntegrable i j

/-- The source-facing Itô process associated with `SourceData` and one
Euclidean Brownian driver. Internally this is assembled coordinatewise from
the scalar global Itô integral, then repackaged as one Euclidean vector. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:119published source at 7bcd37294df1

- The source-facing Itô process associated with `SourceData` and one Euclidean Brownian driver. Internally this is assembled coordinatewise from the scalar global Itô integral, then repackaged as one Euclidean vector.

noncomputable def process
    [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) :
    ℝ≥0 → Omega → EuclideanSpace ℝ iota :=
  fun t omega =>
    WithLp.toLp 2
      (coordinateItoProcess hUsual data.toCoordinateItoData
        (coordinateFamily hB) t omega)

/-- Chewi Definition 1.1.17, displayed at an arbitrary state coordinate.
The stochastic term is a finite sum over coordinates of the same
`R^N`-valued Brownian motion. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:136published source at 7bcd37294df1

- Chewi Definition 1.1.17, displayed at an arbitrary state coordinate. The stochastic term is a finite sum over coordinates of the same `R^N`-valued Brownian motion.

theorem definition_1_1_17_coordinate_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) (omega : Omega) (i : iota) :
    process hUsual data hB t omega i =
      data.initial omega i +
        (∫ s, data.drift s omega i ∂(TimeMeasure.upTo t)) +
        ∑ j,
          GlobalItoProcessGluing.globalItoProcess hUsual
            ((data.toCoordinateItoData).diffusion i j)
            ((coordinateFamily hB).isBrownian j) t omega := by
  rfl

/-- Literal textbook dimensions: state space `R^d` and Brownian space `R^N`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:152published source at 7bcd37294df1

- Literal textbook dimensions: state space `R^d` and Brownian space `R^N`.

abbrev ChewiSourceData (d N : ℕ)
    (filtration : Filtration ℝ≥0 m) (mu : Measure Omega) :=
  SourceData (Omega := Omega) (iota := Fin d) (kappa := Fin N)
    (filtration := filtration) (mu := mu)

end ChewiItoProcess
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean:170published source at 7bcd37294df1