OAI/Probability/SLE/Mass/LevelRadonMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Every compact moment bound passes from the actual level measures to any of their common convex Radon limits.

  1. lemma OAI.SLEExactGauge.Multipoint.extendHalfPlaneTest_nonneg line 17
  2. lemma OAI.SLEExactGauge.Multipoint.ofReal_integral_halfPlaneLevelMeasure line 24
  3. theorem OAI.SLEExactGauge.Multipoint.uniform_halfPlaneLevelMeasure_test_moments line 44
  4. theorem OAI.SLEExactGauge.Multipoint.uniform_convexLevelMeasure_test_moments line 68
  5. theorem OAI.SLEExactGauge.Multipoint.level_radon_limit_test_moments line 96
  6. lemma OAI.SLEExactGauge.Multipoint.measure_compact_le_nonneg_test line 122
  7. theorem OAI.SLEExactGauge.Multipoint.level_radon_limit_compact_moments line 137