OAI/Probability/SLE/Stochastic/DriverPastFactorization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real continuous driver prefixes realize the natural filtration. Radon kernels adapted to that filtration factor through each stopped prefix.

  1. def OAI.SLEExactGauge.driverPathStopped line 20
  2. def OAI.SLEExactGauge.driverPathFiltration line 23
  3. lemma OAI.SLEExactGauge.driverPathStopped_eq_of_agree line 27
  4. lemma OAI.SLEExactGauge.driverPathStopped_measurable_past line 33
  5. lemma OAI.SLEExactGauge.natural_le_stoppedDriverPath_comap line 44
  6. lemma OAI.SLEExactGauge.exists_stopped_driver_radon_factor line 61