OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/FiniteSchur.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySparseSieve.finite_schur line 14
2. def OAI.OrdinarySparseSieve.weightedGram line 47
3. lemma OAI.OrdinarySparseSieve.weightedGram_symm line 50
4. lemma OAI.OrdinarySparseSieve.weighted_dual_energy line 60
5. lemma OAI.OrdinarySparseSieve.complex_cauchy_sq line 92
6. theorem OAI.OrdinarySparseSieve.sparse_majorant_duality line 100