OAI/MathematicalPhysics/SheetFlows/Clocks.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows clocks.

  1. def OAI.Solenoidal.pulseClock line 17
  2. def OAI.Solenoidal.localPulse line 19
  3. def OAI.Solenoidal.periodicPulse line 21
  4. theorem OAI.Solenoidal.pulseClock_contDiff line 23
  5. theorem OAI.Solenoidal.pulseClock_zero line 28
  6. theorem OAI.Solenoidal.pulseClock_one line 33
  7. theorem OAI.Solenoidal.pulseClock_monotone line 38
  8. theorem OAI.Solenoidal.localPulse_contDiff line 44
  9. theorem OAI.Solenoidal.localPulse_nonneg line 48
  10. theorem OAI.Solenoidal.localPulse_zero_left line 51
  11. theorem OAI.Solenoidal.localPulse_zero_right line 62
  12. theorem OAI.Solenoidal.periodicPulse_periodic line 73
  13. theorem OAI.Solenoidal.periodicPulse_contDiff line 76
  14. theorem OAI.Solenoidal.periodicPulse_nonneg line 85
  15. theorem OAI.Solenoidal.periodicPulse_on_chart line 89
  16. theorem OAI.Solenoidal.periodicPulse_on_fraction line 98
  17. theorem OAI.Solenoidal.periodicPulse_integral_one line 107
  18. def OAI.Solenoidal.slotLeft line 122
  19. def OAI.Solenoidal.slotRight line 124
  20. def OAI.Solenoidal.scheduledPulse line 126
  21. theorem OAI.Solenoidal.slot_bounds line 129
  22. theorem OAI.Solenoidal.slot_ordered line 143
  23. theorem OAI.Solenoidal.scheduledPulse_contDiff line 151
  24. theorem OAI.Solenoidal.scheduledPulse_periodic line 155
  25. theorem OAI.Solenoidal.scheduledPulse_nonneg line 158
  26. theorem OAI.Solenoidal.scheduledPulse_integral_one line 161
  27. theorem OAI.Solenoidal.scheduledPulse_active line 166
  28. theorem OAI.Solenoidal.scheduledPulse_disjoint line 176
  29. theorem OAI.Solenoidal.scheduledPulse_integer_collar line 186
  30. def OAI.Solenoidal.tensorScalar line 205
  31. def OAI.Solenoidal.tensorVelocity line 207
  32. theorem OAI.Solenoidal.tensorScalar_contDiff line 210
  33. theorem OAI.Solenoidal.tensorVelocity_smooth line 215
  34. theorem OAI.Solenoidal.tensorVelocity_spatially_periodic line 219
  35. theorem OAI.Solenoidal.tensorScalar_integral line 228
  36. theorem OAI.Solenoidal.tensorVelocity_mean_zero line 236
  37. theorem OAI.Solenoidal.tensorScalar_eraseAxis line 246
  38. theorem OAI.Solenoidal.tensorVelocity_eq_axial line 256
  39. theorem OAI.Solenoidal.tensorVelocity_divergence_free line 263
  40. theorem OAI.Solenoidal.tensorVelocity_advection_zero line 270