OAI/Geometry/RCD/Heat/HeatGamma.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The energy density of an actual heat solution is Sobolev

The weak Bochner inequality is tested against heat regularizations of the same nonnegative energy density. Its bounded amplitude controls the mixed term uniformly as the regularization time tends to zero.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_gamma_finite_energy line 20