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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Finite expressions for the actual moving Hamiltonian gates, including all collar terms. The center velocity is differentiated from its code.

  1. def OAI.ForcedComputation.ExpandingDetector.displacementCode line 16
  2. theorem OAI.ForcedComputation.ExpandingDetector.displacementCode_val line 20
  3. def OAI.ForcedComputation.ExpandingDetector.gateCutoffCode line 32
  4. theorem OAI.ForcedComputation.ExpandingDetector.gateCutoffCode_val line 36
  5. def OAI.ForcedComputation.ExpandingDetector.gatePotentialCode line 47
  6. def OAI.ForcedComputation.ExpandingDetector.movingGatePotential line 53
  7. theorem OAI.ForcedComputation.ExpandingDetector.gatePotentialCode_val line 56
  8. theorem OAI.ForcedComputation.ExpandingDetector.movingGatePotential_smooth line 67
  9. def OAI.ForcedComputation.ExpandingDetector.horizontalSpaceTime line 78
  10. theorem OAI.ForcedComputation.ExpandingDetector.expression_spatial_lift line 82
  11. def OAI.ForcedComputation.ExpandingDetector.movingGateCode line 111
  12. theorem OAI.ForcedComputation.ExpandingDetector.movingGateCode_val line 116