OAI/NumberTheory/Ostmann/Quadratic/QuadraticWeightedBilinearBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integrating the uniform divisor comparison against a smooth weight

  1. theorem OAI.Ostmann.quadratic_weighted_bilinear_bound line 12