OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimeTruncation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The small- and large-prime deletion in the double-convolution argument. All errors are uniform over one-bounded coefficients.

  1. def OAI.TwoPointCorrelations.halaszPrimeTerm line 14

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

  2. def OAI.TwoPointCorrelations.halaszPrimePrefix line 17

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:17 (same declaration text).

  3. def OAI.TwoPointCorrelations.halaszPrimeBandConvolution line 20

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:20 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_prime_term_bound line 23

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:23 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_prime_set_bound line 42

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:42 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_prime_prefix_eq line 50

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:50 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_prime_band_eq line 58

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:58 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.halasz_prime_prefix_bound line 63

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:63 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.halasz_prime_band_bound line 69

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:69 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.halasz_prime_truncation_error line 77

    Source documentation

    Delete all primes at most L and greater than N/2.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:77 (same declaration text).

    theorem halasz_prime_truncation_error (f : ℕ → ℂ) (hf : OneBounded f)
    (N : ℕ) {L : ℝ} (hL : 1 ≤ L) (hLN : L ≤ (N : ℝ) / 2) :
    ‖halaszPrimeConvolution f N - halaszPrimeBandConvolution f N L ((N : ℝ) / 2)‖ ≤
      (N : ℝ) * (Real.log L + Real.log 2 + 3 * halaszMertensConstant) := by
…

    Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszPrimeConvolution, OAI.TwoPointCorrelations.halaszPrimeBandConvolution, OAI.TwoPointCorrelations.halaszMertensConstant

  11. theorem OAI.TwoPointCorrelations.halasz_truncated_convolution_mean_bound line 101

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeTruncation.lean:101 (same declaration text).