OAI/MathematicalPhysics/SheetFlows/EnergyIdentities.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Solenoidal.measurableSet_fundamentalCell line 15
2. theorem OAI.Solenoidal.fundamentalCell_subset_cube line 18
3. theorem OAI.Solenoidal.cylinder_uniform_bound line 22
4. theorem OAI.Solenoidal.cylinder_integral_continuousOn line 31
5. theorem OAI.Solenoidal.cylinder_integral_hasDerivAt line 47
6. theorem OAI.Solenoidal.hasDerivAt_kineticDensity line 71
7. def OAI.Solenoidal.euclidDot line 87
8. theorem OAI.Solenoidal.continuous_euclidDot line 89
9. theorem OAI.Solenoidal.euclidDot_add line 95
10. theorem OAI.Solenoidal.euclidDot_sub line 99
11. theorem OAI.Solenoidal.euclidDot_neg line 103
12. theorem OAI.Solenoidal.euclidDot_smul line 106
13. theorem OAI.Solenoidal.TorusC1.fderiv_along_continuous line 110
14. theorem OAI.Solenoidal.periodic_pressure_energy_zero line 120
15. theorem OAI.Solenoidal.periodic_viscous_energy_nonpos line 130
16. theorem OAI.Solenoidal.stretching_energy_bound line 158
17. theorem OAI.Solenoidal.spatialPartial_sub_at line 185
18. theorem OAI.Solenoidal.laplacian_sub_at line 193
19. theorem OAI.Solenoidal.advection_sub_identity line 204
20. theorem OAI.Solenoidal.gradient_sub_at line 212
21. theorem OAI.Solenoidal.ClassicalSolution.difference_equation line 220
22. theorem OAI.Solenoidal.ClassicalSolution.hasDerivAt line 236
23. def OAI.Solenoidal.relativeEnergy line 241
24. theorem OAI.Solenoidal.relativeEnergy_nonneg line 244
25. theorem OAI.Solenoidal.ClassicalSolution.relativeEnergy_zero line 247
26. theorem OAI.Solenoidal.continuousOn_euclidDot line 252
27. theorem OAI.Solenoidal.ClassicalSolution.relativeEnergy_continuousOn line 259
28. theorem OAI.Solenoidal.ClassicalSolution.relativeEnergy_hasDerivAt line 265
29. theorem OAI.Solenoidal.ClassicalSolution.gradient_cylinder_bound line 282
30. theorem OAI.Solenoidal.ClassicalSolution.relativeEnergy_derivative_bound line 294