OAI/MathematicalPhysics/NavierStokes/ShearFlows/RationalEvaluation.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ShearFlows.QBall line 14
  2. def OAI.ShearFlows.QBall.Contains line 21
  3. def OAI.ShearFlows.QBall.exact line 23
  4. def OAI.ShearFlows.QBall.add line 24
  5. def OAI.ShearFlows.QBall.mul line 25
  6. def OAI.ShearFlows.QBall.pow line 27
  7. def OAI.ShearFlows.QBall.invLower line 30
  8. theorem OAI.ShearFlows.QBall.contains_exact line 33
  9. theorem OAI.ShearFlows.QBall.radius_nonneg line 35
  10. theorem OAI.ShearFlows.QBall.contains_add line 38
  11. theorem OAI.ShearFlows.QBall.contains_mul line 47
  12. theorem OAI.ShearFlows.QBall.contains_pow line 65
  13. theorem OAI.ShearFlows.QBall.contains_invLower line 71
  14. def OAI.ShearFlows.QBall.Converges line 90
  15. theorem OAI.ShearFlows.QBall.converges_exact line 94
  16. theorem OAI.ShearFlows.QBall.Converges.add line 97
  17. theorem OAI.ShearFlows.QBall.Converges.mul line 103
  18. theorem OAI.ShearFlows.QBall.Converges.pow line 109
  19. theorem OAI.ShearFlows.QBall.Converges.invLower line 115
  20. def OAI.ShearFlows.expTerms line 125
  21. def OAI.ShearFlows.expIndex line 128
  22. def OAI.ShearFlows.expBall line 130
  23. theorem OAI.ShearFlows.expTerms_cast line 133
  24. theorem OAI.ShearFlows.expBall_contains line 137
  25. theorem OAI.ShearFlows.expIndex_tendsto line 161
  26. theorem OAI.ShearFlows.expBall_converges line 164
  27. def OAI.ShearFlows.glueBall line 173
  28. theorem OAI.ShearFlows.glueBall_contains line 176
  29. theorem OAI.ShearFlows.glueBall_converges line 184
  30. def OAI.ShearFlows.ProfileExpr.enclose line 194
  31. theorem OAI.ShearFlows.ProfileExpr.enclose_contains line 203
  32. theorem OAI.ShearFlows.ProfileExpr.enclose_converges line 220