OAI/Probability/SLE/Gauge/CanonicalDiskMomentTails.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Summable tails for the exact prescribed moments, obtained from the actual finite centered laws. The supremum is taken over finite radius levels.

  1. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.finiteMoment_nat_le_moment line 25
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.centeredDiskLaw_integrable_pow line 34
  3. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.centeredDiskLaw_integral_pow line 48
  4. def OAI.SLEExactGauge.Multipoint.CanonicalMass.limitingDiskTail line 61
  5. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.centeredDiskTail_nat_mono line 65
  6. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.limitingDiskTail_batch_bound line 75
  7. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.limitingDiskTail_cleanup_bound line 99