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

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Arbitrary effective centers are handled by fast names. A translated input oracle is compiled from the original oracle and the center name; translation does not change its global derivative bounds.

  1. def OAI.ForcedComputation.VelocityDetector.CompactNames.addPoint line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.rationalPoint_add line 17
  3. def OAI.ForcedComputation.VelocityDetector.CompactNames.addName line 24
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.addName_spec line 27
  5. def OAI.ForcedComputation.VelocityDetector.CompactNames.rationalShiftName line 44
  6. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.rationalShiftName_spec line 47
  7. def OAI.ForcedComputation.VelocityDetector.CompactNames.inputShift line 54
  8. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.inputShift_smooth line 57
  9. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.componentJet_shift line 61
  10. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.coordinate_clock line 72
  11. def OAI.ForcedComputation.VelocityDetector.CompactNames.shiftedEnclosure line 75
  12. theorem OAI.ForcedComputation.VelocityDetector.CompactNames.shiftedEnclosure_contains line 82
  13. def OAI.ForcedComputation.VelocityDetector.CompactNames.shiftedOracle line 93