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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The analytic detector at an arbitrary center. Its prescribed drift and source are translations of the fixed-center program. The two numerical choices use the same force.

  1. def OAI.ForcedComputation.VelocityDetector.CompactCenter.centerShift line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.reference_add_shift line 18
  3. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.euclidean_translated line 22
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.euclidean_translated_first line 28
  5. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.euclidean_translated_second line 33
  6. def OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredDrift line 41
  7. def OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredSource line 44
  8. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredDrift_eq line 47
  9. def OAI.ForcedComputation.VelocityDetector.CompactCenter.centeredForce line 55
  10. theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.general_center_compact_detector line 59