OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCofactorWindow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The cofactor polynomial has an actual fixed multiplicative window. Finite partial summation turns its ordinary reciprocal-count prefix bound into a pointwise bound for that polynomial.

  1. lemma OAI.TwoPointCorrelations.mrt_cofactor_window_set line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorWindow.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_cofactor_window_ratio line 48

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorWindow.lean:48 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.mrt_dirichlet_atom_twist line 68

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorWindow.lean:68 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrt_cofactor_window_identity line 80

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorWindow.lean:80 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.mrt_cofactor_bound_of_prefix line 95

    Source documentation

    Only the prefixes in the actual cofactor scale enter this bound.

    Also declared: OAI/NumberTheory/TwoPointCorrelations/MRTCofactorWindow.lean:95 (same declaration text).

    theorem mrt_cofactor_bound_of_prefix (P : Finset ℕ) (F : ℕ → ℂ)
    (N : ℕ) {a : ℝ} (ha : 1 ≤ a) (hx : 2 ≤ (N : ℝ) / a)
    (t : ℝ) {A : ℝ} (hA : 0 ≤ A)
    (hprefix : ∀ k ∈ Icc ⌊(N : ℝ) / a⌋₊ ⌊(2 * N : ℝ) / a⌋₊,
      ‖∑ n ∈ Icc 1 k, (F n * conj (mrtArchimedeanTwist t n)) /
        ((finitePrimeDivisorCount P n : ℂ) + 1)‖ ≤ A * k) :
    ‖mrtCofactorPolynomial P F N a t‖ ≤ 5 * A := by
…

    Mentions: OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.finitePrimeDivisorCount, OAI.TwoPointCorrelations.mrtCofactorPolynomial