OAI/Geometry/RCD/Heat/BoundedHeatComplement.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Approximating the bounded complement in the conservative heat kernel

The complement of an L2 function need not be in L2 on an infinite-volume space. Finite-ball truncations stay in L2 and their heat values converge to the exact bounded complement, by mass conservation.

  1. theorem OAI.RegularPointCoordinates.bounded_heat_complement_sequence line 21