OAI/Probability/SLE/Mass/LevelRadonTwoPoint.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted two-point control of the actual limiting Radon measure. Finite spatial cutoff sums are bounded by the near-diagonal kernel.

  1. theorem OAI.SLEExactGauge.Multipoint.level_radon_limit_test_moment_le_cappedKernel line 15
  2. theorem OAI.SLEExactGauge.Multipoint.level_radon_cutoff_square_sum_le line 48