OAI/Geometry/RCD/Harmonic/CenteredHamiltonJacobiPairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The gradient pairing in a fixed constant gauge

The compact test and its weak Laplacian have zero boundary contribution. The Laplacian has total mass zero, so the value pairing uses the same centered potential as the small-noise compactness construction.

  1. theorem OAI.RegularPointCoordinates.local_centered_hamilton_jacobi_test_pairing line 20