Cauchylems

theorem cc (f : ℤ → ℂ) (hc : CauchySeq fun (N : ℕ) => ∑ m ∈ Finset.Icc (-↑N) ↑N, f m) (hs : ∀ (n : ℤ), f n = f (-n)) : Filter.Tendsto f Filter.atTop (nhds 0)

theorem sum_Icc_eq_sum_Ico_succ {α : Type u_1} [AddCommMonoid α] (f : ℤ → α) {l u : ℤ} (h : l ≤ u) : ∑ m ∈ Finset.Icc l u, f m = ∑ m ∈ Finset.Ico l u, f m + f u

theorem CauchySeq_Icc_iff_CauchySeq_Ico (f : ℤ → ℂ) (hs : ∀ (n : ℤ), f n = f (-n)) (hc : CauchySeq fun (N : ℕ) => ∑ m ∈ Finset.Icc (-↑N) ↑N, f m) : CauchySeq fun (N : ℕ) => ∑ m ∈ Finset.Ico (-↑N) ↑N, f m

theorem extracted_2 (z : UpperHalfPlane) (b : ℤ) : CauchySeq fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, 1 / ((↑b * ↑z + ↑n) ^ 2 * (↑b * ↑z + ↑n + 1))

theorem extracted_2_δ (z : UpperHalfPlane) (b : ℤ) : CauchySeq fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, (1 / ((↑b * ↑z + ↑n) ^ 2 * (↑b * ↑z + ↑n + 1)) + δ b n)

theorem telescope_aux (z : UpperHalfPlane) (m : ℤ) (b : ℕ) : ∑ n ∈ Finset.Ico (-↑b) ↑b, (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) = 1 / (↑m * ↑z - ↑b) - 1 / (↑m * ↑z + ↑b)

theorem extracted_3 (z : UpperHalfPlane) (b : ℤ) : CauchySeq fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))

theorem extracted_4 (z : UpperHalfPlane) (b : ℤ) : CauchySeq fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, 1 / (↑b * ↑z + ↑n) ^ 2

theorem extracted_5 (z : UpperHalfPlane) (b : ℤ) : CauchySeq fun (N : ℕ) => ∑ n ∈ Finset.Ico (-↑N) ↑N, 1 / (↑b * ↑z - ↑n) ^ 2

theorem CauchySeq.congr (f g : ℕ → ℂ) (hf : f = g) (hh : CauchySeq g) : CauchySeq f

theorem cauchy_seq_mul_const (f : ℕ → ℂ) (c : ℂ) (hc : c ≠ 0) : CauchySeq f → CauchySeq (c • f)

theorem auxer (a c : ℂ) : a + 2 * 2 * c - 2 * c = a + 2 * c

noncomputable def summableTerm (z : UpperHalfPlane) : ℤ → ℂ

The summand appearing in the Eisenstein-type series used in the Cauchy lemmas.

Equations

• summableTerm z m = ∑' (n : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2

theorem term_evem (z : UpperHalfPlane) (m : ℤ) : summableTerm z m = summableTerm z (-m)

theorem t8 (z : UpperHalfPlane) : (fun (N : ℕ) => ∑ m ∈ Finset.Icc (-↑N) ↑N, ∑' (n : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) = (fun (x : ℕ) => 2 * riemannZeta 2) + fun (N : ℕ) => ∑ m ∈ Finset.range N, 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)

theorem G2_c_tendsto (z : UpperHalfPlane) : Filter.Tendsto (fun (N : ℕ) => ∑ x ∈ Finset.range N, 2 * (2 * ↑Real.pi * Complex.I) ^ 2 * ∑' (n : ℕ+), ↑↑n * Complex.exp (2 * ↑Real.pi * Complex.I * (↑x + 1) * ↑z * ↑↑n)) Filter.atTop (nhds (-8 * ↑Real.pi ^ 2 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)))

theorem G2_cauchy (z : UpperHalfPlane) : CauchySeq fun (N : ℕ) => ∑ m ∈ Finset.Icc (-↑N) ↑N, ∑' (n : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2