OAI/MathematicalPhysics/NavierStokes/BalancedTransport/Work.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BalancedTransport.Geometry.pd line 11
  2. theorem OAI.BalancedTransport.Geometry.pd_const line 14
  3. theorem OAI.BalancedTransport.Geometry.pd_coord line 17
  4. theorem OAI.BalancedTransport.Geometry.pd_sub_const line 22
  5. theorem OAI.BalancedTransport.Geometry.pd_add line 26
  6. theorem OAI.BalancedTransport.Geometry.pd_sub line 31
  7. theorem OAI.BalancedTransport.Geometry.pd_mul line 36
  8. theorem OAI.BalancedTransport.Geometry.pd_apply line 42
  9. theorem OAI.BalancedTransport.Geometry.pd_contDiff line 48
  10. theorem OAI.BalancedTransport.Geometry.pd_comm line 52
  11. def OAI.BalancedTransport.Geometry.curl line 64
  12. def OAI.BalancedTransport.Geometry.divergence line 69
  13. theorem OAI.BalancedTransport.Geometry.curl_contDiff line 72
  14. theorem OAI.BalancedTransport.Geometry.divergence_curl line 82
  15. theorem OAI.BalancedTransport.Geometry.curl_congr line 98
  16. theorem OAI.BalancedTransport.Geometry.curl_zero line 104
  17. theorem OAI.BalancedTransport.Geometry.tsupport_curl_subset line 108
  18. theorem OAI.BalancedTransport.Geometry.curl_hasCompactSupport line 117
  19. def OAI.BalancedTransport.Geometry.affinePotential line 121
  20. theorem OAI.BalancedTransport.Geometry.affinePotential_contDiff line 129
  21. theorem OAI.BalancedTransport.Geometry.curl_affinePotential line 135
  22. def OAI.BalancedTransport.Geometry.boxCutoff line 145
  23. def OAI.BalancedTransport.Geometry.openEnlargement line 149
  24. def OAI.BalancedTransport.Geometry.closedEnlargement line 152
  25. theorem OAI.BalancedTransport.Geometry.mem_openEnlargement line 155
  26. theorem OAI.BalancedTransport.Geometry.mem_closedEnlargement line 159
  27. theorem OAI.BalancedTransport.Geometry.openEnlargement_isOpen line 163
  28. theorem OAI.BalancedTransport.Geometry.closedEnlargement_isCompact line 167
  29. theorem OAI.BalancedTransport.Geometry.boxCutoff_contDiff line 170
  30. theorem OAI.BalancedTransport.Geometry.boxCutoff_eq_one line 175
  31. theorem OAI.BalancedTransport.Geometry.boxCutoff_eventually_one line 183
  32. theorem OAI.BalancedTransport.Geometry.boxCutoff_eq_zero line 192
  33. theorem OAI.BalancedTransport.Geometry.tsupport_boxCutoff_subset line 208
  34. theorem OAI.BalancedTransport.Geometry.boxCutoff_hasCompactSupport line 215
  35. def OAI.BalancedTransport.Geometry.localizedAffine line 220
  36. theorem OAI.BalancedTransport.Geometry.localizedAffine_contDiff line 223
  37. theorem OAI.BalancedTransport.Geometry.localizedAffine_divergence line 227
  38. theorem OAI.BalancedTransport.Geometry.localizedAffine_eq line 231
  39. theorem OAI.BalancedTransport.Geometry.tsupport_localizedAffine_subset line 239
  40. theorem OAI.BalancedTransport.Geometry.localizedAffine_hasCompactSupport line 247