OAI/Geometry/RCD/Heat/HeatOverlapKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A symmetric lower-semicontinuous version of the heat overlap

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel line 22

    Source documentation

    Increasing continuous capped overlaps define an extended-real kernel. Pointwise finiteness is kept separate from this construction.

    def heatOverlapKernel (t : ℝ) (ht : 0 < t) (x y : X) : ℝ≥0∞ :=
…
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel_lowerSemicontinuous line 25
  3. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel_symmetric line 32
  4. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel_eq_lintegral line 37
  5. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heatOverlapKernel_ae line 83

    Source documentation

    At each starting point the symmetric overlap is the actual heat density at double time, up to a null set of endpoints.

    theorem heatOverlapKernel_ae (t : ℝ) (ht : 0 < t) (x : X) :
    hX.heatOverlapKernel hn p t ht x =ᵐ[hausdorff n X]
      fun y => ENNReal.ofReal (hX.heatJointDensity hn p (t+t) (add_pos ht ht) x y) := by
…

    Mentions: OAI.RegularPointCoordinates.hausdorff