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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The square-distance formulation gives continuity in the usual L2 space, rather than only pointwise time continuity.

  1. abbrev OAI.ForcedComputation.VelocityDetector.PlaneL2 line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.planeL2_norm_sq line 16
  3. theorem OAI.ForcedComputation.VelocityDetector.planeL2_sub_norm_sq line 24
  4. theorem OAI.ForcedComputation.VelocityDetector.planeL2_continuousOn_of_squareDistance line 30