OAI/NumberTheory/Ostmann/QuadraticSieveMellinSeparation.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticSieve.mellinTwistline 10 - def
OAI.Ostmann.QuadraticSieve.coprimeMellinJacobiKernelline 13 - theorem
OAI.Ostmann.QuadraticSieve.bilinearMellinRow_jacobiline 16 - theorem
OAI.Ostmann.QuadraticSieve.coprime_jacobi_mellin_separationline 28 - theorem
OAI.Ostmann.QuadraticSieve.coprime_jacobi_mellin_weight_integrableline 44 - theorem
OAI.Ostmann.QuadraticSieve.coefficientEnergy_mellinTwistline 55