OAI/Probability/SLE/Geometry/CanonicalDiskPotential.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The source-prescribed disk potential is the remaining canonical disk mass, with exactly the source's Brownian clock normalization.

  1. def OAI.SLEExactGauge.Multipoint.CanonicalMass.diskScalar line 20
  2. def OAI.SLEExactGauge.Multipoint.CanonicalMass.diskTerminalScalar line 23
  3. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.target_potential_condExp line 27
  4. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.target_potential_lintegral_ne_top line 51