production module

`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessProgressive`

1 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalItoProcessProgressive.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessGluing

Imported by

AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcessProgressiveTests.Chapter1ProgressiveAPITests.GlobalItoProcessProgressive

Placeholder scan

0 declaration(s) flagged

Gate status

Compiled

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessProgressive.globalItoProcess_stronglyProgressive Compiled Not mapped

- The everywhere-continuous, strongly adapted global Itô integral built for Chewi Proposition 1.1.16 is strongly progressive.

theorem globalItoProcess_stronglyProgressive
    [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    (hB : IsBrownianMotionWithFiltration B filtration mu) :
    IsStronglyProgressive filtration
      (globalItoProcess hUsual eta hB) :=
  (globalItoProcess_stronglyAdapted hUsual eta hB).isStronglyProgressive_of_continuous
    (globalItoProcess_continuous hUsual eta hB)

end GlobalItoProcessProgressive
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalItoProcessProgressive.lean:29published source at 7bcd37294df1