awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
⊢ LE.le (α := ℕ) 1 1

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑a : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
⊢ 0 < (HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ)).im

Tactic:
simpa [show 0 < ((a + 1) : ℝ) by positivity] using z.2

Premises used: UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
⊢ ∑' (n : ℤ),
      1 /
        ((↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) + (↑n : ℂ)) ^
          HAdd.hAdd (α := ℕ) 1 1 =
    (-2 * (↑π : ℂ) * I) ^ HAdd.hAdd (α := ℕ) 1 1 / (↑1! : ℂ) *
      ∑' (n : ℕ+),
        HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℕ) : ℂ) 1 *
          cexp (2 * (↑π : ℂ) * I * (↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
            (↑n : ℕ)

Tactic:
have H2 := qExpansion_identity_pnat (k := 1) (by grind)
    ⟨(a + 1) * z, by simpa [show 0 < ((a + 1) : ℝ) by positivity] using z.2⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ),
      1 /
        ((↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ) + (↑n : ℂ)) ^
          HAdd.hAdd (α := ℕ) 1 1 =
    (-2 * (↑π : ℂ) * I) ^ HAdd.hAdd (α := ℕ) 1 1 / (↑1! : ℂ) *
      ∑' (n : ℕ+),
        HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℕ) : ℂ) 1 *
          cexp (2 * (↑π : ℂ) * I * (↑{ coe := HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (↑z : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)) ^
            (↑n : ℕ)
⊢ ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)

Tactic:
simp only [add_comm, Nat.reduceAdd, one_div, mul_comm, mul_neg, even_two,
    Even.neg_pow, Nat.factorial_one, Nat.cast_one, div_one, pow_one] at H2

Premises used: even_two, Even.neg_pow, Nat.reduceAdd, add_comm, pow_one, one_div, mul_comm, div_one, Nat.cast_one, mul_neg, Nat.factorial_one
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
e_a :
  Eq (α := ℂ)
    (∑' (x : ℕ+),
      2 *
        (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
          (cexp ((↑x : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑x : ℕ) : ℂ))))
    (∑' (b : ℕ+),
      -(8 *
          (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
              (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ))))))
⊢ HMul.hMul (α := ℂ) 2 (∑' (n : ℤ), (HPow.hPow (β := ℤ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+),
            cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (↑n : ℕ) *
              (cexp ((↑z : ℂ) * (I * (↑π : ℂ)) * 2) ^ (a * (↑n : ℕ)) * (↑(↑n : ℕ) : ℂ))))

Tactic:
simp_rw [zpow_ofNat, H2, ← tsum_mul_left, ← tsum_neg, ← exp_nsmul]

Premises used: Complex.exp_nsmul, tsum_mul_left, zpow_ofNat, tsum_neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
⊢ Eq (α := ℂ)
    (∑' (x : ℕ+),
      2 *
        (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
          (cexp ((↑x : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑x : ℕ) : ℂ))))
    (∑' (b : ℕ+),
      -(8 *
          (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
              (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ))))))

Tactic:
tsum_congr fun b ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
e_a :
  ∀ (b : ℕ+),
    2 *
        (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
          (cexp ((↑b : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑b : ℕ) : ℂ))) =
      -(8 *
          (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
              (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ)))))
⊢ Eq (α := ℂ)
    (∑' (x : ℕ+),
      2 *
        (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
          (cexp ((↑x : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑x : ℕ) : ℂ))))
    (∑' (b : ℕ+),
      -(8 *
          (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
              (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ))))))

Tactic:
refine tsum_congr fun b ↦ ?_

Premises used: tsum_congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
b : ℕ+
e_a :
  HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑(↑b : ℕ) : ℂ) *
        cexp
          (I * (↑π : ℂ) * (↑z : ℂ) * (↑a : ℂ) * (↑(↑b : ℕ) : ℂ) * 2 + I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * 2) *
      8 =
    -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑(↑b : ℕ) : ℂ) * cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * 2) *
          cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * (↑a : ℂ) * 2) *
        8)
