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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Canonical representatives in L2 on a finite time interval. The values outside the specified interval have no role in the regularity statement.

  1. def OAI.ForcedComputation.VelocityDetector.planeL2Lift line 12
  2. theorem OAI.ForcedComputation.VelocityDetector.planeL2Lift_ae line 17
  3. theorem OAI.ForcedComputation.VelocityDetector.exists_planeL2_continuous_representation line 23
  4. def OAI.ForcedComputation.VelocityDetector.PlaneC1L2 line 31
  5. theorem OAI.ForcedComputation.VelocityDetector.planeC1L2_of_square_estimates line 36