OAI/Probability/SLE/Loewner/StoppedDriverConcatenation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Reconstruct the old driver through τ+t from its stopped past at τ and the fresh prefix through t. The reconstruction is jointly measurable in exactly those two past sigma algebras.

  1. def OAI.SLEExactGauge.restartDriverPathAt line 18
  2. def OAI.SLEExactGauge.concatenateDriverPath line 22
  3. lemma OAI.SLEExactGauge.measurable_concatenateDriverPath line 33
  4. theorem OAI.SLEExactGauge.stoppedDriverPath_concatenation line 49
  5. lemma OAI.SLEExactGauge.restartDriverPathAt_add line 64
  6. lemma OAI.SLEExactGauge.concatenate_stopped_restart line 71
  7. lemma OAI.SLEExactGauge.sourceRestartDriverPath_add line 82
  8. lemma OAI.SLEExactGauge.sourceRestartDriverPath_split line 89
  9. lemma OAI.SLEExactGauge.source_stoppedDriverPath_measurable line 98
  10. lemma OAI.SLEExactGauge.source_stoppedDriverTime_measurable line 117
  11. theorem OAI.SLEExactGauge.measurable_past_fresh_prefix_concatenation line 126
  12. theorem OAI.SLEExactGauge.source_stoppedDriverPath_restart_identity line 140