⊢ 2 *
      (HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
        (cexp ((↑b : ℕ) • ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2)))) * (↑(↑b : ℕ) : ℂ))) =
    -(8 *
        (HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          (cexp ((↑b : ℕ) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) *
            (cexp ((a * (↑b : ℕ)) • ((↑z : ℂ) * (I * (↑π : ℂ)) * 2)) * (↑(↑b : ℕ) : ℂ)))))

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), (HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1) 2)⁻¹ =
    HPow.hPow (β := ℕ) (I * ((↑π : ℂ) * 2)) 2 *
      ∑' (n : ℕ+), cexp ((↑z : ℂ) * HAdd.hAdd (α := ℂ) (↑a : ℂ) 1 * (I * ((↑π : ℂ) * 2))) ^ (↑n : ℕ) * (↑(↑n : ℕ) : ℂ)
b : ℕ+
⊢ HPow.hPow (β := ℕ) I 2 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑(↑b : ℕ) : ℂ) *
        cexp
          (I * (↑π : ℂ) * (↑z : ℂ) * (↑a : ℂ) * (↑(↑b : ℕ) : ℂ) * 2 + I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * 2) *
      8 =
    -(HPow.hPow (β := ℕ) (↑π : ℂ) 2 * (↑(↑b : ℕ) : ℂ) * cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * 2) *
          cexp (I * (↑π : ℂ) * (↑z : ℂ) * (↑(↑b : ℕ) : ℂ) * (↑a : ℂ) * 2) *
        8)

Tactic:
grind [I_sq, exp_add]

Premises used: Complex.exp_add, Complex.I_sq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Eq (α := ℂ)
    (∑' (d : ℕ+) (c : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))

Tactic:
have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  Eq (α := ℂ)
    (∑' (d : ℕ+) (c : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑d : ℕ) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))
⊢ Eq (α := ℂ)
    (∑' (n : ℕ) (c : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((n + 1) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))

Tactic:
rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this

Premises used: tsum_pnat_eq_tsum_succ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  Eq (α := ℂ)
    (∑' (n : ℕ) (c : ℕ+),
      HPow.hPow (α := ℂ) (β := ℕ) (↑(↑c : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((n + 1) * (↑c : ℕ)))
    (∑' (e : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑e : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑e : ℕ))
⊢ -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))

Tactic:
simp [← tsum_mul_left, ← this]

Premises used: tsum_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))

Tactic:
have : -8 * π ^ 2 * ∑' n : ℕ+, σ 1 n * 𝕢 z ^ (n : ℕ) =
      ∑' m : ℕ, (-8 * π ^ 2 * ∑' n : ℕ+, n * 𝕢 z ^ ((m + 1) * n)) := by
    have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)
    rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this
    simp [← tsum_mul_left, ← this]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
rw :
  Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (∑' (m : ℕ),
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))))
⊢ Tendsto
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (-8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)))

Tactic:
rw [this]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (∑' (m : ℕ),
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))))

Tactic:
(Summable.mul_left _ ?_).hasSum.comp tendsto_finset_range

Premises used: Multiset.sum, Multiset.foldr, Filter.tendsto_finset_range, Summable.mul_left, Summable.hasSum, Filter.Tendsto.comp, Finset.sum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
refine :
  Summable (α := ℂ) fun (m : ℕ) ↦
    ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ Tendsto (β := ℂ)
    (fun (N : ℕ) ↦
      ∑ m ∈ range N,
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ)))
    atTop
    (𝓝
      (∑' (m : ℕ),
        -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))))

Tactic:
refine (Summable.mul_left _ ?_).hasSum.comp tendsto_finset_range

Premises used: Filter.tendsto_finset_range, Summable.mul_left, Summable.hasSum, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
rw :
  Summable (α := ℂ) fun (x : ℕ+) ↦
    ∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑x : ℕ) * (↑c : ℕ))
⊢ Summable (α := ℂ) fun (m : ℕ) ↦
    ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))

