theorem int_sum_neg {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [T2Space α] (f : ℤ → α) : ∑' (d : ℤ), f d = ∑' (d : ℤ), f (-d)

theorem summable_neg {α : Type u_1} [TopologicalSpace α] [AddCommMonoid α] (f : ℤ → α) (hf : Summable f) : Summable fun (d : ℤ) => f (-d)

theorem aux33 (f : ℕ → ℂ) (hf : Summable f) : ∑' (n : ℕ), f n = limUnder Filter.atTop fun (N : ℕ) => ∑ n ∈ Finset.range N, f n

theorem tsum_pnat_eq_tsum_succ3 {α : Type u_1} [TopologicalSpace α] [AddCommMonoid α] [T2Space α] (f : ℕ → α) : ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f (n + 1)

theorem nat_pos_tsum2 {α : Type u_1} [TopologicalSpace α] [AddCommMonoid α] (f : ℕ → α) (hf : f 0 = 0) : (Summable fun (x : ℕ+) => f ↑x) ↔ Summable f

theorem tsum_pNat {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [T2Space α] [CompleteSpace α] (f : ℕ → α) (hf : f 0 = 0) : ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n

theorem tsum_pnat_eq_tsum_succ4 {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] [T2Space α] (f : ℕ → α) (hf : Summable f) : f 0 + ∑' (n : ℕ+), f ↑n = ∑' (n : ℕ), f n

theorem nat_pos_tsum2' {α : Type u_1} [TopologicalSpace α] [AddCommMonoid α] (f : ℕ → α) : (Summable fun (x : ℕ+) => f ↑x) ↔ Summable fun (x : ℕ) => f (x + 1)

theorem int_nat_sum {α : Type u_1} [AddCommGroup α] [UniformSpace α] [IsUniformAddGroup α] [CompleteSpace α] (f : ℤ → α) : Summable f → Summable fun (x : ℕ) => f ↑x

theorem HasSum.nonneg_add_neg {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] [T2Space α] {a b : α} {f : ℤ → α} (hnonneg : HasSum (fun (n : ℕ) => f ↑n) a) (hneg : HasSum (fun (n : ℕ) => f (-↑n.succ)) b) : HasSum f (a + b)

theorem HasSum.pos_add_zero_add_neg {α : Type u_1} [TopologicalSpace α] [AddCommGroup α] [IsTopologicalAddGroup α] [T2Space α] {a b : α} {f : ℤ → α} (hpos : HasSum (fun (n : ℕ) => f (↑n + 1)) a) (hneg : HasSum (fun (n : ℕ) => f (-↑n.succ)) b) : HasSum f (a + f 0 + b)

theorem int_tsum_pNat {α : Type u_1} [UniformSpace α] [CommRing α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] (f : ℤ → α) (hf2 : Summable f) : ∑' (n : ℤ), f n = f 0 + ∑' (n : ℕ+), f ↑↑n + ∑' (m : ℕ+), f (-↑↑m)

theorem upp_half_not_ints (z : UpperHalfPlane) (n : ℤ) : ↑z ≠ ↑n

theorem aus (a b : ℂ) : a + b ≠ 0 ↔ a ≠ -b

theorem pnat_inv_sub_squares (z : UpperHalfPlane) : (fun (n : ℕ+) => 1 / (↑z - ↑↑n) + 1 / (↑z + ↑↑n)) = fun (n : ℕ+) => 2 * ↑z * (1 / (↑z ^ 2 - ↑↑n ^ 2))

theorem upper_half_plane_ne_int_pow_two (z : UpperHalfPlane) (n : ℤ) : ↑z ^ 2 - ↑n ^ 2 ≠ 0

theorem upbnd (z : UpperHalfPlane) (d : ℤ) : ↑d ^ 2 * EisensteinSeries.r z ^ 2 ≤ ‖↑z ^ 2 - ↑d ^ 2‖

theorem lhs_summable (z : UpperHalfPlane) : Summable fun (n : ℕ+) => 1 / (↑z - ↑↑n) + 1 / (↑z + ↑↑n)

theorem sum_int_even {α : Type u_1} [UniformSpace α] [CommRing α] [IsUniformAddGroup α] [CompleteSpace α] [T2Space α] (f : ℤ → α) (hf : ∀ (n : ℤ), f n = f (-n)) (hf2 : Summable f) : ∑' (n : ℤ), f n = f 0 + 2 * ∑' (n : ℕ+), f ↑↑n

theorem neg_div_neg_aux (a b : ℂ) : -a / b = a / -b

theorem summable_diff (z : UpperHalfPlane) (d : ℤ) : Summable fun (m : ℕ+) => 1 / (-↑d / ↑z - ↑↑m) + 1 / (-↑d / ↑z + ↑↑m)

theorem arg1 (a b c d e f g h : ℂ) : e / f + g / h - a / b - c / d = e / f + g / h + a / -b + c / -d

theorem sum_int_pnat3 (z : UpperHalfPlane) (d : ℤ) : ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑d) + 1 / (-↑↑m * ↑z + -↑d) - 1 / (↑↑m * ↑z + ↑d) - 1 / (-↑↑m * ↑z + ↑d)) = 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑d / ↑z - ↑↑m) + 1 / (-↑d / ↑z + ↑↑m))

