OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/CompactPeriodizationNS.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Local periodization preserves the full residual equation. A pressure projection, when supplied by the torus Poisson solver, is a separate algebraic step and does not change the velocity or its trajectories.

  1. theorem OAI.RapidForcing.CompactEmbedding.field_chartSupported line 15
  2. theorem OAI.RapidForcing.CompactEmbedding.periodic_divergence line 25
  3. theorem OAI.RapidForcing.CompactEmbedding.periodic_advection line 31
  4. theorem OAI.RapidForcing.CompactEmbedding.periodic_laplace line 37
  5. theorem OAI.RapidForcing.CompactEmbedding.periodic_residual line 46
  6. theorem OAI.RapidForcing.CompactEmbedding.periodic_navierStokes line 52
  7. theorem OAI.RapidForcing.CompactEmbedding.navierStokes_pressure_projection line 68