OAI/NumberTheory/Ostmann/QuadraticCenter/InverseWeylBins.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.weylBin line 8
2. def OAI.Ostmann.QuadraticCenter.weylKey line 9
3. theorem OAI.Ostmann.QuadraticCenter.weylBin_le line 12
4. theorem OAI.Ostmann.QuadraticCenter.weylKey_injective_on line 16
5. def OAI.Ostmann.QuadraticCenter.weylBinWeight line 69
6. theorem OAI.Ostmann.QuadraticCenter.le_weylBinWeight line 72
7. theorem OAI.Ostmann.QuadraticCenter.weylBinWeight_sum line 87
8. theorem OAI.Ostmann.QuadraticCenter.separated_linear_sum_bound line 96