OAI/Geometry/RCD/Heat/HeatActionStrongGradient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strong local gradient convergence to the constructed heat action

This uses the original convergent subsequence and arbitrary chosen local Sobolev realizations. No further subsequence or gradient premise is needed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatConverges.strong_gradient line 22