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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integration by parts against a compact scalar test function on the whole plane. The diffusing scalar itself need not have compact support.

  1. theorem OAI.ForcedComputation.VelocityDetector.spatialD_mul line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.integral_compact_spatialD line 25
  3. theorem OAI.ForcedComputation.VelocityDetector.integral_compact_second_spatialD line 40
  4. theorem OAI.ForcedComputation.VelocityDetector.integral_compact_laplacian line 57