OAI/Probability/SLE/Geometry/CanonicalNormalizedPotential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Canonical remaining mass in the exact clock and natural filtration of the source-prescribed Brownian driver.

  1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.normalized_potential_condExp line 21
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.normalized_potential_lintegral_ne_top line 39
  3. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.normalized_levelTime_measurable line 53