OAI/MathematicalPhysics/SheetFlows/JetCalculus.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows jet calculus.

  1. def OAI.Solenoidal.flatJet line 13
  2. def OAI.Solenoidal.flatNext line 16
  3. theorem OAI.Solenoidal.flatJet_smooth line 18
  4. theorem OAI.Solenoidal.flatJet_hasDerivAt line 21
  5. def OAI.Solenoidal.flatBound line 28
  6. theorem OAI.Solenoidal.flatBound_nonneg line 30
  7. theorem OAI.Solenoidal.pow_mul_exp_neg_le_factorial line 35
  8. theorem OAI.Solenoidal.flatJet_bound line 44
  9. def OAI.Solenoidal.transitionReciprocal line 67
  10. theorem OAI.Solenoidal.transitionReciprocal_smooth line 70
  11. theorem OAI.Solenoidal.transitionReciprocal_bound line 75
  12. theorem OAI.Solenoidal.transitionReciprocal_hasDerivAt line 96
  13. inductive OAI.Solenoidal.JetExpr line 114
  14. def OAI.Solenoidal.JetExpr.eval line 125
  15. theorem OAI.Solenoidal.JetExpr.smooth line 134
  16. def OAI.Solenoidal.JetExpr.diff line 144
  17. theorem OAI.Solenoidal.JetExpr.diff_correct line 154
  18. def OAI.Solenoidal.JetExpr.nth line 170
  19. theorem OAI.Solenoidal.JetExpr.nth_correct line 174
  20. def OAI.Solenoidal.JetExpr.bound line 181
  21. theorem OAI.Solenoidal.JetExpr.bound_nonneg line 190
  22. theorem OAI.Solenoidal.JetExpr.bound_correct line 200
  23. theorem OAI.Solenoidal.JetExpr.nth_bound line 220