English
As x approaches 1 from the right, the real part of the residue-class L-series grows at least like (q totient)^{-1}/(x-1) up to a bounded constant.
Русский
При x → 1+ вещественная часть L‑серии остаточного класса растёт не меньше чем пропорционально (q totient)^{-1}/(x-1) минус константа.
LaTeX
$$$\\exists C\\in\\mathbb{R}\\,\\forall x\\in(1,2],\\; (q.totient)^{-1}/(x-1) - C \\le \\sum'_{n} \\frac{\\operatorname{residueClass}(a,n)}{n^x}$$$
Lean4
/-- As `x` approaches `1` from the right along the real axis, the L-series of
`ArithmeticFunction.vonMangoldt.residueClass` is bounded below by `(q.totient)⁻¹/(x-1) - C`. -/
theorem LSeries_residueClass_lower_bound (ha : IsUnit a) :
∃ C : ℝ, ∀ {x : ℝ} (_ : x ∈ Set.Ioc 1 2), (q.totient : ℝ)⁻¹ / (x - 1) - C ≤ ∑' n, residueClass a n / (n : ℝ) ^ x :=
by
have H {x : ℝ} (hx : 1 < x) :
∑' n, residueClass a n / (n : ℝ) ^ x = (LFunctionResidueClassAux a x).re + (q.totient : ℝ)⁻¹ / (x - 1) :=
by
refine ofReal_injective ?_
simp only [ofReal_tsum, ofReal_div, ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast, ofReal_add, ofReal_inv,
ofReal_sub, ofReal_one]
simp_rw [← LFunctionResidueClassAux_real ha hx,
eqOn_LFunctionResidueClassAux ha <| Set.mem_setOf.mpr (ofReal_re x ▸ hx), sub_add_cancel, LSeries, term]
refine tsum_congr fun n ↦ ?_
split_ifs with hn
· simp only [hn, residueClass_apply_zero, ofReal_zero, zero_div]
· rfl
have : ContinuousOn (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) (Set.Icc 1 2) :=
continuous_re.continuousOn.comp (t := Set.univ) (continuousOn_LFunctionResidueClassAux a)
(fun ⦃x⦄ a ↦ trivial) |>.comp
continuous_ofReal.continuousOn fun x hx ↦ by simpa only [Set.mem_setOf_eq, ofReal_re] using hx.1
obtain ⟨C, hC⟩ := bddBelow_def.mp <| IsCompact.bddBelow_image isCompact_Icc this
replace hC {x : ℝ} (hx : x ∈ Set.Icc 1 2) : C ≤ (LFunctionResidueClassAux a x).re :=
hC (LFunctionResidueClassAux a x).re <| Set.mem_image_of_mem (fun x : ℝ ↦ (LFunctionResidueClassAux a x).re) hx
refine ⟨-C, fun {x} hx ↦ ?_⟩
rw [H hx.1, add_comm, sub_neg_eq_add, add_le_add_iff_left]
exact hC <| Set.mem_Icc_of_Ioc hx
