OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PhaseBalls.lean
3 declarations, 0 contain sorry, 0 declared as axioms
Rational balls for the finite derivative recurrence of the logarithmic clock. No modulus for a derivative of the slowed field is assumed.
- def
OAI.ForcedComputation.phaseBallsline 12 - theorem
OAI.ForcedComputation.phaseBalls_containsline 19 - theorem
OAI.ForcedComputation.phaseBalls_convergesline 35