OAI/Probability/SLE/Stochastic/ProgressiveParameterTime.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A parameter may choose both the sample and the evaluation time of a progressive process. Finite truncation keeps the original raw sigma algebras.

  1. theorem OAI.MeasureTheory.IsProgressive.parameter_time_measurable line 15