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

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Finite expressions for an individual prescribed detector block. The processor and bump are sampled by explicit rational clock profiles.

  1. def OAI.ForcedComputation.VelocityDetector.bumpExpression line 16
  2. theorem OAI.ForcedComputation.VelocityDetector.bumpExpression_valid line 20
  3. theorem OAI.ForcedComputation.VelocityDetector.bumpExpression_val line 23
  4. def OAI.ForcedComputation.VelocityDetector.processorComponent line 29
  5. theorem OAI.ForcedComputation.VelocityDetector.processorComponent_valid line 32
  6. theorem OAI.ForcedComputation.VelocityDetector.processorComponent_val line 36
  7. def OAI.ForcedComputation.VelocityDetector.sourceTermExpression line 44
  8. theorem OAI.ForcedComputation.VelocityDetector.sourceTermExpression_valid line 48
  9. theorem OAI.ForcedComputation.VelocityDetector.sourceTermExpression_val line 52
  10. def OAI.ForcedComputation.VelocityDetector.driftComponentExpression line 58
  11. theorem OAI.ForcedComputation.VelocityDetector.driftComponentExpression_valid line 62
  12. theorem OAI.ForcedComputation.VelocityDetector.driftComponentExpression_val line 66
  13. def OAI.ForcedComputation.VelocityDetector.driftTermExpression line 74
  14. theorem OAI.ForcedComputation.VelocityDetector.driftTermExpression_valid line 77
  15. theorem OAI.ForcedComputation.VelocityDetector.driftTermExpression_val line 85
  16. def OAI.ForcedComputation.VelocityDetector.sourcePrefixExpression line 98
  17. def OAI.ForcedComputation.VelocityDetector.driftPrefixExpression line 101
  18. theorem OAI.ForcedComputation.VelocityDetector.sourcePrefixExpression_valid line 104
  19. theorem OAI.ForcedComputation.VelocityDetector.driftPrefixExpression_valid line 107
  20. theorem OAI.ForcedComputation.VelocityDetector.sourcePrefixExpression_val line 111
  21. theorem OAI.ForcedComputation.VelocityDetector.driftPrefixExpression_val line 117