OAI/MathematicalPhysics/SheetFlows/BoxJets.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows box jets.

  1. def OAI.Solenoidal.coordinateLinear line 14
  2. theorem OAI.Solenoidal.coordinateLinear_eq line 20
  3. theorem OAI.Solenoidal.coordinateLinear_basis line 24
  4. inductive OAI.Solenoidal.BoxExpr line 28
  5. def OAI.Solenoidal.BoxExpr.eval line 36
  6. theorem OAI.Solenoidal.BoxExpr.smooth line 42
  7. def OAI.Solenoidal.BoxExpr.diff line 49
  8. theorem OAI.Solenoidal.BoxExpr.diff_correct line 55
  9. def OAI.Solenoidal.BoxExpr.mixed line 79
  10. def OAI.Solenoidal.BoxExpr.bound line 83
  11. theorem OAI.Solenoidal.BoxExpr.bound_nonneg line 89
  12. theorem OAI.Solenoidal.BoxExpr.bound_correct line 96
  13. def OAI.Solenoidal.expressionField line 109
  14. theorem OAI.Solenoidal.expressionField_smooth line 111
  15. theorem OAI.Solenoidal.mixedDerivative_expressionField line 114
  16. def OAI.Solenoidal.expressionBound line 125
  17. theorem OAI.Solenoidal.expressionBound_nonneg line 128
  18. theorem OAI.Solenoidal.expressionBound_correct line 132
  19. def OAI.Solenoidal.closedPeriodCell line 142
  20. theorem OAI.Solenoidal.mixedDerivative_eqOn_open line 144
  21. theorem OAI.Solenoidal.mixedDerivative_eqOn_cell line 155
  22. theorem OAI.Solenoidal.periodic_expression_mixed_bound line 174