OAI/NumberTheory/Ostmann/QuadraticCenter/AdaptiveArrayLinear.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.adaptive_jacobi_norm_le line 9
2. theorem OAI.Ostmann.QuadraticCenter.adaptive_sqrt_inv_norm_le line 12
3. def OAI.Ostmann.QuadraticCenter.adaptiveArrayLinear line 19
4. theorem OAI.Ostmann.QuadraticCenter.adaptiveArrayLinear_sub line 24
5. theorem OAI.Ostmann.QuadraticCenter.adaptiveArrayLinear_norm_le line 30
6. theorem OAI.Ostmann.QuadraticCenter.positiveDivisorArray_eq_linear line 71