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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar solution has continuous L2 representatives for all spatial derivatives through order two, and is continuously differentiable in L2.

  1. def OAI.ForcedComputation.VelocityDetector.PlaneContinuousL2 line 14
  2. def OAI.ForcedComputation.VelocityDetector.PlaneCInH2 line 18
  3. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.cInH2 line 23
  4. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.c1L2 line 49