OAI/MathematicalPhysics/AlternatingFlow/SpatialCurls.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Spatial.d line 10
  2. lemma OAI.AlternatingNS.Spatial.coord_smooth line 13
  3. lemma OAI.AlternatingNS.Spatial.coord_hasFDeriv line 16
  4. lemma OAI.AlternatingNS.Spatial.e_apply line 20
  5. lemma OAI.AlternatingNS.Spatial.d_smooth line 23
  6. lemma OAI.AlternatingNS.Spatial.d_tsupport line 27
  7. lemma OAI.AlternatingNS.Spatial.d_comm line 31
  8. def OAI.AlternatingNS.Spatial.curl line 42
  9. lemma OAI.AlternatingNS.Spatial.curl_smooth line 45
  10. lemma OAI.AlternatingNS.Spatial.curl_tsupport line 49
  11. lemma OAI.AlternatingNS.Spatial.curl_div line 55
  12. def OAI.AlternatingNS.Spatial.box line 70
  13. def OAI.AlternatingNS.Spatial.plateau line 72
  14. def OAI.AlternatingNS.Spatial.cutoff line 74
  15. lemma OAI.AlternatingNS.Spatial.cutoff_smooth line 78
  16. lemma OAI.AlternatingNS.Spatial.isClosed_box line 85
  17. lemma OAI.AlternatingNS.Spatial.box_compact line 90
  18. lemma OAI.AlternatingNS.Spatial.plateau_open line 103
  19. lemma OAI.AlternatingNS.Spatial.cutoff_one line 108
  20. lemma OAI.AlternatingNS.Spatial.cutoff_one_near line 115
  21. lemma OAI.AlternatingNS.Spatial.cutoff_support line 119
  22. def OAI.AlternatingNS.Spatial.shearPotential line 130
  23. def OAI.AlternatingNS.Spatial.localizedShear line 133
  24. lemma OAI.AlternatingNS.Spatial.shearPotential_smooth line 136
  25. lemma OAI.AlternatingNS.Spatial.localizedShear_smooth line 142
  26. lemma OAI.AlternatingNS.Spatial.localizedShear_support line 147
  27. lemma OAI.AlternatingNS.Spatial.localizedShear_div line 151
  28. lemma OAI.AlternatingNS.Spatial.localizedShear_plateau line 156