OAI/Probability/SLE/Loewner/RawRestartAdaptation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed raw mass applied to the fresh driver is progressive in the original filtration shifted by the stopping time. Its continuous increasing paths are transferred on the explicit measurable good set.

  1. lemma OAI.SLEExactGauge.driverPath_measurable_past_of_adapted line 19
  2. theorem OAI.SLEExactGauge.raw_process_comp_progressive line 30
  3. lemma OAI.SLEExactGauge.sourceRestartDriverPath_shifted_adapted line 40
  4. theorem OAI.SLEExactGauge.sourceRestart_raw_process_progressive line 57
  5. theorem OAI.SLEExactGauge.sourceRestart_mem_full_driver_set line 69
  6. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_raw_with_restarted_paths line 89