OAI/Geometry/PolarProducts/PeriodicSolutions.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FourierPolynomial.critical_H1_bounds line 15
  2. theorem OAI.FourierPolynomial.critical_modulus line 35
  3. theorem OAI.FourierPolynomial.critical_loop_bound line 50
  4. theorem OAI.FourierPolynomial.critical_subsequence line 63
  5. def OAI.FourierPolynomial.coordPath line 76
  6. theorem OAI.FourierPolynomial.coordPath_apply line 79
  7. def OAI.FourierPolynomial.gradPath line 81
  8. theorem OAI.FourierPolynomial.contDiff_gradPath line 84
  9. theorem OAI.FourierPolynomial.critical_coefficient line 87
  10. theorem OAI.FourierPolynomial.limit_coefficient line 100
  11. theorem OAI.FourierPolynomial.hasDerivAt_of_critical_coefficients line 119
  12. theorem OAI.FourierPolynomial.positive_action_limit line 136
  13. def OAI.HamiltonianPeriodic.negativeMode line 159
  14. def OAI.HamiltonianPeriodic.positiveMode line 160
  15. def OAI.HamiltonianPeriodic.frequency line 161
  16. theorem OAI.HamiltonianPeriodic.negativeMode_nonpos line 164
  17. theorem OAI.HamiltonianPeriodic.positiveMode_pos line 167
  18. theorem OAI.HamiltonianPeriodic.positiveMode_injective line 169
  19. theorem OAI.HamiltonianPeriodic.frequency_injective line 174
  20. theorem OAI.HamiltonianPeriodic.frequency_exhausts line 186
  21. theorem OAI.HamiltonianPeriodic.exists_positive_periodic line 202