ArithmeticKernelMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual lag kernel inherits the uniform arithmetic mass bound

theorem OAI.JointDickman.arithmeticLagMass_eq_kernel line 11

theorem OAI.JointDickman.arithmeticKernelMass_bound line 34

Source documentation

The normalized kernel has the manuscript's summable lag majorant. The statement is simultaneous in every regularity parameter.

theorem arithmeticKernelMass_bound
    (hFord : PublishedInputs.FordUpperSieveInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ K : ℝ, 0 < K ∧ ∀ᶠ B : ℕ in atTop, ∀ T : ℕ, ∀ j : ℤ,
      0 < T → (T : ℝ) ≤ Real.exp ((1/10 : ℝ)*B) → j ≠ 0 →
      j.natAbs ≤ auxiliaryCutoff B → ∀ ε : ℝ, 0 < ε →
      ∀ᶠ N : ℕ in atTop, ∀ L : ℕ, ∀ τ C : ℝ,
        (∑ n ∈ Icc 1 (arithmeticGraphVertexCap B N),
          rawArithmeticGraphKernel B L τ C T N j n)/((B : ℝ)*T*N) ≤
          K*singularFactor 24 j.natAbs/(T : ℝ)+ε := by
…

Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.auxiliaryCutoff, OAI.JointDickman.arithmeticGraphVertexCap, OAI.JointDickman.rawArithmeticGraphKernel, OAI.JointDickman.singularFactor