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

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The classical comparison class on R² times the unit circle. The Sobolev conditions use actual L2 representatives of the classical spatial derivatives. No spatial decay of a competing solution is assumed.

  1. def OAI.ForcedComputation.VelocityDetector.cylinderPullback line 14
  2. def OAI.ForcedComputation.VelocityDetector.scalarSpatialD line 16
  3. def OAI.ForcedComputation.VelocityDetector.CylinderCInH2 line 19
  4. def OAI.ForcedComputation.VelocityDetector.CylinderCInH1 line 25
  5. def OAI.ForcedComputation.VelocityDetector.VerticallyPeriodic line 29
  6. structure OAI.ForcedComputation.VelocityDetector.IsCylinderClassicalSolution line 32