OAI/Geometry/RCD/Heat/HeatSobolevWeightedBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Dimensional heat estimate on the actual Sobolev space

Compact recovery of the minimal relaxed gradient and continuity of the positive-time heat generator pass both nonnegative terms to the limit.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_weighted_generator_bochner line 17