OAI/Probability/SLE/Mass/LevelApproximationTests.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Bounded nonnegative tests of the actual finite-level measures inherit the compact moment bounds used for simultaneous convex extraction.

  1. def OAI.SLEExactGauge.Multipoint.levelApproximationTest line 14
  2. lemma OAI.SLEExactGauge.Multipoint.lintegral_le_const_mul_measure_of_support line 19
  3. lemma OAI.SLEExactGauge.Multipoint.levelApproximationTest_le line 29
  4. lemma OAI.SLEExactGauge.Multipoint.levelApproximationTest_measurable line 41
  5. theorem OAI.SLEExactGauge.Multipoint.uniform_levelApproximationTest_moments line 57