OAI/NumberTheory/Ostmann/Characters/SkewKernelSquare.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A finite algebraic identity for the large-sieve kernel

This is the cancellation underlying Montgomery--Vaughan's equation (3.6). The diagonal correction is retained explicitly before any norm estimate.

  1. theorem OAI.Ostmann.skew_kernel_square_entry line 20