OAI/Probability/SLE/Loewner/StoppedInversePaths.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The finite fresh mass transported by the actual stopped inverse chart. The same raw functional is used for all finite stopping times.

  1. lemma OAI.SLEExactGauge.weightedImageMass_mono line 18
  2. lemma OAI.SLEExactGauge.weightedImageMass_zero line 27
  3. lemma OAI.SLEExactGauge.weightedImageMass_finite_on_compacts line 31
  4. lemma OAI.SLEExactGauge.weightedImageMass_positive_test_continuous line 38
  5. lemma OAI.SLEExactGauge.positive_test_integral_measurable line 70
  6. structure OAI.SLEExactGauge.PositiveMassPaths line 82
  7. lemma OAI.SLEExactGauge.weightedImageMass_positive_paths line 90
  8. def OAI.SLEExactGauge.Multipoint.stoppedFreshMass line 121
  9. theorem OAI.SLEExactGauge.Multipoint.stoppedFreshMass_adapted line 130
  10. theorem OAI.SLEExactGauge.Multipoint.stoppedFreshMass_paths line 149
  11. theorem OAI.SLEExactGauge.Multipoint.stoppedFreshMass_positive_test_adapted line 186