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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A compact vertical cutoff of a planar incompressible processor. Its horizontal trajectories at a cutoff plateau remain exact, and the cutoff introduces no divergence because the lifted field has zero third component.

  1. def OAI.ForcedComputation.CompactLift.spatial line 15
  2. def OAI.ForcedComputation.CompactLift.velocity line 18
  3. theorem OAI.ForcedComputation.CompactLift.spatial_smooth line 21
  4. theorem OAI.ForcedComputation.CompactLift.velocity_smooth line 27
  5. theorem OAI.ForcedComputation.CompactLift.spatial_third line 40
  6. theorem OAI.ForcedComputation.CompactLift.spatial_atHeight line 44
  7. theorem OAI.ForcedComputation.CompactLift.height_fderiv line 51
  8. theorem OAI.ForcedComputation.CompactLift.spatial_divergence line 59
  9. theorem OAI.ForcedComputation.CompactLift.atHeight_hasDerivAt line 84
  10. theorem OAI.ForcedComputation.CompactLift.trajectory_atHeight line 93