summable_norm_eisSummand — Mathlib

English

If k is at least 3, then for each z in the upper half-plane, the family x ↦ |eisSummand(k,x,z)| is summable over x ∈ Fin(2 → ℤ).

Русский

При k ≥ 3 для любой z в верхней полуплоскости семейство x ↦ |eisSummand(k,x,z)| сходится по сумме по x ∈ Fin(2 → ℤ).

LaTeX

$$$\text{Summable}_{x:Fin(2\to\mathbb{Z})} \|\mathrm{eisSummand}(k,x,z)\|,$ если $3 \le k$.$$

Lean4

theorem summable_norm_eisSummand {k : ℤ} (hk : 3 ≤ k) (z : ℍ) : Summable fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖ :=
  by
  have hk' : (2 : ℝ) < k := by norm_cast
  apply ((summable_one_div_norm_rpow hk').mul_left <| r z ^ (-k : ℝ)).of_nonneg_of_le (fun _ ↦ norm_nonneg _)
  intro b
  simp only [eisSummand, norm_zpow]
  exact_mod_cast summand_bound z (show 0 ≤ (k : ℝ) by positivity) b

Похожие утверждения