theorem pow_max (x y : ℕ) : max x y ^ 2 = max (x ^ 2) (y ^ 2)

theorem extracted_abs_norm_summable (z : UpperHalfPlane) (i : ℤ) : Summable fun (m : ℤ) => 1 / (EisensteinSeries.r z ^ 2 * 2⁻¹ * ‖![m, i]‖ ^ 2)

theorem aux (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : a⁻¹ ≤ c * b⁻¹ ↔ b ≤ c * a

theorem summable_hammerTime {α : Type} [NormedField α] [CompleteSpace α] (f : ℤ → α) (a : ℝ) (hab : 1 < a) (hf : (fun (n : ℤ) => (f n)⁻¹) =O[Filter.cofinite] fun (n : ℤ) => (|↑n| ^ a)⁻¹) : Summable fun (n : ℤ) => (f n)⁻¹

theorem summable_hammerTime_nat {α : Type} [NormedField α] [CompleteSpace α] (f : ℕ → α) (a : ℝ) (hab : 1 < a) (hf : (fun (n : ℕ) => (f n)⁻¹) =O[Filter.cofinite] fun (n : ℕ) => (|↑n| ^ a)⁻¹) : Summable fun (n : ℕ) => (f n)⁻¹

theorem summable_diff_denom (z : UpperHalfPlane) (i : ℤ) : Summable fun (m : ℤ) => (↑m * ↑z + ↑i + 1)⁻¹ * (↑m * ↑z + ↑i)⁻¹

theorem summable_pain (z : UpperHalfPlane) (i : ℤ) : Summable fun (m : ℤ) => 1 / (↑m * ↑z + ↑i) - 1 / (↑m * ↑z + ↑i + 1)

theorem vector_norm_bound (b : Fin 2 → ℤ) (hb : b ≠ 0) (HB1 : b ≠ ![0, -1]) : ‖![b 0, b 1 + 1]‖ ^ (-1) * ‖b‖ ^ (-2) ≤ 2 * ‖b‖ ^ (-3)

theorem G_2_alt_summable (z : UpperHalfPlane) : Summable fun (m : Fin 2 → ℤ) => 1 / ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1))

def δ (a b : ℤ) : ℂ

Equations

• δ a b = if a = 0 ∧ b = 0 then 1 else if a = 0 ∧ b = -1 then 2 else 0

@[simp]

theorem δ_eq : δ 0 0 = 1

@[simp]

theorem δ_eq2 : δ 0 (-1) = 2

theorem δ_neq (a b : ℤ) (h : a ≠ 0) : δ a b = 0

theorem G_2_alt_summable_δ (z : UpperHalfPlane) : Summable fun (m : Fin 2 → ℤ) => 1 / ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1)) + δ (m 0) (m 1)

theorem G2_prod_summable1 (z : UpperHalfPlane) (b : ℤ) : Summable fun (c : ℤ) => (↑b * ↑z + ↑c + 1)⁻¹ * ((↑b * ↑z + ↑c) ^ 2)⁻¹

