OAI/Geometry/RCD/Harmonic/LocalVelocityIdentification.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing the auxiliary compact contact representative

Equality with a scaled heat slice on the transported measure identifies both its gradient length and every weak velocity pairing.

  1. theorem OAI.RegularPointCoordinates.scaled_contact_gradient_length line 18
  2. theorem OAI.RegularPointCoordinates.scaled_contact_gradient_ratio line 44
  3. theorem OAI.RegularPointCoordinates.scaled_contact_velocity_pair line 59