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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Strong differentiation of the scalar in the actual L2 norm.

  1. theorem OAI.ForcedComputation.VelocityDetector.planeL2_slope_ae line 13
  2. theorem OAI.ForcedComputation.VelocityDetector.planeL2_hasDerivWithinAt_of_strongDerivative line 25