OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/TorusDetectorMain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The compact-chart velocity detector on the unit three-torus. All analytic existence inputs are explicit. The force is given by finite expressions and terminating rational arithmetic, before solving the fluid.

  1. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_vertical line 16
  2. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_fixed_observation line 21
  3. theorem OAI.ForcedComputation.VelocityDetector.torus_velocity_detection line 36