OAI/MathematicalPhysics/SheetFlows/ScheduledForce.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows scheduled force.

  1. theorem OAI.Solenoidal.mixedDerivative_contDiff line 16
  2. theorem OAI.Solenoidal.mixedDerivative_translation line 22
  3. theorem OAI.Solenoidal.mixedDerivative_spatially_periodic line 32
  4. theorem OAI.Solenoidal.mixedDerivative_onePeriodic line 40
  5. def OAI.Solenoidal.wrapSpace line 48
  6. theorem OAI.Solenoidal.wrapSpace_mem line 50
  7. theorem OAI.Solenoidal.wrapSpace_add_deck line 57
  8. theorem OAI.Solenoidal.periodic_field_reduction line 63
  9. theorem OAI.Solenoidal.periodic_continuous_bounded line 76
  10. theorem OAI.Solenoidal.periodic_smooth_mixed_bounded line 88
  11. theorem OAI.Solenoidal.fieldDirectional_commute line 98
  12. theorem OAI.Solenoidal.directional_component line 105
  13. theorem OAI.Solenoidal.divergence_fieldDirectional line 112
  14. theorem OAI.Solenoidal.fieldDirectional_divergence_free line 132
  15. theorem OAI.Solenoidal.spatialPartial_divergence_free line 141
  16. theorem OAI.Solenoidal.fullTimePartial_divergence_free line 146
  17. theorem OAI.Solenoidal.divergence_sub line 151
  18. theorem OAI.Solenoidal.divergence_smul line 159
  19. theorem OAI.Solenoidal.divergence_sum line 166
  20. theorem OAI.Solenoidal.laplacian_divergence_free line 175
  21. theorem OAI.Solenoidal.globalDirectForce_divergence_free line 187
  22. theorem OAI.Solenoidal.cell_ae_eq_Icc line 198
  23. theorem OAI.Solenoidal.face_front_eq_back_deck line 201
  24. theorem OAI.Solenoidal.periodic_integral_divergence_zero line 208
  25. theorem OAI.Solenoidal.periodic_integral_partial_zero line 233
  26. theorem OAI.Solenoidal.spatialPartial_mean_zero line 250
  27. theorem OAI.Solenoidal.meanZero_sum line 255
  28. theorem OAI.Solenoidal.laplacian_mean_zero line 263
  29. theorem OAI.Solenoidal.scheduleVelocity_fullTimePartial line 273
  30. theorem OAI.Solenoidal.scheduleVelocity_fullTimePartial_mean_zero line 280
  31. theorem OAI.Solenoidal.globalDirectForce_mean_zero line 290
  32. theorem OAI.Solenoidal.scheduled_direct_forcing line 301