OAI/Probability/SLE/Mass/CompactLevelMoments.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Integrating the actual multipoint bound on an interior compact set. The bound is independent of the common radius level.

  1. lemma OAI.SLEExactGauge.Multipoint.ae_tuple_mem line 15
  2. lemma OAI.SLEExactGauge.Multipoint.compact_positive_radius_cap line 21
  3. def OAI.SLEExactGauge.Multipoint.compactLevelMomentBound line 25
  4. theorem OAI.SLEExactGauge.Multipoint.levelMass_moment_le_cappedKernel line 30
  5. lemma OAI.SLEExactGauge.Multipoint.compactLevelMomentBound_lt_top line 61
  6. theorem OAI.SLEExactGauge.Multipoint.uniform_levelMass_compact_moments line 68
  7. theorem OAI.SLEExactGauge.Multipoint.uniform_levelApproximation_compact_moments line 86
  8. def OAI.SLEExactGauge.Multipoint.centeredLevelMomentBound line 104
  9. theorem OAI.SLEExactGauge.Multipoint.levelMass_centered_moment_le_cappedKernel line 109
  10. theorem OAI.SLEExactGauge.Multipoint.uniform_levelMass_centered_compact_moments line 168