OAI/Geometry/RCD/Sobolev/LipschitzGreenTrace.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The compact-test Laplacian pairing for a Lipschitz Euclidean function

  1. theorem OAI.RegularPointCoordinates.euclidean_gradient_pairing_sum line 14
  2. theorem OAI.RegularPointCoordinates.lipschitz_green_trace line 24