OAI/Analysis/LienardCycles/ConditionalFit.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuinticLienard.QuadraticFit.slope_curvature_deriv line 20
  2. def OAI.QuinticLienard.QuadraticFit.conditionalV line 40
  3. lemma OAI.QuinticLienard.QuadraticFit.conditionalV_analytic line 42
  4. lemma OAI.QuinticLienard.QuadraticFit.conditionalV_deriv line 48
  5. lemma OAI.QuinticLienard.QuadraticFit.conditionalV_strictMono line 65
  6. lemma OAI.QuinticLienard.QuadraticFit.reference_midpoint_exists line 72
  7. lemma OAI.QuinticLienard.QuadraticFit.reference_midpoint_strictMono line 82
  8. def OAI.QuinticLienard.QuadraticFit.label line 89
  9. lemma OAI.QuinticLienard.QuadraticFit.label_spec line 93
  10. lemma OAI.QuinticLienard.QuadraticFit.label_eq line 99
  11. lemma OAI.QuinticLienard.QuadraticFit.label_analytic line 103
  12. lemma OAI.QuinticLienard.QuadraticFit.label_curvature_deriv line 121
  13. lemma OAI.QuinticLienard.QuadraticFit.T_strictAnti line 140
  14. lemma OAI.QuinticLienard.QuadraticFit.conditionalA_deriv line 151
  15. lemma OAI.QuinticLienard.QuadraticFit.conditionalA_strictMono line 165