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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Full-orbit separation excludes a false observation both during a burst and during its subsequent heat evolution.

  1. theorem OAI.ForcedComputation.VelocityDetector.torusNorm_zero line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.detectorReference_separated line 20
  3. theorem OAI.ForcedComputation.VelocityDetector.detectorReference_zero_on_target line 39
  4. theorem OAI.ForcedComputation.VelocityDetector.detectorReference_heat_bound line 53