OAI/Geometry/RCD/Heat/CompactHeatVelocityPotential.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual logarithmic velocity and its uniform local gradient

  1. def OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.velocityPotential line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.CompactHeatScalingData.velocity_local_gradient line 27