OAI/NumberTheory/TwoPoint/Halasz/HalaszCauchyMeanSquare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Summing the translated unit-window estimates against the Cauchy weight gives the global weighted mean square used in the Perron argument.

  1. lemma OAI.TwoPointCorrelations.halasz_polynomial_norm_le line 14

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCauchyMeanSquare.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_cauchy_polynomial_integrable line 21

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCauchyMeanSquare.lean:21 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_cauchy_integer_summable line 38

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCauchyMeanSquare.lean:38 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_cauchy_weight_window line 54

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCauchyMeanSquare.lean:54 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.halasz_prime_mean_square_cauchy line 65

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszCauchyMeanSquare.lean:65 (same declaration text).