theorem G2_prod_summable1_δ (z : UpperHalfPlane) (b : ℤ) : Summable fun (c : ℤ) => (↑b * ↑z + ↑c + 1)⁻¹ * ((↑b * ↑z + ↑c) ^ 2)⁻¹ + δ b c

theorem G2_alt_indexing_δ (z : UpperHalfPlane) : ∑' (m : Fin 2 → ℤ), (1 / ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1)) + δ (m 0) (m 1)) = ∑' (m : ℤ) (n : ℤ), (1 / ((↑m * ↑z + ↑n) ^ 2 * (↑m * ↑z + ↑n + 1)) + δ m n)

theorem G2_alt_indexing2_δ (z : UpperHalfPlane) : ∑' (m : Fin 2 → ℤ), (1 / ((↑(m 0) * ↑z + ↑(m 1)) ^ 2 * (↑(m 0) * ↑z + ↑(m 1) + 1)) + δ (m 0) (m 1)) = ∑' (n : ℤ) (m : ℤ), (1 / ((↑m * ↑z + ↑n) ^ 2 * (↑m * ↑z + ↑n + 1)) + δ m n)

theorem summable_1 (k : ℕ) (z : UpperHalfPlane) (hk : 1 ≤ k) : Summable fun (b : ℕ) => ((↑z - ↑b) ^ (k + 1))⁻¹

theorem summable_2 (k : ℕ) (z : UpperHalfPlane) (hk : 1 ≤ k) : Summable fun (b : ℕ) => ((↑z + ↑b) ^ (k + 1))⁻¹

theorem summable_3 (m : ℕ) (y : ↑{z : ℂ | 0 < z.im}) : Summable fun (n : ℕ+) => (-1) ^ m * ↑m.factorial * (1 / (↑y - ↑↑n) ^ (m + 1)) + (-1) ^ m * ↑m.factorial * (1 / (↑y + ↑↑n) ^ (m + 1))

theorem summable_iter_derv' (k : ℕ) (y : ↑ℍ') : Summable fun (n : ℕ) => (2 * ↑Real.pi * Complex.I * ↑n) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑y)

theorem sigma_eq_sum_div' (k n : ℕ) : (ArithmeticFunction.sigma k) n = ∑ d ∈ n.divisors, (n / d) ^ k

theorem a33 (k : ℕ) (e : ℕ+) (z : UpperHalfPlane) : Summable fun (c : ℕ+) => ↑↑c ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑e * ↑z * ↑↑c)

theorem hsum (k : ℕ) (z : UpperHalfPlane) : Summable fun (b : ℕ+) => ∑ x ∈ (↑b).divisors, ↑↑b ^ k * ‖Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑b)‖

theorem summable_auxil_1 (k : ℕ) (z : UpperHalfPlane) : Summable fun (c : (n : ℕ+) × { x : ℕ × ℕ // x ∈ (↑n).divisorsAntidiagonal }) => ↑(↑c.snd).1 ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑(↑c.snd).1 * ↑(↑c.snd).2)

theorem sum_range_zero (f : ℤ → ℂ) (n : ℕ) : ∑ m ∈ Finset.range (n + 1), f ↑m = f 0 + ∑ m ∈ Finset.range n, f (↑m + 1)

theorem exp_series_ite_deriv_uexp2 (k : ℕ) (x : ↑{z : ℂ | 0 < z.im}) : iteratedDerivWithin k (fun (z : ℂ) => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z)) {z : ℂ | 0 < z.im} ↑x = ∑' (n : ℕ), iteratedDerivWithin k (fun (s : ℂ) => Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * s)) {z : ℂ | 0 < z.im} ↑x

theorem exp_series_ite_deriv_uexp'' (k : ℕ) (x : ↑{z : ℂ | 0 < z.im}) : iteratedDerivWithin k (fun (z : ℂ) => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z)) {z : ℂ | 0 < z.im} ↑x = ∑' (n : ℕ), (2 * ↑Real.pi * Complex.I * ↑n) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x)

