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

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Spatial calculus for the triangular velocity U(Y,z) = (a(Y), w(Y)). This is the scalar-to-Navier–Stokes reduction used by both detectors.

  1. def OAI.ForcedComputation.VelocityDetector.triangularLift line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.horizontalLinear_eq line 18
  3. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_eq line 22
  4. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_smooth line 29
  5. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_fderiv line 35
  6. theorem OAI.ForcedComputation.VelocityDetector.horizontalLinear_basis line 50
  7. theorem OAI.ForcedComputation.VelocityDetector.horizontalLinear_basis_two line 56
  8. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_derivative line 60
  9. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_vertical_derivative line 69
  10. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_divergence line 76
  11. theorem OAI.ForcedComputation.VelocityDetector.horizontal_triangularLift line 91
  12. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_advection line 96
  13. def OAI.ForcedComputation.VelocityDetector.planarVectorLaplacian line 104
  14. theorem OAI.ForcedComputation.VelocityDetector.triangularLift_laplacian line 108