OAI/Geometry/PolarProducts/HamiltonianODE.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.HamiltonianODE.inner_I_self line 17
  2. theorem OAI.HamiltonianODE.inner_I_left line 21
  3. theorem OAI.HamiltonianODE.inner_I_I line 26
  4. theorem OAI.HamiltonianODE.zero_derivative_constant line 31
  5. theorem OAI.HamiltonianODE.energy_constant line 35
  6. theorem OAI.HamiltonianODE.quadratic_constant line 42
  7. theorem OAI.HamiltonianODE.linear_solution line 51
  8. theorem OAI.HamiltonianODE.periodic_frequency line 67
  9. theorem OAI.HamiltonianODE.slow_linear_constant line 81
  10. theorem OAI.HamiltonianODE.diag_one line 109
  11. theorem OAI.HamiltonianODE.energy_one line 113
  12. theorem OAI.HamiltonianODE.gradient_comp_energy line 116
  13. theorem OAI.HamiltonianODE.coordinate_derivative line 129
  14. theorem OAI.HamiltonianODE.slow_diagonal_constant line 138
  15. theorem OAI.HamiltonianODE.slow_radial_constant line 147
  16. theorem OAI.HamiltonianODE.moderate_linear_either line 164
  17. theorem OAI.HamiltonianODE.diagonal_either line 183