OAI/Analysis/LienardCycles/ActualFitTransport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuinticLienard.QuinticFit.M line 21
  2. def OAI.QuinticLienard.QuinticFit.V line 22
  3. lemma OAI.QuinticLienard.QuinticFit.M_analytic line 23
  4. lemma OAI.QuinticLienard.QuinticFit.V_analytic line 25
  5. lemma OAI.QuinticLienard.QuinticFit.M_abs_lt line 27
  6. lemma OAI.QuinticLienard.QuinticFit.V_abs_lt line 29
  7. lemma OAI.QuinticLienard.QuinticFit.n_eq_V line 31
  8. lemma OAI.QuinticLienard.QuinticFit.fit_eq line 35
  9. lemma OAI.QuinticLienard.QuinticFit.lambda_analytic line 40
  10. lemma OAI.QuinticLienard.QuinticFit.kappa_analytic line 47
  11. def OAI.QuinticLienard.QuinticFit.fit line 54
  12. lemma OAI.QuinticLienard.QuinticFit.spec line 55
  13. lemma OAI.QuinticLienard.QuinticFit.model_pull_derivatives line 60
  14. lemma OAI.QuinticLienard.QuinticFit.chain_M line 79
  15. lemma OAI.QuinticLienard.QuinticFit.Hr_d_direction line 88
  16. lemma OAI.QuinticLienard.QuinticFit.Hr_k_direction line 90
  17. lemma OAI.QuinticLienard.QuinticFit.chain_V line 92
  18. def OAI.QuinticLienard.QuinticFit.α line 103
  19. def OAI.QuinticLienard.QuinticFit.D line 104
  20. lemma OAI.QuinticLienard.QuinticFit.fit_transport line 105