OAI/Geometry/RCD/Sobolev/HessianVelocityPolarization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Velocity and logarithmic-density polarization of the Hessian action

  1. theorem OAI.RegularPointCoordinates.localGamma_sub_right line 13
  2. theorem OAI.RegularPointCoordinates.localHessianAction_velocity_polarization line 20
  3. theorem OAI.RegularPointCoordinates.localGamma_velocity_square_reps line 38