OAI/MathematicalPhysics/NavierStokes/ShearFlows/PeriodicCalculus.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShearFlows.dot line 13
  2. theorem OAI.ShearFlows.dot_comm line 15
  3. theorem OAI.ShearFlows.dot_zero_right line 18
  4. theorem OAI.ShearFlows.dot_zero_left line 19
  5. theorem OAI.ShearFlows.dot_add_right line 20
  6. theorem OAI.ShearFlows.dot_sub_right line 22
  7. theorem OAI.ShearFlows.dot_neg_right line 24
  8. theorem OAI.ShearFlows.dot_smul_right line 25
  9. theorem OAI.ShearFlows.dot_contDiff line 28
  10. theorem OAI.ShearFlows.dot_continuous line 33
  11. theorem OAI.ShearFlows.dot_self_nonneg line 38
  12. theorem OAI.ShearFlows.fderiv_dot line 41
  13. theorem OAI.ShearFlows.fderiv_dot_self line 53
  14. theorem OAI.ShearFlows.divergence_scalar_mul line 58
  15. theorem OAI.ShearFlows.integral_periodic_divergence line 65
  16. theorem OAI.ShearFlows.integral_pressure_transport_zero line 91
  17. theorem OAI.ShearFlows.integral_transport_zero line 104
  18. theorem OAI.ShearFlows.dot_sum_right line 120
  19. theorem OAI.ShearFlows.CubePeriodic.fderiv line 125
  20. theorem OAI.ShearFlows.CubePeriodic.derivative line 131
  21. theorem OAI.ShearFlows.derivative_contDiff line 137
  22. theorem OAI.ShearFlows.divergence_dot_derivative line 141
  23. theorem OAI.ShearFlows.integral_dot_laplacian_nonpos line 163