OAI/Probability/SLE/Mass/WeightedLevelMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual multipoint estimate with spatial weights retained. This retains the near-diagonal gain needed for nonatomicity.

  1. def OAI.SLEExactGauge.Multipoint.weightedLevelMass line 15
  2. theorem OAI.SLEExactGauge.Multipoint.weightedLevelMass_moment_identity line 21
  3. theorem OAI.SLEExactGauge.Multipoint.actual_product_le_cappedKernel line 44
  4. theorem OAI.SLEExactGauge.Multipoint.weightedLevelMass_moment_le_cappedKernel line 69
  5. lemma OAI.SLEExactGauge.Multipoint.levelApproximationTest_le_weightedLevelMass line 99
  6. theorem OAI.SLEExactGauge.Multipoint.levelApproximationTest_moment_le_cappedKernel line 127
  7. theorem OAI.SLEExactGauge.Multipoint.level_radon_limit_test_moment_le line 149