LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Absolute convergence and holomorphy of the lattice Eisenstein sums

Statement

For every even $k \geq 4$ and every $τ \in H$ the family $((m τ + n)^{- k})_{(m, n) \in Z^{2} ∖ {(0, 0)}}$ is absolutely summable, and the convergence is uniform on compact subsets of $H$ . Consequently $G_{k} (τ) : = \sum_{(m, n)}^{'} (m τ + n)^{- k}$ defines a holomorphic function on $H$ , and it depends only on the lattice $Λ_{τ} = Z + Z τ$ assigned to $τ$ .

Facts & Assumptions

Given: An even integer $k \geq 4$ , the upper half-plane $H$ with $Im > 0$ (The modular group and its action on the upper half-plane), and a compact $K \subseteq H$ with $Im τ \geq y_{0} > 0$ and $∣ Re τ ∣ \leq X$ for all $τ \in K$ .

[F1]

Convergence, absolute convergence and nonnegative comparison of series are as in Series, partial sums, convergence and the sum, divergence, and the tail series, Absolutely convergent and conditionally convergent series, and the general starting index and A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum.

[F2]

If $0 \leq a_{j} \leq b_{j}$ eventually and $\sum b_{j}$ converges then $\sum a_{j}$ converges (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ); $\sum_{j} j^{- p}$ converges for rational $p > 1$ (For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ ).

[F3]

For a complex double family with summable absolute values, apply the real double-series theorem separately to its real and imaginary parts. The family may then be summed in any order, in particular iterated or regrouped into shells (Fubini for double series: if $\sum_{i} \sum_{j} ∣ a_{i j} ∣$ converges then both iterated sums and the sum along every bijection $N \to N \times N$ converge to one and the same value, If $\sum ∣ a_{k} ∣$ converges then $\sum a_{k}$ converges).

[F4]

If holomorphic functions on an open set converge locally uniformly, their limit is holomorphic (Locally uniform limits of holomorphic functions are holomorphic and their derivatives converge locally uniformly).

[F5]

$∣ z + w ∣ \geq ∣ ∣ z ∣ - ∣ w ∣ ∣$ , $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ , and $∣ Re z ∣ \leq ∣ z ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Real and imaginary parts, complex conjugation, and modulus).

Proof

1.1F5givenalgebra

Since $m τ + n = 0$ with $(m, n) \neq (0, 0)$ would give $τ = - n / m \in R$ when $m \neq 0$ and $n = 0$ when $m = 0$ , no denominator vanishes. Let $c_{K} : = \min (1 / 2, y_{0} / \max (1, 2 X)) > 0$ . For $(m, n) \neq (0, 0)$ and $τ \in K$ we claim $∣ m τ + n ∣ \geq c_{K} \max (∣ m ∣, ∣ n ∣)$ . If $∣ n ∣ \geq 2 X ∣ m ∣$ , then $∣ Re (m τ + n) ∣ = ∣ m Re τ + n ∣ \geq ∣ n ∣ - X ∣ m ∣ \geq ∣ n ∣ / 2$ by [F5]; if moreover $∣ n ∣ \geq ∣ m ∣$ then $∣ m τ + n ∣ \geq ∣ n ∣ / 2 \geq \max (∣ m ∣, ∣ n ∣) / 2$ , while if $∣ n ∣ < ∣ m ∣$ then the imaginary part gives $∣ m τ + n ∣ \geq y_{0} ∣ m ∣ = y_{0} \max (∣ m ∣, ∣ n ∣)$ . If instead $∣ n ∣ < 2 X ∣ m ∣$ , then $\max (∣ m ∣, ∣ n ∣) \leq \max (1, 2 X) ∣ m ∣$ and the imaginary part gives $∣ m τ + n ∣ \geq y_{0} ∣ m ∣ \geq \frac{y_{0}}{\max (1, 2 X)} \max (∣ m ∣, ∣ n ∣)$ . In all cases the claim holds.

2.1F1F2F3step 1.1givenalgebra

Regroup the nonzero pairs by the shell $j : = \max (∣ m ∣, ∣ n ∣) \geq 1$ ; the shell has $(2 j + 1)^{2} - (2 j - 1)^{2} = 8 j$ elements, and by 1.1 each contributes at most $(c_{K} j)^{- k}$ , so shell $j$ contributes at most $8 c_{K}^{- k} j^{1 - k}$ . Since $k \geq 4$ gives $k - 1 > 1$ , the bound $\sum_{j \geq 1} 8 c_{K}^{- k} j^{1 - k} < \infty$ follows from [F2]. The shell partial sums of the family are therefore nonnegative and bounded uniformly in $τ \in K$ by an absolute constant, so they converge by the bounded-partial-sums criterion of [F1]; in the terminology of [F1] the family $((m τ + n)^{- k})_{(m, n) \neq (0, 0)}$ is absolutely summable for each $τ \in K$ , the regrouping being licensed by [F3], and the tail beyond shell $J$ is bounded uniformly on $K$ by $8 c_{K}^{- k} \sum_{j > J} j^{1 - k}$ .

3.1F3F4step 2.1givenalgebra∎

Each term $τ \mapsto (m τ + n)^{- k}$ is holomorphic on $H$ for $(m, n) \neq (0, 0)$ , being a power of the nonvanishing holomorphic function $τ \mapsto m τ + n$ . By 2.1 the partial sums over shells converge uniformly on every compact $K \subseteq H$ (compactness supplies some $y_{0}, X$ ), so [F4] makes the shell-sum limit $G_{k}$ holomorphic on $H$ , and this limit agrees with the (absolutely summable, hence order-independent by [F3]) family sum. Finally $(m, n) \mapsto m τ + n$ is a bijection of $Z^{2}$ onto the lattice $Λ_{τ} = Z + Z τ$ , so the summed family is exactly the family of values $λ^{- k}$ over the nonzero points $λ \in Λ_{τ}$ ; hence $G_{k} (τ)$ depends only on $Λ_{τ}$ and not on the enumeration.

Depends on

Used by

Dependency tree · two levels

81 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

J. S. Milne, Modular Functions and Modular Forms (v1.31, 2017) (standard reference, not scraped)
D. Zagier, Elliptic Modular Forms and Their Applications, in The 1-2-3 of Modular Forms (Universitext, Springer, 2008) (standard reference, not scraped)
C. T. McMullen, Advanced Complex Analysis, Math 213a course notes (Harvard, 2010) (standard reference, not scraped)