OAI/MathematicalPhysics/NavierStokes/VelocityDetection/MachineTorus.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.MachineTorus.data line 12
  2. def OAI.VelocityDetection.MachineTorus.initialAddress line 15

    Also declared: ComparatorChallenges/NavierStokesVelocity.lean:767 (same declaration text).

  3. def OAI.VelocityDetection.MachineTorus.force line 18
  4. def OAI.VelocityDetection.MachineTorus.velocity line 21
  5. def OAI.VelocityDetection.MachineTorus.correctnessTrace line 25
  6. theorem OAI.VelocityDetection.MachineTorus.trace_initial line 30
  7. theorem OAI.VelocityDetection.MachineTorus.trace_active line 33
  8. theorem OAI.VelocityDetection.MachineTorus.contDiff_force line 38
  9. theorem OAI.VelocityDetection.MachineTorus.force_periodic line 42
  10. theorem OAI.VelocityDetection.MachineTorus.bounded_force line 46
  11. theorem OAI.VelocityDetection.MachineTorus.force_support line 52
  12. theorem OAI.VelocityDetection.MachineTorus.contDiff_velocity line 60
  13. theorem OAI.VelocityDetection.MachineTorus.comparisonClass line 64
  14. theorem OAI.VelocityDetection.MachineTorus.navierStokes line 68
  15. theorem OAI.VelocityDetection.MachineTorus.unique line 72
  16. theorem OAI.VelocityDetection.MachineTorus.detection line 78
  17. theorem OAI.VelocityDetection.MachineTorus.analytic_result line 85