OAI/Geometry/RCD/Heat/HeatPlanWeakVelocity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Physical-time weak velocity of the actual heat limit

The local heat representative has gradient length twice the metric speed. Its gradient pairing gives the signed physical-time mean variation.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.heat_plan_weak_velocity_of_representative line 29
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.heat_plan_weak_velocity line 91