OAI/Probability/SLE/Multipoint/NearDiagonalKernel.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integrable two-point kernels have vanishing mass near the diagonal. Finite cutoff sums with bounded overlap inherit this decay.

  1. def OAI.SLEExactGauge.Multipoint.nearDiagonalKernel line 16
  2. lemma OAI.SLEExactGauge.Multipoint.nearDiagonalKernel_measurable line 19
  3. theorem OAI.SLEExactGauge.Multipoint.nearDiagonalKernel_integral_tendsto_zero line 24
  4. lemma OAI.SLEExactGauge.Multipoint.sum_weighted_pair_kernel_le line 45