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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The arbitrary-center force is supported in the spatial support of the input processor together with one fixed small torus neighborhood.

  1. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.torusNorm_lipschitz line 15
  2. def OAI.ForcedComputation.VelocityDetector.CompactCenter.processorSupport line 31
  3. def OAI.ForcedComputation.VelocityDetector.CompactCenter.injectionNeighborhood line 34
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.injectionNeighborhood_closed line 37
  5. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.injectionNeighborhood_contains line 41
  6. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.processor_zero_outside line 50
  7. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centered_bump_zero_outside line 55
  8. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredSource_zero_outside line 83
  9. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredForce_supported line 92