OAI/Probability/SLE/Multipoint/MultipointCappedKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The exact fixed-cap, nearest-neighbor distance kernel from mp:kernel-integral, and its expansion into finite graph terms.

  1. def OAI.SLEExactGauge.Multipoint.capEntry line 15
  2. def OAI.SLEExactGauge.Multipoint.cappedDistance line 19
  3. theorem OAI.SLEExactGauge.Multipoint.cap_pos line 23
  4. theorem OAI.SLEExactGauge.Multipoint.cap_le_fixed line 37
  5. theorem OAI.SLEExactGauge.Multipoint.cap_le_dist line 41
  6. theorem OAI.SLEExactGauge.Multipoint.continuous_cappedDistance line 48
  7. def OAI.SLEExactGauge.Multipoint.cappedDistanceKernel line 60
  8. lemma OAI.SLEExactGauge.Multipoint.measurable_cappedDistanceKernel line 64
  9. def OAI.SLEExactGauge.Multipoint.rowChoice line 70
  10. lemma OAI.SLEExactGauge.Multipoint.cap_reciprocal_le_row line 74
  11. lemma OAI.SLEExactGauge.Multipoint.cappedDistanceKernel_le_expansion line 91