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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The local Hamiltonian translation gate used at each finite address. Its plateau is exact and its support is inherited from the cutoff.

  1. theorem OAI.ForcedComputation.ExpandingDetector.field_translate line 14
  2. def OAI.ForcedComputation.ExpandingDetector.translationGate line 20
  3. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_smooth line 24
  4. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_solenoidal line 31
  5. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_plateau line 38
  6. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_support line 46
  7. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_compactSupport line 50