ResidueSummatory.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The uniform progression estimate for rough squarefree integers

def OAI.JointDickman.roughResidueSummatory line 12
theorem OAI.JointDickman.auxiliary_modulus_le_cutoff line 16

theorem OAI.JointDickman.roughResidueSummatory_error line 26

Source documentation

Equidistribution in the unit classes, before partial summation.

theorem roughResidueSummatory_error
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z D : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) (hD : 0 ≤ D) :
    ∃ K : ℝ, 0 ≤ K ∧ ∀ᶠ B : ℕ in atTop, ∀ Y : ℝ,
      (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log Y → 9 ≤ Y →
      ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
      ∀ r : (ZMod q)ˣ,
      |roughResidueSummatory (r : ZMod q) (Nat.primesLE (auxiliaryCutoff B)) z Y -
        roughSquarefreeSummatory (Nat.primesLE (auxiliaryCutoff B)) z Y / q.totient| ≤
        K * Y * (B : ℝ) ^ (-D) := by
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.roughResidueSummatory, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.roughSquarefreeSummatory

theorem OAI.JointDickman.roughResidueSummatory_expansion line 50

Source documentation

The same actual coefficients as the untwisted expansion serve in all unit progressions; the error is uniform in every modulus up to B^100.

theorem roughResidueSummatory_expansion
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) {z D : ℝ}
    (hz : z = 1 / 4 ∨ z = 1 / 2) (hD : 0 ≤ D) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant z ∧ 0 < c 0 ∧
      ∃ H : ℕ, ∃ K : ℝ, 0 ≤ K ∧ ∀ᶠ B : ℕ in atTop, ∀ Y : ℝ,
        (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log Y → 9 ≤ Y →
        ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
        ∀ r : (ZMod q)ˣ,
        |roughResidueSummatory (r : ZMod q) (Nat.primesLE (auxiliaryCutoff B)) z Y -
          (Y * ∑ ν ∈ range (H + 1),
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.roughResidueSummatory, OAI.JointDickman.auxiliaryCutoff