OAI/Probability/SLE/Loewner/TargetDriverContinuation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The prescribed based-driver concatenation is the ordinary Brownian continuation kernel, including its finite real-valued conditional mean.

  1. def OAI.SLEExactGauge.Target.centerDriver line 18
  2. lemma OAI.SLEExactGauge.Target.measurable_centerDriver line 23
  3. lemma OAI.SLEExactGauge.Target.measurable_driverInclusion line 29
  4. lemma OAI.SLEExactGauge.Target.centerDriver_inclusion line 33
  5. lemma OAI.SLEExactGauge.Target.measurable_concat line 38
  6. lemma OAI.SLEExactGauge.Target.centerDriver_concatenate line 54
  7. def OAI.SLEExactGauge.Target.driverFiltration line 65
  8. def OAI.SLEExactGauge.Target.continuationMean line 69
  9. lemma OAI.SLEExactGauge.Target.measurable_continuationMean line 72
  10. lemma OAI.SLEExactGauge.Target.continuationMean_eq_pathMean line 78
  11. lemma OAI.SLEExactGauge.Target.continuationMean_measurable_past line 90
  12. theorem OAI.SLEExactGauge.Target.continuationMean_condLExp line 111
  13. theorem OAI.SLEExactGauge.Target.continuationMean_setLIntegral line 130
  14. theorem OAI.SLEExactGauge.Target.continuationMean_finite_condExp line 138