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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The scalar and its first two spatial derivatives vary continuously in L2 on each closed finite time interval. This is the spatial H2 time condition.

  1. theorem OAI.ForcedComputation.VelocityDetector.planeTailProfile_le_derivativeTail line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.uniform_jet2_tail line 24
  3. def OAI.ForcedComputation.VelocityDetector.PlaneH2ContinuousOn line 61
  4. theorem OAI.ForcedComputation.VelocityDetector.PlaneScalarSolution.h2_continuousOn line 66