OAI/Probability/SLE/Loewner/StoppedInverseTerminalBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The transported fresh terminal mass is locally integrable. The bound comes from the original canonical Green kernel at the stopping time.

  1. lemma OAI.SLEExactGauge.Multipoint.halfPlaneStoppingGreenMeasure_finite_time line 19
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.green_at_finite_stop_mean_le line 27
  3. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.stoppedFreshTerminalMass_mean_le line 60
  4. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.stoppedFreshTerminalMass_ae_finite_on_compacts line 69