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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The scalar tail and a third-derivative bound force second directional derivatives to have an integrable square envelope.

  1. def OAI.ForcedComputation.VelocityDetector.derivativeTail line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.derivativeTail_pos line 16
  3. theorem OAI.ForcedComputation.VelocityDetector.derivativeTail_le_one line 19
  4. theorem OAI.ForcedComputation.VelocityDetector.derivativeTail_cube line 22
  5. theorem OAI.ForcedComputation.VelocityDetector.derivativeTail_continuous line 27
  6. theorem OAI.ForcedComputation.VelocityDetector.derivativeTail_square_integrable line 30
  7. theorem OAI.ForcedComputation.VelocityDetector.scalar_second_directional_tail line 52
  8. theorem OAI.ForcedComputation.VelocityDetector.scalar_first_directional_tail line 83