Tactic:
rw [← summable_pnat_iff_summable_succ (f := fun b ↦ ∑' c : ℕ+, c * 𝕢 z ^ (b * c : ℕ))]

Premises used: summable_pnat_iff_summable_succ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
apply :
  ∀ (b : ℕ+),
    Eq (α := ℂ)
      (∑' (c : ℕ+),
        HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(b, c).2 : ℕ) : ℂ) 1 *
          cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑(b, c).1 : ℕ) * (↑(b, c).2 : ℕ)))
      (∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑b : ℕ) * (↑c : ℕ)))
⊢ Summable (α := ℂ) fun (x : ℕ+) ↦
    ∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑x : ℕ) * (↑c : ℕ))

Tactic:
apply (summable_prod_mul_pow 1 (norm_exp_two_pi_I_lt_one z)).prod.congr

Premises used: UpperHalfPlane.norm_exp_two_pi_I_lt_one, summable_prod_mul_pow, Summable.prod, Summable.congr, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
this :
  -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
      ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) =
    ∑' (m : ℕ),
      -8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑(↑n : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((m + 1) * (↑n : ℕ))
⊢ ∀ (b : ℕ+),
    Eq (α := ℂ)
      (∑' (c : ℕ+),
        HPow.hPow (α := ℂ) (β := ℕ) (↑(↑(b, c).2 : ℕ) : ℂ) 1 *
          cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑(b, c).1 : ℕ) * (↑(b, c).2 : ℕ)))
      (∑' (c : ℕ+), (↑(↑c : ℕ) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ ((↑b : ℕ) * (↑c : ℕ)))

Tactic:
simp [← exp_nsmul]

Premises used: Complex.exp_nsmul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ HasSum (fun (x : ℤ) ↦ e2Summand x z)
    (2 * riemannZeta 2 -
      8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
    (symmetricIcc ℤ)

Tactic:
simpa [HasSum, -symmetricIcc_filter, symmetricIcc_eq_map_Icc_nat, Function.comp_def,
    G2_partial_sum_eq] using (aux_G2_tendsto z).const_add _

Premises used: _private.0.EisensteinSeries.G2_partial_sum_eq, Function.comp_def, HasSum, SummationFilter.symmetricIcc_filter, _private.0.EisensteinSeries.aux_G2_tendsto, Filter.Tendsto.const_add, SummationFilter.symmetricIcc_eq_map_Icc_nat, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Summable (α := ℂ) (fun (x : ℤ) ↦ e2Summand x z) (symmetricIcc ℤ)

Tactic:
(hasSum_e2Summand_symmetricIcc z).summable

Premises used: EisensteinSeries.hasSum_e2Summand_symmetricIcc, HasSum.summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ G2 z =
    2 * riemannZeta 2 -
      8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)

Tactic:
(hasSum_e2Summand_symmetricIcc z).tsum_eq

Premises used: EisensteinSeries.hasSum_e2Summand_symmetricIcc, EisensteinSeries.G2, HasSum.tsum_eq
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
simp :
  6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
      (2 * (HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6) -
        8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)) =
    1 -
      HMul.hMul (α := ℂ) 24
        (∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
⊢ E2 z =
    1 -
      HMul.hMul (α := ℂ) 24
        (∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))

Tactic:
simp [E2, G2_eq_tsum_cexp, riemannZeta_two]

Premises used: riemannZeta_two, EisensteinSeries.G2_eq_tsum_cexp, EisensteinSeries.E2
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ 6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
      (2 * (HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6) -
        8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
          ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)) =
    1 -
      HMul.hMul (α := ℂ) 24
        (∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))

Tactic:
field
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Tendsto (β := ℂ) (fun (x : ℤ) ↦ e2Summand x z) atTop (𝓝 0)

Tactic:
(summable_e2Summand_symmetricIcc z).tendsto_zero_of_even_summable_symmetricIcc (e2Summand_even _)

