OAI/Probability/SLE/Geometry/CanonicalRawTerminal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Terminal extension of the fixed raw canonical mass functional. Its integer-time vague limit agrees with the locally exhausted terminal mass.

  1. structure OAI.SLEExactGauge.Multipoint.RawCanonicalMass line 19
  2. def OAI.SLEExactGauge.Multipoint.rawTerminalMass line 28
  3. lemma OAI.SLEExactGauge.Multipoint.rawTerminalMass_measurable line 32
  4. lemma OAI.SLEExactGauge.Multipoint.rawTerminalMass_radon line 43
  5. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.rawTerminal_realizes line 49
  6. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_raw_canonical line 67