OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/EnergyComplexLe.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinaryRoughWeighted.energy_complex_le line 28
2. lemma OAI.OrdinaryRoughWeighted.fourth_complex_le line 51
3. theorem OAI.OrdinaryRoughWeighted.weighted_short_convolution line 81
4. theorem OAI.OrdinaryRoughWeighted.weighted_correlation_bound line 117