OAI/NumberTheory/TwoPointCorrelations/HalaszCauchySchwarz.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The finite-interval Cauchy--Schwarz step of the triple convolution. One factor keeps its unweighted prime mean square; the second uses the Cauchy weight from Perron's kernel.

  1. lemma OAI.TwoPointCorrelations.halasz_integral_cauchy_schwarz line 14

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszCauchySchwarz.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_weighted_integral_cauchy_schwarz line 33

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszCauchySchwarz.lean:33 (same declaration text).