OAI/Geometry/PolarProducts/HamiltonianGrowth.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HamiltonianGrowth.contDiff_gradient line 16
  2. theorem OAI.HamiltonianGrowth.gradient_translate line 21
  3. theorem OAI.HamiltonianGrowth.energy_upper line 29
  4. theorem OAI.HamiltonianGrowth.energy_sub_uniform line 34
  5. theorem OAI.HamiltonianGrowth.quadratic_error line 38
  6. theorem OAI.HamiltonianGrowth.quartic_bound line 59
  7. theorem OAI.HamiltonianGrowth.lower_bound line 84
  8. theorem OAI.HamiltonianGrowth.bounded_remainder_translate line 93
  9. theorem OAI.HamiltonianGrowth.bound_remainder_of_compact line 106
  10. def OAI.HamiltonianPeriodic.actionIntegral line 130
  11. theorem OAI.HamiltonianPeriodic.integral_gradient_pairing line 133
  12. theorem OAI.HamiltonianPeriodic.action_translate line 147
  13. theorem OAI.HamiltonianPeriodic.exists_positive_flat line 180
  14. theorem OAI.HamiltonianPeriodic.exists_positive_at_flat_point line 206