OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/BalancedExpressions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

The balanced compiler uses the existing nonperiodic finite syntax. Periodic time pulses are replaced, on a rational time window, by the finite set of translates which can meet that window. Spatial cutoffs remain exact on the whole plane, including their collars.

  1. def OAI.ForcedComputation.BalancedExpressions.coordinate line 17
  2. theorem OAI.ForcedComputation.BalancedExpressions.coordinate_val line 19
  3. def OAI.ForcedComputation.BalancedExpressions.cutoffCode line 23
  4. theorem OAI.ForcedComputation.BalancedExpressions.cutoffCode_val line 29
  5. def OAI.ForcedComputation.BalancedExpressions.primitiveCode line 35
  6. theorem OAI.ForcedComputation.BalancedExpressions.primitiveCode_val line 43
  7. def OAI.ForcedComputation.BalancedExpressions.potentialCode line 49
  8. theorem OAI.ForcedComputation.BalancedExpressions.potentialCode_val line 52
  9. def OAI.ForcedComputation.BalancedExpressions.translateIndices line 57
  10. def OAI.ForcedComputation.BalancedExpressions.translatePulse line 60
  11. theorem OAI.ForcedComputation.BalancedExpressions.translatePulse_val line 64
  12. def OAI.ForcedComputation.BalancedExpressions.pulseCode line 71
  13. theorem OAI.ForcedComputation.BalancedExpressions.pulseCode_val line 74
  14. def OAI.ForcedComputation.BalancedExpressions.hamiltonianCode line 90
  15. theorem OAI.ForcedComputation.BalancedExpressions.hamiltonianCode_val line 93
  16. def OAI.ForcedComputation.BalancedExpressions.hamiltonianField line 101
  17. theorem OAI.ForcedComputation.BalancedExpressions.horizontal_derivative line 104
  18. theorem OAI.ForcedComputation.BalancedExpressions.hamiltonianField_val line 127