theorem exp_series_ite_deriv_uexp''' (k : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z)) ℍ') (fun (x : ℂ) => ∑' (n : ℕ), (2 * ↑Real.pi * Complex.I * ↑n) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * x)) ℍ'

theorem tsum_uexp_contDiffOn (k : ℕ) : ContDiffOn ℂ (↑k) (fun (z : ℂ) => ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z)) ℍ'

theorem iter_der_within_add (k : ℕ+) (x : ↑{z : ℂ | 0 < z.im}) : iteratedDerivWithin (↑k) (fun (z : ℂ) => ↑Real.pi * Complex.I - (2 * ↑Real.pi * Complex.I) • ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z)) {z : ℂ | 0 < z.im} ↑x = -(2 * ↑Real.pi * Complex.I) * ∑' (n : ℕ), (2 * ↑Real.pi * Complex.I * ↑n) ^ ↑k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑x)

theorem iter_exp_eqOn (k : ℕ+) : Set.EqOn (iteratedDerivWithin (↑k) (fun (z : ℂ) => ↑Real.pi * Complex.I - (2 * ↑Real.pi * Complex.I) • ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * z)) {z : ℂ | 0 < z.im}) (fun (x : ℂ) => -(2 * ↑Real.pi * Complex.I) * ∑' (n : ℕ), (2 * ↑Real.pi * Complex.I * ↑n) ^ ↑k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * x)) {z : ℂ | 0 < z.im}

theorem summable_iter_aut (k : ℕ) (z : UpperHalfPlane) : Summable fun (n : ℕ+) => iteratedDerivWithin k (fun (z : ℂ) => 1 / (z - ↑↑n) + 1 / (z + ↑↑n)) {z : ℂ | 0 < z.im} ↑z

theorem sub_bound (s : ↑{z : ℂ | 0 < z.im}) (A B : ℝ) (hB : 0 < B) (hs : s ∈ UpperHalfPlane.verticalStrip A B) (k : ℕ) (n : ℕ+) : ‖(-1) ^ (k + 1) * ↑(k + 1).factorial * (1 / (↑s - ↑↑n) ^ (k + 2))‖ ≤ ‖↑(k + 1).factorial / EisensteinSeries.r ⟨{ re := A, im := B }, hB⟩ ^ (k + 2) * (↑↑n ^ (↑k + 2))⁻¹‖

theorem add_bound (s : ↑{z : ℂ | 0 < z.im}) (A B : ℝ) (hB : 0 < B) (hs : s ∈ UpperHalfPlane.verticalStrip A B) (k : ℕ) (n : ℕ+) : ‖(-1) ^ (k + 1) * ↑(k + 1).factorial * (1 / (↑s + ↑↑n) ^ (k + 2))‖ ≤ ‖↑(k + 1).factorial / EisensteinSeries.r ⟨{ re := A, im := B }, hB⟩ ^ (k + 2) * (↑↑n ^ (↑k + 2))⁻¹‖

theorem aut_bound_on_comp (K : Set ↑{z : ℂ | 0 < z.im}) (hk2 : IsCompact K) (k : ℕ) : ∃ (u : ℕ+ → ℝ), Summable u ∧ ∀ (n : ℕ+) (s : ↑K), ‖derivWithin (fun (z : ℂ) => iteratedDerivWithin k (fun (z : ℂ) => (z - ↑↑n)⁻¹ + (z + ↑↑n)⁻¹) {z : ℂ | 0 < z.im} z) {z : ℂ | 0 < z.im} ↑↑s‖ ≤ u n

theorem diff_on_aux (k : ℕ) (n : ℕ+) : DifferentiableOn ℂ ((fun (t : ℂ) => (-1) ^ k * ↑k.factorial * (1 / (t - ↑↑n) ^ (k + 1))) + fun (t : ℂ) => (-1) ^ k * ↑k.factorial * (1 / (t + ↑↑n) ^ (k + 1))) {z : ℂ | 0 < z.im}

theorem diff_at_aux (s : ↑{z : ℂ | 0 < z.im}) (k : ℕ) (n : ℕ+) : DifferentiableAt ℂ (fun (z : ℂ) => iteratedDerivWithin k (fun (z : ℂ) => (z - ↑↑n)⁻¹ + (z + ↑↑n)⁻¹) {z : ℂ | 0 < z.im} z) ↑s

theorem aut_series_ite_deriv_uexp2 (k : ℕ) (x : UpperHalfPlane) : iteratedDerivWithin k (fun (z : ℂ) => ∑' (n : ℕ+), (1 / (z - ↑↑n) + 1 / (z + ↑↑n))) {z : ℂ | 0 < z.im} ↑x = ∑' (n : ℕ+), iteratedDerivWithin k (fun (z : ℂ) => 1 / (z - ↑↑n) + 1 / (z + ↑↑n)) {z : ℂ | 0 < z.im} ↑x

theorem tsum_ider_der_eq (k : ℕ) (x : ↑{z : ℂ | 0 < z.im}) : ∑' (n : ℕ+), iteratedDerivWithin k (fun (z : ℂ) => 1 / (z - ↑↑n) + 1 / (z + ↑↑n)) {z : ℂ | 0 < z.im} ↑x = ∑' (n : ℕ+), ((-1) ^ k * ↑k.factorial * (1 / (↑x - ↑↑n) ^ (k + 1)) + (-1) ^ k * ↑k.factorial * (1 / (↑x + ↑↑n) ^ (k + 1)))

theorem auxp_series_ite_deriv_uexp''' (k : ℕ) : Set.EqOn (iteratedDerivWithin k (fun (z : ℂ) => ∑' (n : ℕ+), (1 / (z - ↑↑n) + 1 / (z + ↑↑n))) {z : ℂ | 0 < z.im}) (fun (x : ℂ) => ∑' (n : ℕ+), ((-1) ^ k * ↑k.factorial * (1 / (x - ↑↑n) ^ (k + 1)) + (-1) ^ k * ↑k.factorial * (1 / (x + ↑↑n) ^ (k + 1)))) {z : ℂ | 0 < z.im}

theorem tsum_aexp_contDiffOn (k : ℕ) : ContDiffOn ℂ (↑k) (fun (z : ℂ) => ∑' (n : ℕ+), (1 / (z - ↑↑n) + 1 / (z + ↑↑n))) {z : ℂ | 0 < z.im}

theorem aux_iter_der_tsum (k : ℕ) (hk : 1 ≤ k) (x : UpperHalfPlane) : iteratedDerivWithin k ((fun (z : ℂ) => 1 / z) + fun (z : ℂ) => ∑' (n : ℕ+), (1 / (z - ↑↑n) + 1 / (z + ↑↑n))) {z : ℂ | 0 < z.im} ↑x = (-1) ^ k * ↑k.factorial * ∑' (n : ℤ), 1 / (↑x + ↑n) ^ (k + 1)

theorem aux_iter_der_tsum_eqOn (k : ℕ) (hk : 2 ≤ k) : Set.EqOn (iteratedDerivWithin (k - 1) ((fun (z : ℂ) => 1 / z) + fun (z : ℂ) => ∑' (n : ℕ+), (1 / (z - ↑↑n) + 1 / (z + ↑↑n))) {z : ℂ | 0 < z.im}) (fun (z : ℂ) => (-1) ^ (k - 1) * ↑(k - 1).factorial * ∑' (n : ℤ), 1 / (z + ↑n) ^ k) {z : ℂ | 0 < z.im}

theorem pos_sum_eq (k : ℕ) (hk : 0 < k) : (fun (x : ℂ) => -(2 * ↑Real.pi * Complex.I) * ∑' (n : ℕ), (2 * ↑Real.pi * Complex.I * ↑n) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * x)) = fun (x : ℂ) => -(2 * ↑Real.pi * Complex.I) * ∑' (n : ℕ+), (2 * ↑Real.pi * Complex.I * ↑↑n) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * x)

theorem cot_series_repr (z : UpperHalfPlane) : ↑Real.pi * (↑Real.pi * ↑z).cot - 1 / ↑z = ∑' (n : ℕ+), (1 / (↑z - ↑↑n) + 1 / (↑z + ↑↑n))

theorem EisensteinSeries_Identity (z : UpperHalfPlane) : 1 / ↑z + ∑' (n : ℕ+), (1 / (↑z - ↑↑n) + 1 / (↑z + ↑↑n)) = ↑Real.pi * Complex.I - 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n

theorem q_exp_iden'' (k : ℕ) (hk : 2 ≤ k) : Set.EqOn (fun (z : ℂ) => (-1) ^ (k - 1) * ↑(k - 1).factorial * ∑' (d : ℤ), 1 / (z + ↑d) ^ k) (fun (z : ℂ) => -(2 * ↑Real.pi * Complex.I) * ∑' (n : ℕ+), (2 * ↑Real.pi * Complex.I * ↑↑n) ^ (k - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * z)) {z : ℂ | 0 < z.im}

theorem q_exp_iden (k : ℕ) (hk : 2 ≤ k) (z : UpperHalfPlane) : ∑' (d : ℤ), 1 / (↑z + ↑d) ^ k = (-2 * ↑Real.pi * Complex.I) ^ k / ↑(k - 1).factorial * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑n)

theorem tsum_sigma_eqn2 (k : ℕ) (z : UpperHalfPlane) : ∑' (c : Fin 2 → ℕ+), ↑↑(c 0) ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑(c 0) * ↑↑(c 1)) = ∑' (e : ℕ+), ↑((ArithmeticFunction.sigma k) ↑e) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑e)

theorem G2_summable_aux (n : ℤ) (z : UpperHalfPlane) (k : ℤ) (hk : 2 ≤ k) : Summable fun (d : ℤ) => ((↑n * ↑z + ↑d) ^ k)⁻¹

theorem tsum_sigma_eqn {k : ℕ} (z : UpperHalfPlane) : ∑' (c : ℕ+ × ℕ+), ↑↑c.1 ^ k * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑c.1 * ↑↑c.2) = ∑' (e : ℕ+), ↑((ArithmeticFunction.sigma k) ↑e) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑e * ↑z)

theorem exp_aux (z : UpperHalfPlane) (n : ℕ) : Complex.exp (2 * ↑Real.pi * Complex.I * ↑n * ↑z) = Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n

theorem summable_exp_pow (z : UpperHalfPlane) : Summable fun (i : ℕ) => ‖Complex.exp (2 * ↑Real.pi * Complex.I * (↑i + 1) * ↑z)‖

theorem a1 (k : ℕ) (e : ℕ+) (z : UpperHalfPlane) : Summable fun (c : ℕ) => ↑↑e ^ (k - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑↑e * ↑c)

theorem a4 (k : ℕ) (z : UpperHalfPlane) : Summable (Function.uncurry fun (b c : ℕ+) => ↑↑b ^ (k - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑c * ↑z * ↑↑b))

theorem t9 (z : UpperHalfPlane) : ∑' (m : ℕ), 2 * (-2 * ↑Real.pi * Complex.I) ^ 2 / ↑(2 - 1).factorial * ∑' (n : ℕ+), ↑↑n ^ (2 - 1) * Complex.exp (2 * ↑Real.pi * Complex.I * (↑m + 1) * ↑z * ↑↑n) = -8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

theorem summable_pnats (f : ℕ → ℂ) : (Summable fun (n : ℕ+) => f ↑n) ↔ Summable f

theorem auxf (a b c d : ℂ) : a / b - c / d = a / b + c / -d

theorem summable_diff_right_a (z : UpperHalfPlane) (d : ℕ+) : Summable fun (n : ℕ) => 1 / (↑n * ↑z - ↑↑d) - 1 / (↑n * ↑z + ↑↑d)

theorem summable_diff_right (z : UpperHalfPlane) (d : ℕ+) : Summable fun (m : ℤ) => 1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)

theorem sum_int_pnatt (z : UpperHalfPlane) (d : ℕ+) : 2 / ↑↑d + ∑' (m : ℤ), (1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)) = ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d))

theorem sum_int_pnat2_pnat (z : UpperHalfPlane) (d : ℕ+) : ∑' (m : ℤ), (1 / (↑m * ↑z - ↑↑d) - 1 / (↑m * ↑z + ↑↑d)) = -2 / ↑↑d + ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d))