OAI/MathematicalPhysics/NavierStokes/BalancedTransport/TimeRegularity.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BalancedTransport.Geometry.JointSmooth line 11
  2. theorem OAI.BalancedTransport.Geometry.JointSmooth.slice line 14
  3. theorem OAI.BalancedTransport.Geometry.JointSmooth.spaceD line 17
  4. theorem OAI.BalancedTransport.Geometry.JointSmooth.curl line 24
  5. theorem OAI.BalancedTransport.Geometry.divergence_eq_div line 35
  6. theorem OAI.BalancedTransport.Geometry.JointSmooth.solenoidal_curl line 41
  7. def OAI.BalancedTransport.Geometry.fullTimeD line 46
  8. theorem OAI.BalancedTransport.Geometry.JointSmooth.fullTimeD line 48
  9. def OAI.BalancedTransport.Geometry.lowerEndpoint line 56
  10. def OAI.BalancedTransport.Geometry.logarithmicRate line 59
  11. def OAI.BalancedTransport.Geometry.movingBoxVelocity line 62
  12. lemma OAI.BalancedTransport.Geometry.logarithmicRate_trace_zero line 66
  13. lemma OAI.BalancedTransport.Geometry.logarithmicRate_contDiff line 82
  14. theorem OAI.BalancedTransport.Geometry.movingBoxVelocity_jointSmooth line 89
  15. theorem OAI.BalancedTransport.Geometry.movingBoxVelocity_divergence line 109
  16. def OAI.BalancedTransport.Geometry.affinePath line 116
  17. lemma OAI.BalancedTransport.Geometry.affinePath_mem_plateau line 119
  18. theorem OAI.BalancedTransport.Geometry.affinePath_hasDerivAt_of_mem_plateau line 131
  19. theorem OAI.BalancedTransport.Geometry.affinePath_hasDerivAt line 154
  20. lemma OAI.BalancedTransport.Geometry.affinePath_mem_plateau_of_scaled_bound line 163
  21. theorem OAI.BalancedTransport.Geometry.affinePath_neighborhood line 175
  22. lemma OAI.BalancedTransport.Geometry.affinePotential_zero line 185
  23. lemma OAI.BalancedTransport.Geometry.localizedAffine_zero line 189
  24. theorem OAI.BalancedTransport.Geometry.movingBoxVelocity_zero line 198
  25. lemma OAI.BalancedTransport.Geometry.tsupport_movingBoxVelocity_subset line 204