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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Certified rational balls for the quadratic and viscous phase fields. All oracle calls go to derivatives of the original finite two-table program.

  1. theorem OAI.ForcedComputation.iteratedDeriv_spatialPhase_eq_mixed line 14
  2. def OAI.ForcedComputation.initializedVelocityBalls line 21
  3. def OAI.ForcedComputation.quadraticPhaseBalls line 26
  4. def OAI.ForcedComputation.viscousPhaseBalls line 34
  5. theorem OAI.ForcedComputation.initializedVelocityBalls_contains line 44
  6. theorem OAI.ForcedComputation.initializedVelocityBalls_converges line 51
  7. theorem OAI.ForcedComputation.quadraticPhaseBalls_contains line 58
  8. theorem OAI.ForcedComputation.quadraticPhaseBalls_converges line 75
  9. theorem OAI.ForcedComputation.viscousPhaseBalls_contains line 90
  10. theorem OAI.ForcedComputation.viscousPhaseBalls_converges line 104