OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/DetectorForceSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Locality of the prescribed force: where the planar processor and every injection vanish on a spatial neighborhood, all terms of the force vanish.

  1. theorem OAI.ForcedComputation.VelocityDetector.triangularForce_zero_of_neighborhood line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.detector_coefficients_zero_of_neighborhood line 38
  3. theorem OAI.ForcedComputation.VelocityDetector.detectorForce_zero_of_neighborhood line 54