OAI/NumberTheory/Ostmann/Preliminaries/CosecantHilbertBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Montgomery--Vaughan's finite unweighted Hilbert inequality

This is Theorem 1, inequality (1.2), of Montgomery--Vaughan (1974). It is derived from the checked finite kernel cancellation and row estimate.

  1. def OAI.Ostmann.cosecantMatrix line 20
  2. theorem OAI.Ostmann.cosecantMatrix_hermitian line 24
  3. theorem OAI.Ostmann.cosecant_eigenvalue_bound line 27
  4. theorem OAI.Ostmann.cosecantMatrix_norm_bound line 42
  5. theorem OAI.Ostmann.cosecant_hilbert_bound line 58