OAI/Analysis/LienardCycles/PositiveWidth.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuinticLienard.PositiveWidth.width_small_base line 22
  2. def OAI.QuinticLienard.PositiveWidth.widthFamily line 71
  3. def OAI.QuinticLienard.PositiveWidth.midpointFamily line 73
  4. theorem OAI.QuinticLienard.PositiveWidth.width_analytic line 78
  5. theorem OAI.QuinticLienard.PositiveWidth.midpoint_analytic line 83
  6. theorem OAI.QuinticLienard.PositiveWidth.width_pos line 90
  7. theorem OAI.QuinticLienard.PositiveWidth.gap_pos line 100
  8. theorem OAI.QuinticLienard.PositiveWidth.width_base_deriv line 110
  9. theorem OAI.QuinticLienard.PositiveWidth.height_energy_antitone line 135
  10. theorem OAI.QuinticLienard.PositiveWidth.height_bound line 159
  11. theorem OAI.QuinticLienard.PositiveWidth.width_strictAnti_base line 172
  12. theorem OAI.QuinticLienard.PositiveWidth.width_strictMono_peak line 182
  13. theorem OAI.QuinticLienard.PositiveWidth.small_peak_exists line 191
  14. theorem OAI.QuinticLienard.PositiveWidth.peak_exists line 214
  15. def OAI.QuinticLienard.PositiveWidth.peakAtWidth line 235
  16. theorem OAI.QuinticLienard.PositiveWidth.peak_spec line 238
  17. theorem OAI.QuinticLienard.PositiveWidth.peak_eq line 243
  18. theorem OAI.QuinticLienard.PositiveWidth.peak_analytic line 248
  19. def OAI.QuinticLienard.PositiveWidth.midpointAtWidth line 271
  20. theorem OAI.QuinticLienard.PositiveWidth.midpointAtWidth_analytic line 274
  21. theorem OAI.QuinticLienard.PositiveWidth.midpointAtWidth_abs_lt line 280