OAI/NumberTheory/Ostmann/QuadraticCenter/InverseWeylWitnessAbel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.QuadraticCenter.exists_large_partial_sum_of_cutoff_weighted line 11
2. theorem OAI.Ostmann.QuadraticCenter.progression_weyl_sum_eq line 31
3. lemma OAI.Ostmann.QuadraticCenter.progression_weyl_sum_norm line 42
4. lemma OAI.Ostmann.QuadraticCenter.quadraticWeylSum_norm_le_length line 47
5. theorem OAI.Ostmann.QuadraticCenter.exists_quadraticWeylSum_of_weighted_progression line 55