OAI/Probability/SLE/Gauge/CanonicalGaugeTails.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All prescribed gauge entries have a summable limiting centered-disk tail, including repeated dyadic entries and the cleanup sequence.

  1. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.limitingDiskTail_all_batches_bound line 27
  2. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.limitingDiskTail_summable line 50