OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PeriodicLatticeFluid.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Navier--Stokes transport for the transverse lattice transformation. The vanishing first derivative makes the nonisometric scaling harmless.

  1. theorem OAI.PeriodicLattice.RapidTorus.transformedField_laplacian line 14
  2. theorem OAI.PeriodicLattice.RapidTorus.transformedField_timeD line 22
  3. theorem OAI.PeriodicLattice.RapidTorus.transformedField_advection line 29
  4. theorem OAI.PeriodicLattice.RapidTorus.transformedField_divergence line 39
  5. theorem OAI.PeriodicLattice.RapidTorus.shiftedField_gradient line 54
  6. theorem OAI.PeriodicLattice.RapidTorus.transformed_classical_equations line 69
  7. theorem OAI.PeriodicLattice.RapidTorus.velocity_firstDerivative line 89
  8. theorem OAI.PeriodicLattice.RapidTorus.potential_firstDerivative line 102
  9. theorem OAI.PeriodicLattice.RapidTorus.shiftedField_meanZero line 115
  10. theorem OAI.PeriodicLattice.RapidTorus.algebra_firstDerivative line 121
  11. theorem OAI.PeriodicLattice.RapidTorus.vectorAlgebra_firstDerivative line 138
  12. theorem OAI.PeriodicLattice.RapidTorus.transformed_solenoidalForce line 146
  13. theorem OAI.PeriodicLattice.RapidTorus.transformed_classical_solution line 154