OAI/NumberTheory/Ostmann/QuadraticCenter/QuadraticEnergyHighMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.quadraticHighWeightIndices line 13
2. theorem OAI.Ostmann.QuadraticCenter.sum_weight_mul_residue_le line 17
3. theorem OAI.Ostmann.QuadraticCenter.quadraticHighWeightIndices_residue line 36
4. theorem OAI.Ostmann.QuadraticCenter.high_weight_periodic_l1_eventually line 48
5. theorem OAI.Ostmann.QuadraticCenter.high_weight_transform_product_eventually line 68