OAI/Analysis/LienardCycles/AxisSecants.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.AxisFlow.Vm line 21
  2. def OAI.QuinticLienard.AxisFlow.Vk line 22
  3. lemma OAI.QuinticLienard.AxisFlow.Vm_deriv line 23
  4. lemma OAI.QuinticLienard.AxisFlow.Vk_deriv line 28
  5. lemma OAI.QuinticLienard.AxisFlow.Vk_pos line 33
  6. lemma OAI.QuinticLienard.AxisFlow.abs_segment_lt line 36
  7. def OAI.QuinticLienard.AxisFlow.mSegment line 45
  8. def OAI.QuinticLienard.AxisFlow.kSegment line 47
  9. def OAI.QuinticLienard.AxisFlow.secantA line 49
  10. def OAI.QuinticLienard.AxisFlow.secantB line 50
  11. lemma OAI.QuinticLienard.AxisFlow.mSegment_continuousAt line 51
  12. lemma OAI.QuinticLienard.AxisFlow.kSegment_continuousAt line 58
  13. lemma OAI.QuinticLienard.AxisFlow.secant_integrands_continuous line 65
  14. lemma OAI.QuinticLienard.AxisFlow.secantA_continuousOn line 80
  15. lemma OAI.QuinticLienard.AxisFlow.secantB_pos line 83
  16. lemma OAI.QuinticLienard.AxisFlow.secant_identity line 90