OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/CofactorEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinarySmoothRough.cofactorEnergy line 23
2. lemma OAI.OrdinarySmoothRough.cofactor_coefficient_bound line 26
3. lemma OAI.OrdinarySmoothRough.complex_norm_add_sq line 36
4. lemma OAI.OrdinarySmoothRough.cofactorEnergy_union line 40
5. lemma OAI.OrdinarySmoothRough.cofactorEnergy_biUnion line 50
6. theorem OAI.OrdinarySmoothRough.sparse_cofactor_decomposition line 62