OAI/Geometry/RCD/Heat/HeatCappedOverlap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Continuous bounded approximations to the heat overlap kernel

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap line 19

    Source documentation

    The overlap of two density rows after clipping at a finite height.

    def heatCappedOverlap (t : ℝ) (ht : 0 < t) (C : ℝ≥0) (x y : X) : ℝ :=
…
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap_integrable line 24
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap_nonneg line 32
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap_symmetric line 39
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap_le line 43
  6. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatCappedOverlap_lipschitz line 55