OAI/Probability/SLE/Stochastic/ProgressiveRandomTime.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Measurable evaluation of a progressive process at an arbitrary finite random time. The target needs only a measurable-space structure.

  1. theorem OAI.MeasureTheory.IsProgressive.random_time_measurable line 16
  2. theorem OAI.MeasureTheory.IsProgressive.extended_random_time_measurable line 48