OAI/Geometry/RCD/Heat/FirstOrderHeatMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A vanishing full-mass heat approximation of each original splitting coordinate

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.first_order_heat_mass line 15