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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

One rational translation supplies the entire input-dependent loading period.

  1. def OAI.ForcedComputation.centeredBox line 15
  2. theorem OAI.ForcedComputation.centeredBox_center line 18
  3. theorem OAI.ForcedComputation.centeredBox_halfWidth line 23
  4. def OAI.ForcedComputation.loaderInstruction line 28
  5. def OAI.ForcedComputation.loaderInput line 31
  6. theorem OAI.ForcedComputation.loaderInstruction_image line 39
  7. theorem OAI.ForcedComputation.loaderInput_valid line 46
  8. theorem OAI.ForcedComputation.loaderInstruction_center line 141
  9. theorem OAI.ForcedComputation.loaderInstruction_contains_center line 146
  10. theorem OAI.ForcedComputation.loaderFlow_endpoint line 154
  11. theorem OAI.ForcedComputation.loaderFlow_first_le line 172
  12. theorem OAI.ForcedComputation.loaderFlow_first_ge line 186