OAI/MathematicalPhysics/NavierStokes/Material/Curls.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Alternating.spatialD_smooth line 11
  2. theorem OAI.Alternating.spatialD_twice line 16
  3. theorem OAI.Alternating.spatialD_comm line 25
  4. def OAI.Alternating.pairedCurl line 33
  5. theorem OAI.Alternating.pairedCurl_smooth line 36
  6. theorem OAI.Alternating.divergence_sub line 41
  7. theorem OAI.Alternating.divergence_basis_smul line 47
  8. theorem OAI.Alternating.pairedCurl_divergence line 55
  9. def OAI.Alternating.spatialCutoff line 65
  10. theorem OAI.Alternating.spatialCutoff_smooth line 68
  11. theorem OAI.Alternating.spatialCutoff_one line 72
  12. theorem OAI.Alternating.spatialCutoff_zero line 77
  13. theorem OAI.Alternating.spatialCutoff_support line 82
  14. theorem OAI.Alternating.spatialCutoff_compact line 89
  15. theorem OAI.Alternating.spatialCutoff_one_near line 92
  16. theorem OAI.Alternating.tsupport_spatialD_subset line 97
  17. theorem OAI.Alternating.tsupport_pairedCurl_subset line 102
  18. def OAI.Alternating.localizedCurl line 109
  19. theorem OAI.Alternating.localizedCurl_smooth line 112
  20. theorem OAI.Alternating.localizedCurl_divergence line 116
  21. theorem OAI.Alternating.localizedCurl_support line 120
  22. theorem OAI.Alternating.localizedCurl_compact line 124
  23. theorem OAI.Alternating.localizedCurl_on_plateau line 129
  24. theorem OAI.Alternating.spatialD_sub line 136
  25. theorem OAI.Alternating.spatialD_mul line 141
  26. theorem OAI.Alternating.spatialD_coord line 147
  27. theorem OAI.Alternating.spatialD_other_coord line 153
  28. def OAI.Alternating.evenPotential line 161
  29. def OAI.Alternating.oddPotential line 164
  30. theorem OAI.Alternating.evenPotential_smooth line 167
  31. theorem OAI.Alternating.oddPotential_smooth line 173
  32. theorem OAI.Alternating.evenPotential_curl line 179
  33. theorem OAI.Alternating.oddPotential_curl line 202
  34. def OAI.Alternating.slotVelocity line 225
  35. theorem OAI.Alternating.slotVelocity_smooth line 231
  36. theorem OAI.Alternating.slotVelocity_divergence line 240
  37. theorem OAI.Alternating.slotVelocity_support line 249
  38. theorem OAI.Alternating.slotVelocity_compact line 254
  39. theorem OAI.Alternating.slotVelocity_on_plateau line 259
  40. theorem OAI.Alternating.slotVelocity_donor_stationary line 271