OAI/Geometry/RCD/Heat/HeatGammaSobolev.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Sobolev regularity of heat energy densities from weak Bochner

Testing the actual weak Bochner inequality with heat regularizations of the energy density bounds their Dirichlet energies uniformly. Lower semicontinuity then puts the density itself in the Sobolev space.

  1. theorem OAI.RegularPointCoordinates.energyLp_le_of_heat_energy_bound line 21