OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/LogPhaseMulConj.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySelbergWeights.logPhase_mul_conj line 17
2. def OAI.OrdinarySelbergWeights.triangleSieveMajorant line 25
3. lemma OAI.OrdinarySelbergWeights.triangleSieveMajorant_nonneg line 28
4. lemma OAI.OrdinarySelbergWeights.triangleSieveMajorant_one line 32
5. lemma OAI.OrdinarySelbergWeights.triangleSieveGram line 46
6. lemma OAI.OrdinarySelbergWeights.sieveTriangleKernel_norm line 63
7. theorem OAI.OrdinarySelbergWeights.sparse_rough_gram_row line 79