AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcessProgressive

- A time-constant initial coordinate is progressive once its `F_0` measurability is known.

theorem initialCoordinateProcess_stronglyProgressive
    {iota kappa : Type*}
    (data : CoordinateItoData (filtration := filtration) (mu := mu) iota kappa)
    (i : iota) :
    IsStronglyProgressive filtration (fun _ omega => data.initial omega i) := by
  have hAdapted :
      StronglyAdapted filtration (fun _ omega => data.initial omega i) := by
    intro t
    exact (data.initialStronglyMeasurable i).mono (filtration.mono bot_le)
  exact hAdapted.isStronglyProgressive_of_continuous (fun _ => continuous_const)

/-- The finite stochastic sum over Brownian coordinates is progressive. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcessProgressive.lean:32published source at 7bcd37294df1

- The finite stochastic sum over Brownian coordinates is progressive.

theorem coordinateStochasticTerm_stronglyProgressive
    {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)
    (i : iota) :
    IsStronglyProgressive filtration
      (fun t omega => coordinateStochasticTerm hUsual data brownian t omega i) := by
  unfold coordinateStochasticTerm
  simpa only using
    (IsStronglyProgressive.finsetSum (s := Finset.univ)
      (fun j _ =>
        globalItoProcess_stronglyProgressive hUsual
          (data.diffusion i j) (brownian.isBrownian j)))

/-- Every scalar coordinate of the finite-dimensional Itô process is strongly
progressive. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcessProgressive.lean:44published source at 7bcd37294df1

- Every scalar coordinate of the finite-dimensional Itô process is strongly progressive.

theorem coordinateItoProcess_coordinate_stronglyProgressive
    {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)
    (i : iota) :
    IsStronglyProgressive filtration
      (fun t omega => coordinateItoProcess hUsual data brownian t omega i) := by
  change IsStronglyProgressive filtration
    (fun t omega =>
      data.initial omega i +
        prefixIntegralProcess (data.drift i) t omega +
        coordinateStochasticTerm hUsual data brownian t omega i)
  exact
    ((initialCoordinateProcess_stronglyProgressive data i).add
      (prefixIntegralProcess_stronglyProgressive (data.drift i)
        (data.driftProgressive i))).add
      (coordinateStochasticTerm_stronglyProgressive hUsual data brownian i)

end FiniteDimensionalItoProcessProgressive
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcessProgressive.lean:63published source at 7bcd37294df1