OAI/Geometry/RCD/Sobolev/HamiltonJacobiTimeBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Time increments controlled by the local weak equation

The source term is tested only on the support of the compact test. Its bound uses the actual weak Laplacian and the local slope bound.

  1. theorem OAI.RegularPointCoordinates.local_hamilton_jacobi_source_bound line 21
  2. theorem OAI.RegularPointCoordinates.hamilton_jacobi_pairing_time_bound line 85