OAI/NumberTheory/Ostmann/QuadraticCenter/AdaptiveSmallArray.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticCenter.exists_near_adaptiveSmallArrayFamilyline 12 - theorem
OAI.Ostmann.QuadraticCenter.adaptive_small_radius_lowerline 39 - theorem
OAI.Ostmann.QuadraticCenter.eventually_near_adaptiveOffEventArrayFamilyline 45 - theorem
OAI.Ostmann.QuadraticCenter.adaptiveSmallArray_total_errorline 63