OAI/MathematicalPhysics/NavierStokes/VelocityDetection/RationalEvaluation.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.Effective.Ball.converges_add line 10
  2. theorem OAI.VelocityDetection.Effective.Ball.converges_neg line 16
  3. theorem OAI.VelocityDetection.Effective.Ball.converges_mul line 20
  4. theorem OAI.VelocityDetection.Effective.Ball.converges_inv line 27
  5. theorem OAI.VelocityDetection.Effective.Ball.eventually_invSafe line 37
  6. theorem OAI.VelocityDetection.Effective.Ball.converges_flat line 45
  7. def OAI.VelocityDetection.Effective.Expr.round line 67

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

  8. def OAI.VelocityDetection.Effective.Expr.safe line 76

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

  9. theorem OAI.VelocityDetection.Effective.Expr.round_certifies line 85
  10. theorem OAI.VelocityDetection.Effective.Expr.round_converges line 97
  11. def OAI.VelocityDetection.Effective.coordinateD line 131

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

  12. def OAI.VelocityDetection.Effective.mixedD line 134

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

  13. theorem OAI.VelocityDetection.Effective.coordinateD_congr line 138
  14. theorem OAI.VelocityDetection.Effective.mixedD_congr line 145
  15. theorem OAI.VelocityDetection.Effective.Expr.coordinateD_eval line 162
  16. theorem OAI.VelocityDetection.Effective.Expr.mixedD_eval line 166
  17. def OAI.VelocityDetection.Effective.accuracy line 183

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

  18. def OAI.VelocityDetection.Effective.Names line 185

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

  19. def OAI.VelocityDetection.Effective.inputBall line 188

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

  20. theorem OAI.VelocityDetection.Effective.accuracy_nonneg line 191
  21. theorem OAI.VelocityDetection.Effective.accuracy_tendsto line 193
  22. theorem OAI.VelocityDetection.Effective.inputBall_certifies line 197
  23. theorem OAI.VelocityDetection.Effective.inputBall_converges line 201
  24. def OAI.VelocityDetection.Effective.trial line 208

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

  25. theorem OAI.VelocityDetection.Effective.trial_correct line 214
  26. theorem OAI.VelocityDetection.Effective.trial_terminates line 227