OAI/Probability/SLE/Mass/SignedLevelTests.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real compact tests of the actual level measures. Both signs are controlled by the same compact moment estimate.

  1. def OAI.SLEExactGauge.Multipoint.levelApproximationRealTest line 14
  2. lemma OAI.SLEExactGauge.Multipoint.integrable_of_bounded_support line 19
  3. lemma OAI.SLEExactGauge.Multipoint.levelApproximationRealTest_measurable line 31
  4. lemma OAI.SLEExactGauge.Multipoint.levelApproximationRealTest_eq_parts line 51
  5. theorem OAI.SLEExactGauge.Multipoint.levelMass_ae_finite line 65
  6. theorem OAI.SLEExactGauge.Multipoint.uniform_signed_levelTest_L2 line 81