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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Certified rational balls for a periodic field evaluated at a smooth clock. The outer evaluation is refined to an explicit dyadic tolerance; the clock error uses the field's global derivative bound.

  1. theorem OAI.ForcedComputation.QBall.converges_of_contains line 15
  2. def OAI.ForcedComputation.ClockedExpr.fieldVector line 26
  3. theorem OAI.ForcedComputation.ClockedExpr.fieldVector_valid line 28
  4. def OAI.ForcedComputation.ClockedExpr.dyadic line 31
  5. theorem OAI.ForcedComputation.ClockedExpr.dyadic_pos line 33
  6. theorem OAI.ForcedComputation.ClockedExpr.dyadic_cast line 35
  7. theorem OAI.ForcedComputation.ClockedExpr.dyadic_tendsto line 38
  8. def OAI.ForcedComputation.ClockedExpr.fieldBall line 41
  9. theorem OAI.ForcedComputation.ClockedExpr.fieldBall_contains line 48
  10. theorem OAI.ForcedComputation.ClockedExpr.fieldBall_converges line 85