OAI/Geometry/RCD/Heat/KernelHeatL2Representation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Kernel representation for every L2 datum

Compact Lipschitz data are dense in L2. The L2 kernel row gives pointwise convergence, and a subsequence of the actual heat evolutions identifies the resulting continuous representative.

  1. theorem OAI.RegularPointCoordinates.lp_integrable_dense line 21
  2. theorem OAI.RegularPointCoordinates.kernelHeat_represents_L2 line 36