OAI/Analysis/LienardCycles/WidthCoordinates.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuinticLienard.WidthCoordinates.width_small_base line 21
  2. def OAI.QuinticLienard.WidthCoordinates.widthFamily line 70
  3. def OAI.QuinticLienard.WidthCoordinates.midpointFamily line 72
  4. theorem OAI.QuinticLienard.WidthCoordinates.width_analytic line 77
  5. theorem OAI.QuinticLienard.WidthCoordinates.midpoint_analytic line 82
  6. theorem OAI.QuinticLienard.WidthCoordinates.width_pos line 89
  7. theorem OAI.QuinticLienard.WidthCoordinates.gap_pos line 98
  8. theorem OAI.QuinticLienard.WidthCoordinates.width_base_deriv line 107
  9. theorem OAI.QuinticLienard.WidthCoordinates.height_energy_antitone line 131
  10. theorem OAI.QuinticLienard.WidthCoordinates.height_bound line 156
  11. theorem OAI.QuinticLienard.WidthCoordinates.width_strictAnti_base line 169
  12. theorem OAI.QuinticLienard.WidthCoordinates.width_strictMono_peak line 178
  13. theorem OAI.QuinticLienard.WidthCoordinates.small_peak_exists line 187
  14. theorem OAI.QuinticLienard.WidthCoordinates.peak_exists line 210
  15. theorem OAI.QuinticLienard.WidthCoordinates.base_exists line 231
  16. def OAI.QuinticLienard.WidthCoordinates.peakAtWidth line 256
  17. def OAI.QuinticLienard.WidthCoordinates.baseAtWidth line 259
  18. theorem OAI.QuinticLienard.WidthCoordinates.peak_spec line 262
  19. theorem OAI.QuinticLienard.WidthCoordinates.base_spec line 267
  20. theorem OAI.QuinticLienard.WidthCoordinates.peak_eq line 272
  21. theorem OAI.QuinticLienard.WidthCoordinates.base_eq line 277
  22. theorem OAI.QuinticLienard.WidthCoordinates.peak_analytic line 282
  23. theorem OAI.QuinticLienard.WidthCoordinates.base_analytic line 303
  24. def OAI.QuinticLienard.WidthCoordinates.midpointAtWidth line 321
  25. theorem OAI.QuinticLienard.WidthCoordinates.midpointAtWidth_analytic line 324
  26. theorem OAI.QuinticLienard.WidthCoordinates.midpointAtWidth_abs_lt line 330