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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A prescribed planar drift and scalar source determine the full external force before the transported scalar is solved.

  1. def OAI.ForcedComputation.VelocityDetector.triangularVelocity line 15
  2. def OAI.ForcedComputation.VelocityDetector.planarResidual line 18
  3. def OAI.ForcedComputation.VelocityDetector.triangularForce line 22
  4. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_smooth line 25
  5. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_timeDerivative line 34
  6. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_periodic line 51
  7. theorem OAI.ForcedComputation.VelocityDetector.GlobalTorusScalarSolution.deriv_eq line 63
  8. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_residual line 75
  9. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_solution line 93