OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneCylinderComponents.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Component identities needed to transfer the planar L2 and strong time derivative estimates to the three-dimensional classical solution.

  1. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_horizontal_component line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.triangularVelocity_vertically_periodic line 19
  3. theorem OAI.ForcedComputation.VelocityDetector.planeTemporalDerivative_component line 26
  4. theorem OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution.initialTimeDerivative_horizontal line 37
  5. theorem OAI.ForcedComputation.VelocityDetector.GlobalPlaneScalarSolution.initialTimeDerivative_vertical line 47
  6. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.mono line 56
  7. theorem OAI.ForcedComputation.VelocityDetector.CylinderC1L2.mono line 61
  8. theorem OAI.ForcedComputation.VelocityDetector.CylinderCInH2.mono line 69
  9. theorem OAI.ForcedComputation.VelocityDetector.CylinderCInH2.congr_slices line 74
  10. theorem OAI.ForcedComputation.VelocityDetector.cylinderCInH1_zero line 80