AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcess

- Scalar Brownian coordinates equipped with the filtration contract required by the Chapter 1 stochastic-integral construction. This is an integration-facing interface. It intentionally does not claim that coordinatewise Brownianity alone is the full source definition of an `N`-dimensional Brownian motion; the joint-law bridge is a separate theorem.

structure CoordinateBrownianFamilyWithFiltration (kappa : Type*) where
  process : kappa → ℝ≥0 → Omega → ℝ
  isBrownian : ∀ j,
    IsBrownianMotionWithFiltration (process j) filtration mu

/-- Coordinate data behind a finite-dimensional Itô process.

`iota` indexes state coordinates and `kappa` indexes Brownian coordinates.
The diffusion field stores one already-audited globally locally square
integrable progressive scalar process for every matrix entry `sigma^{i,j}`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean:54published source at 7bcd37294df1

- Coordinate data behind a finite-dimensional Itô process. `iota` indexes state coordinates and `kappa` indexes Brownian coordinates. The diffusion field stores one already-audited globally locally square integrable progressive scalar process for every matrix entry `sigma^{i,j}`.

structure CoordinateItoData (iota kappa : Type*) where
  initial : Omega → iota → ℝ
  initialStronglyMeasurable : ∀ i,
    StronglyMeasurable[filtration 0] (fun omega => initial omega i)
  drift : iota → ℝ≥0 → Omega → ℝ
  driftProgressive : ∀ i, IsStronglyProgressive filtration (drift i)
  driftIntegrable : ∀ i (T : ℝ≥0),
    ∀ᵐ omega ∂mu,
      Integrable (fun t => drift i t omega) (TimeMeasure.upTo T)
  diffusion : iota → kappa → GlobalLocalProgressiveL2Integrand filtration mu

/-- The finite-coordinate stochastic integral
`sum_j integral sigma^{i,j} dB^j` built exclusively from the scalar global
local Itô integral already proved in Chewi Proposition 1.1.16. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean:64published source at 7bcd37294df1

- The finite-coordinate stochastic integral `sum_j integral sigma^{i,j} dB^j` built exclusively from the scalar global local Itô integral already proved in Chewi Proposition 1.1.16.

noncomputable def coordinateStochasticTerm
    {iota kappa : Type*} [Fintype kappa]
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : CoordinateItoData (filtration := filtration) (mu := mu) iota kappa)
    (brownian : CoordinateBrownianFamilyWithFiltration
      (filtration := filtration) (mu := mu) kappa)
    (t : ℝ≥0) (omega : Omega) (i : iota) : ℝ :=
  ∑ j,
    globalItoProcess hUsual (data.diffusion i j) (brownian.isBrownian j) t omega

/-- The coordinatewise finite-dimensional Itô process associated with the
source data.  Lebesgue time integration uses exactly the same `TimeMeasure.upTo`
measure as the stochastic-integration foundation, so endpoint conventions stay
consistent across both terms. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean:78published source at 7bcd37294df1

- The coordinatewise finite-dimensional Itô process associated with the source data. Lebesgue time integration uses exactly the same `TimeMeasure.upTo` measure as the stochastic-integration foundation, so endpoint conventions stay consistent across both terms.

noncomputable def coordinateItoProcess
    {iota kappa : Type*} [Fintype kappa]
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : CoordinateItoData (filtration := filtration) (mu := mu) iota kappa)
    (brownian : CoordinateBrownianFamilyWithFiltration
      (filtration := filtration) (mu := mu) kappa) :
    ℝ≥0 → Omega → iota → ℝ :=
  fun t omega i =>
    data.initial omega i +
      (∫ s, data.drift i s omega ∂(TimeMeasure.upTo t)) +
      coordinateStochasticTerm hUsual data brownian t omega i

/-- Coordinate display behind Chewi Definition 1.1.17.

This theorem is intentionally named `coordinate_display`: it certifies the
finite-sum assembly but does not by itself close the source item.  Source
completion additionally needs the vector-Brownian-to-coordinate bridge and the
finite-dimensional Hilbert--Schmidt/local-`L^2` equivalence. -/

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

- Coordinate display behind Chewi Definition 1.1.17. This theorem is intentionally named `coordinate_display`: it certifies the finite-sum assembly but does not by itself close the source item. Source completion additionally needs the vector-Brownian-to-coordinate bridge and the finite-dimensional Hilbert--Schmidt/local-`L^2` equivalence.

theorem chewi_definition_1_1_17_coordinate_display
    {iota kappa : Type*} [Fintype kappa]
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (data : CoordinateItoData (filtration := filtration) (mu := mu) iota kappa)
    (brownian : CoordinateBrownianFamilyWithFiltration
      (filtration := filtration) (mu := mu) kappa)
    (t : ℝ≥0) (omega : Omega) (i : iota) :
    coordinateItoProcess hUsual data brownian t omega i =
      data.initial omega i +
        (∫ s, data.drift i s omega ∂(TimeMeasure.upTo t)) +
        ∑ j,
          globalItoProcess hUsual (data.diffusion i j)
            (brownian.isBrownian j) t omega :=
  rfl

/-- Chewi's literal finite dimensions are obtained by taking state coordinates
`Fin d` and Brownian coordinates `Fin N`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean:112published source at 7bcd37294df1

- Chewi's literal finite dimensions are obtained by taking state coordinates `Fin d` and Brownian coordinates `Fin N`.

abbrev ChewiItoData (d N : ℕ)
    (filtration : Filtration ℝ≥0 m) (mu : Measure Omega) :=
  CoordinateItoData (Omega := Omega) (filtration := filtration) (mu := mu)
    (Fin d) (Fin N)

/-- Integration-facing Brownian-coordinate contract for the literal `N`
coordinates in Chewi Definition 1.1.17. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean:130published source at 7bcd37294df1

- Integration-facing Brownian-coordinate contract for the literal `N` coordinates in Chewi Definition 1.1.17.

abbrev ChewiBrownianCoordinates (N : ℕ)
    (filtration : Filtration ℝ≥0 m) (mu : Measure Omega) :=
  CoordinateBrownianFamilyWithFiltration (Omega := Omega)
    (filtration := filtration) (mu := mu) (Fin N)

end FiniteDimensionalItoProcess
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean:137published source at 7bcd37294df1