OAI/Probability/SLE/Mass/CanonicalMassExhaustion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual canonical terminal measure is exhausted by finite times, locally in total variation.

  1. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.mass_ambient_measurable line 19
  2. lemma OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.integer_remaining_mean line 26
  3. theorem OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.finite_times_exhaust_terminal line 52