OAI/Geometry/RCD/Heat/ScaledHeatAveragedGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual averaged heat limit satisfies Hamilton--Jacobi almost everywhere

The gradient and time derivative come from the same Sobolev average. The strict interior ball avoids any assertion at the cutoff boundary.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.scaled_heat_averaged_gradient_of_compactness line 21