OAI/MathematicalPhysics/SheetFlows/ClassicalRegularity.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows classical regularity.

  1. structure OAI.Solenoidal.TorusC1 line 16
  2. theorem OAI.Solenoidal.TorusC1.of_smooth line 22
  3. theorem OAI.Solenoidal.TorusC1.const line 27
  4. theorem OAI.Solenoidal.TorusC1.add line 33
  5. theorem OAI.Solenoidal.TorusC1.sub line 45
  6. theorem OAI.Solenoidal.scalarPartial_mul line 57
  7. theorem OAI.Solenoidal.TorusC1.mul line 64
  8. theorem OAI.Solenoidal.TorusC1.sum line 74
  9. theorem OAI.Solenoidal.fderiv_component line 87
  10. theorem OAI.Solenoidal.TorusC1.component line 94
  11. theorem OAI.Solenoidal.periodic_integral_divergence_zero_C1 line 103
  12. theorem OAI.Solenoidal.periodic_integral_partial_zero_C1 line 125
  13. theorem OAI.Solenoidal.periodic_integration_by_parts line 140
  14. theorem OAI.Solenoidal.cylinder_spatial_slice line 152
  15. theorem OAI.Solenoidal.spatialPartial_periodic_of_differentiable line 159
  16. theorem OAI.Solenoidal.ClassicalSolution.spatialC1 line 164
  17. theorem OAI.Solenoidal.ClassicalSolution.spatialPartialC1 line 170
  18. theorem OAI.Solenoidal.ClassicalSolution.pressureC1 line 179
  19. theorem OAI.Solenoidal.fderiv_apply_eq_sum line 186
  20. theorem OAI.Solenoidal.periodic_transport_zero line 195
  21. def OAI.Solenoidal.kineticDensity line 214
  22. theorem OAI.Solenoidal.kineticDensity_nonneg line 216
  23. theorem OAI.Solenoidal.kineticDensity_continuous line 220
  24. theorem OAI.Solenoidal.fderiv_kineticDensity line 225
  25. theorem OAI.Solenoidal.TorusC1.kineticDensity line 242
  26. theorem OAI.Solenoidal.periodic_transport_energy_zero line 249