OAI/NumberTheory/Ostmann/Preliminaries/SymmetricQuadraticBound.lean
1 declarations, 0 contain sorry, 0 declared as axioms
The finite quadratic bound for the cosecant row estimate
- theorem
OAI.Ostmann.real_symmetric_quadratic_upperline 16