OAI/Geometry/RCD/Heat/HeatCompactWeightedBochner.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Compact weighted dimensional heat estimate

The actual generator term is retained while the output local slope is replaced by the minimal relaxed gradient. Compact initial slope majorants are sufficient for the Sobolev recovery step.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_compact_weighted_generator_bochner line 18