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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Horizontal scalar lifts preserve the strong Sobolev conditions. Their vertical derivatives vanish, and their horizontal derivatives are the ordinary derivatives of the planar scalar.

  1. def OAI.ForcedComputation.VelocityDetector.scalarPlaneLift line 17
  2. theorem OAI.ForcedComputation.VelocityDetector.scalarPlaneLift_pullback line 19
  3. theorem OAI.ForcedComputation.VelocityDetector.scalarPlaneLift_spatialD line 25
  4. theorem OAI.ForcedComputation.VelocityDetector.scalarPlaneLift_verticalD line 35
  5. theorem OAI.ForcedComputation.VelocityDetector.CylinderContinuousL2.congr_slices line 43
  6. theorem OAI.ForcedComputation.VelocityDetector.CylinderC1L2.congr_slices line 49
  7. theorem OAI.ForcedComputation.VelocityDetector.cylinderContinuousL2_zero line 58
  8. theorem OAI.ForcedComputation.VelocityDetector.PlaneContinuousL2.scalarPlaneLift line 62
  9. theorem OAI.ForcedComputation.VelocityDetector.PlaneCInH2.scalarPlaneLift line 67