OAI/Geometry/RCD/Sobolev/HamiltonJacobiWeakEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact integrated gradient energy of the viscous potentials

The local Sobolev representatives need no assumed time regularity. Their weighted energy is identified with continuous value/source pairings.

  1. theorem OAI.RegularPointCoordinates.compact_set_pairing_continuous line 20
  2. theorem OAI.RegularPointCoordinates.hamilton_jacobi_weak_energy line 36