OAI/Geometry/RCD/Heat/HeatPlanFirstVariation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual heat envelope represents the transport velocity

On every reversed interior subpath the compact Sobolev contact potential agrees with the prescribed heat envelope throughout the working ball. Its minimal gradient and signed first variation are derived, not assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.heat_plan_first_variation line 28