Premises used: EisensteinSeries.e2Summand_even, EisensteinSeries.summable_e2Summand_symmetricIcc, Summable.tendsto_zero_of_even_summable_symmetricIcc
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
apply : Tendsto (β := ℂ) (fun (N : ℕ) ↦ -e2Summand (↑N : ℤ) z) atTop (𝓝 0)
⊢ HasSum (fun (x : ℤ) ↦ e2Summand x z)
    (2 * riemannZeta 2 -
      8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
        ∑' (n : ℕ+), (↑((σ 1 : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
    (symmetricIco ℤ)

Tactic:
apply (hasSum_e2Summand_symmetricIcc z).hasSum_symmetricIco_of_hasSum_symmetricIcc

Premises used: EisensteinSeries.hasSum_e2Summand_symmetricIcc, HasSum.hasSum_symmetricIco_of_hasSum_symmetricIcc
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Tendsto (β := ℂ) (fun (N : ℕ) ↦ -e2Summand (↑N : ℤ) z) atTop (𝓝 0)

Tactic:
simpa using (tendsto_e2Summand_atTop_nhds_zero z).neg.comp tendsto_natCast_atTop_atTop

Premises used: Filter.Tendsto.neg, EisensteinSeries.tendsto_e2Summand_atTop_nhds_zero, tendsto_natCast_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
⊢ Summable (α := ℂ) (fun (x : ℤ) ↦ e2Summand x z) (symmetricIco ℤ)

Tactic:
(hasSum_e2Summand_symmetricIco z).summable

Premises used: EisensteinSeries.hasSum_e2Summand_symmetricIco, HasSum.summable
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
rw : Tendsto (β := ℂ) (fun (N : ℕ) ↦ -e2Summand (↑N : ℤ) z) atTop (𝓝 0)
⊢ G2 z = ∑'[symmetricIco ℤ] (m : ℤ), e2Summand m z

Tactic:
rw [G2, tsum_symmetricIcc_eq_tsum_symmetricIco (summable_e2Summand_symmetricIcc z)]

Premises used: SummationFilter.tsum_symmetricIcc_eq_tsum_symmetricIco, EisensteinSeries.G2, EisensteinSeries.summable_e2Summand_symmetricIcc
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
rw :
  1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) - ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ))) *
      (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))
ha : (↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ) ≠ 0
hb : (↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) ≠ 0
⊢ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) - 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ)) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))

Tactic:
rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div]

Premises used: one_div_mul_sub_mul_one_div_eq_one_div_add_one_div
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) - ((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ))) *
      (1 / ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))) =
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (1 / (((↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ))))

Tactic:
grind [one_div, add_sub_add_left_eq_sub, mul_inv_rev]

Premises used: add_sub_add_left_eq_sub, one_div, mul_inv_rev
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ Ne (α := Fin 2 → ℝ) ![(↑m : ℝ), (↑a : ℝ)] 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ (↑m : ℂ) * (↑z : ℂ) + (↑a : ℂ) ≠ 0

Tactic:
simpa using linear_ne_zero z (cd := ![m, a]) (by aesop)

Premises used: UpperHalfPlane.linear_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ Ne (α := Fin 2 → ℝ) ![(↑m : ℝ), (↑b : ℝ)] 0

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ (↑m : ℂ) * (↑z : ℂ) + (↑b : ℂ) ≠ 0

Tactic:
simpa using linear_ne_zero z (cd := ![m, b]) (by aesop)

Premises used: UpperHalfPlane.linear_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
Goal:
z : ℍ
a b : ℤ
⊢ Summable (α := ℂ) fun (i : ℤ) ↦
    HSub.hSub (α := ℂ) (↑b : ℂ) (↑a : ℂ) * (((↑i : ℂ) * (↑z : ℂ) + (↑a : ℂ)) * ((↑i : ℂ) * (↑z : ℂ) + (↑b : ℂ)))⁻¹

Tactic:
have := Summable.mul_left (b - a : ℂ) (summable_linear_left_mul_linear_left (ne_zero z) a b)