norm_le_tsum_norm — Mathlib

English

The norm of the Eisenstein series is bounded by the sum of the norms of its summands: ||eisensteinSeries(a,k,z)|| ≤ ∑' x ‖eisSummand(k,x,z)‖.

Русский

Норма ряда Эйзенштейна не превышает сумму норм его слагаемых: ||EisensteinSeries(a,k,z)|| ≤ ∑' x ‖eisSummand(k,x,z)‖.

LaTeX

$$$\|\mathrm{eisensteinSeries}(a,k,z)\| \leq \sum'_{x:Fin(2\to\mathbb{Z})} \|\mathrm{eisSummand}(k,x,z)\|.$$$

Lean4

/-- The norm of the restricted sum is less than the full sum of the norms. -/
theorem norm_le_tsum_norm (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k) (z : ℍ) :
    ‖eisensteinSeries a k z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖ :=
  by
  simp_rw [eisensteinSeries]
  apply
    le_trans (norm_tsum_le_tsum_norm ((summable_norm_eisSummand hk z).subtype _))
      (Summable.tsum_subtype_le (fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖) _ (fun _ ↦ norm_nonneg _)
        (summable_norm_eisSummand hk z))

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