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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Coordinate change from the Euclidean rapid-field convention to the coordinate convention used for periodic fluid fields and cube integrals.

  1. def OAI.RapidForcing.CompactEmbedding.piCoordinates line 15
  2. theorem OAI.RapidForcing.CompactEmbedding.piCoordinates_apply line 18
  3. theorem OAI.RapidForcing.CompactEmbedding.piCoordinates_symm_apply line 21
  4. theorem OAI.RapidForcing.CompactEmbedding.piCoordinates_basis line 24
  5. theorem OAI.RapidForcing.CompactEmbedding.piCoordinates_symm_basis line 29
  6. theorem OAI.RapidForcing.CompactEmbedding.piCoordinates_symm_lattice line 34
  7. def OAI.RapidForcing.CompactEmbedding.piField line 39
  8. theorem OAI.RapidForcing.CompactEmbedding.piField_smooth line 42
  9. theorem OAI.RapidForcing.CompactEmbedding.piField_derivative line 47
  10. theorem OAI.RapidForcing.CompactEmbedding.piField_divergence line 57
  11. theorem OAI.RapidForcing.CompactEmbedding.piField_advection line 62
  12. theorem OAI.RapidForcing.CompactEmbedding.piField_laplacian line 77
  13. theorem OAI.RapidForcing.CompactEmbedding.piField_timeDerivative line 87
  14. theorem OAI.RapidForcing.CompactEmbedding.piField_periodic line 98
  15. theorem OAI.RapidForcing.CompactEmbedding.piField_periodic_extension line 105