OAI/Probability/SLE/Mass/LevelApproximationL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform Hilbert bounds and one common deterministic convex extraction for the actual finite-level measure tests.

  1. lemma OAI.SLEExactGauge.Multipoint.eLpNorm_toReal_two_le line 15
  2. lemma OAI.SLEExactGauge.Multipoint.memLp_toReal_two line 30
  3. lemma OAI.SLEExactGauge.Multipoint.norm_toLp_toReal_two_le line 38
  4. theorem OAI.SLEExactGauge.Multipoint.exists_common_levelApproximation_test_limits line 48