OAI/Geometry/RCD/Coordinates/RegularizedHamiltonIntegrability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability for regularized Hamilton tests

  1. theorem OAI.RegularPointCoordinates.shifted_log_gap_integrableOn line 14
  2. theorem OAI.RegularPointCoordinates.regularized_gamma_integrable line 34