OAI/MathematicalPhysics/SheetFlows/JetProfiles.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows jet profiles.

  1. def OAI.Solenoidal.JetExpr.transition line 15
  2. theorem OAI.Solenoidal.JetExpr.transition_eval line 17
  3. def OAI.Solenoidal.JetExpr.cutoff line 20
  4. def OAI.Solenoidal.JetExpr.linearCutoff line 24
  5. theorem OAI.Solenoidal.JetExpr.cutoff_eval line 26
  6. theorem OAI.Solenoidal.JetExpr.linearCutoff_eval line 32
  7. def OAI.Solenoidal.JetExpr.shiftedC line 36
  8. def OAI.Solenoidal.JetExpr.shiftedD line 37
  9. def OAI.Solenoidal.JetExpr.clock line 39
  10. def OAI.Solenoidal.JetExpr.clockPulse line 41
  11. theorem OAI.Solenoidal.JetExpr.shiftedC_eval line 43
  12. theorem OAI.Solenoidal.JetExpr.shiftedD_eval line 47
  13. theorem OAI.Solenoidal.JetExpr.clock_eval line 51
  14. theorem OAI.Solenoidal.JetExpr.clockPulse_eval line 58
  15. theorem OAI.Solenoidal.iteratedDeriv_eqOn_Icc line 67
  16. theorem OAI.Solenoidal.iteratedDeriv_periodic line 84
  17. structure OAI.Solenoidal.PeriodicJet line 99
  18. def OAI.Solenoidal.PeriodicJet.bound line 110
  19. theorem OAI.Solenoidal.PeriodicJet.bound_nonneg line 112
  20. theorem OAI.Solenoidal.PeriodicJet.derivative_on_chart line 115
  21. theorem OAI.Solenoidal.PeriodicJet.bound_correct line 121
  22. def OAI.Solenoidal.PeriodicJet.ofPeriodize line 139
  23. def OAI.Solenoidal.PeriodicJet.const line 150
  24. def OAI.Solenoidal.PeriodicJet.add line 157
  25. def OAI.Solenoidal.PeriodicJet.mul line 165
  26. def OAI.Solenoidal.Cprofile_jet line 175
  27. def OAI.Solenoidal.Dprofile_jet line 189
  28. def OAI.Solenoidal.periodicPulse_jet line 203