OAI/Geometry/RCD/Harmonic/EuclideanQuadraticDefect.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Derivatives of the quadratic defining an interior torsion test

  1. def OAI.RegularPointCoordinates.euclideanQuadraticDefect line 13
  2. theorem OAI.RegularPointCoordinates.euclideanQuadraticDefect_smooth line 15
  3. theorem OAI.RegularPointCoordinates.euclideanQuadraticDefect_fderiv line 19
  4. theorem OAI.RegularPointCoordinates.euclideanQuadraticDefect_basis line 27
  5. theorem OAI.RegularPointCoordinates.euclideanQuadraticDefect_laplacian line 32
  6. theorem OAI.RegularPointCoordinates.euclideanQuadraticDefect_gradient_sq line 47