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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The similarity has length scale 1/8. Thus viscosity 64ν before the similarity gives viscosity ν afterwards. All identities are proved directly from the coordinate derivatives used in the rapid construction.

  1. theorem OAI.RapidForcing.CompactEmbedding.spatialD_field line 14
  2. theorem OAI.RapidForcing.CompactEmbedding.divergence_field line 25
  3. theorem OAI.RapidForcing.CompactEmbedding.advection_field line 36
  4. theorem OAI.RapidForcing.CompactEmbedding.spatialD_const_smul line 47
  5. theorem OAI.RapidForcing.CompactEmbedding.spatialD_field_differentiable line 54
  6. theorem OAI.RapidForcing.CompactEmbedding.spatialD_twice_field line 58
  7. theorem OAI.RapidForcing.CompactEmbedding.laplace_field line 75
  8. theorem OAI.RapidForcing.CompactEmbedding.timeD_field line 83
  9. theorem OAI.RapidForcing.CompactEmbedding.residual_field line 89
  10. theorem OAI.RapidForcing.CompactEmbedding.navierStokes_field line 102