OAI/Analysis/LienardCycles/FitProperness.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.QuadraticFit.seqA line 21
  2. def OAI.QuinticLienard.QuadraticFit.seqE line 22
  3. def OAI.QuinticLienard.QuadraticFit.seqJ line 23
  4. def OAI.QuinticLienard.QuadraticFit.seqL line 24
  5. def OAI.QuinticLienard.QuadraticFit.seqθ line 25
  6. def OAI.QuinticLienard.QuadraticFit.seqg line 26
  7. lemma OAI.QuinticLienard.QuadraticFit.seqA_abs line 28
  8. lemma OAI.QuinticLienard.QuadraticFit.seqA_mono line 29
  9. lemma OAI.QuinticLienard.QuadraticFit.seqE_mono line 33
  10. lemma OAI.QuinticLienard.QuadraticFit.seqθ_lower line 37
  11. lemma OAI.QuinticLienard.QuadraticFit.seqE_continuousOn line 41
  12. lemma OAI.QuinticLienard.QuadraticFit.seqJ_continuousOn line 42
  13. lemma OAI.QuinticLienard.QuadraticFit.seqA_continuousOn line 43
  14. lemma OAI.QuinticLienard.QuadraticFit.seqg_continuousOn line 46
  15. lemma OAI.QuinticLienard.QuadraticFit.seqg_pos line 48
  16. lemma OAI.QuinticLienard.QuadraticFit.seqE_integrable line 50
  17. lemma OAI.QuinticLienard.QuadraticFit.seqJ_integrable line 53
  18. lemma OAI.QuinticLienard.QuadraticFit.seqE_integral_bounds line 56
  19. lemma OAI.QuinticLienard.QuadraticFit.seqθ_ae_bdd line 67
  20. lemma OAI.QuinticLienard.QuadraticFit.seqg_uniform_integral_pos line 92
  21. lemma OAI.QuinticLienard.QuadraticFit.seqJ_drop line 131
  22. theorem OAI.QuinticLienard.QuadraticFit.seqL_not_bddAbove line 144