awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z =
    2 * riemannZeta (↑k : ℂ) +
      2 * ((-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ)) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
⊢ 1 < Complex.re (↑k : ℂ)
have norm_cast : 1 < k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z =
    2 * riemannZeta (↑k : ℂ) +
      2 * ((-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ)) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
⊢ HSMul.hSMul (β := ℂ) (1 / 2) (∑' (x : (↑(gammaSet 1 1 0) : Type)), eisSummand (↑k : ℤ) (↑x : Fin 2 → ℤ) z) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
have z2 : riemannZeta (↑k : ℂ) ≠ 0
Tactic: have z2 : riemannZeta k ≠ 0 := riemannZeta_ne_zero_of_one_lt_re <| by norm_cast; grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
HE1 :
  ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z =
    2 * riemannZeta (↑k : ℂ) +
      2 * ((-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ)) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
HE2 : ∑' (v : Fin 2 → ℤ), eisSummand (↑k : ℤ) v z = riemannZeta (↑k : ℂ) * eisensteinSeries (N := 1) 0 (↑k : ℤ) z
z2 : riemannZeta (↑k : ℂ) ≠ 0
⊢ HSMul.hSMul (β := ℂ) (1 / 2) (∑' (x : (↑(gammaSet 1 1 0) : Type)), eisSummand (↑k : ℤ) (↑x : Fin 2 → ℤ) z) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
have simp : ∀
  (HE1 :
    ∑' (v : Fin 2 → ℤ), (((↑(v 0) : ℂ) * (↑z : ℂ) + (↑(v 1) : ℂ)) ^ k)⁻¹ =
      2 * riemannZeta (↑k : ℂ) +
        2 * ((-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ)) *
          ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))
  (HE2 :
    (riemannZeta (↑k : ℂ))⁻¹ * ∑' (v : Fin 2 → ℤ), (((↑(v 0) : ℂ) * (↑z : ℂ) + (↑(v 1) : ℂ)) ^ k)⁻¹ =
      ∑' (x : (↑(gammaSet 1 1 0) : Type)),
        (((↑((↑x : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑x : Fin 2 → ℤ) 1) : ℂ)) ^ k)⁻¹),
  HMul.hMul (α := ℂ) 2⁻¹
      (∑' (x : (↑(gammaSet 1 1 0) : Type)),
        (((↑((↑x : Fin 2 → ℤ) 0) : ℂ) * (↑z : ℂ) + (↑((↑x : Fin 2 → ℤ) 1) : ℂ)) ^ k)⁻¹) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-(2 * (↑π : ℂ) * I)) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ)
Tactic: simp [eisSummand, eisensteinSeries, ← inv_mul_eq_iff_eq_mul₀ z2] at HE1 HE2 ⊢
Cleared hypotheses: HE1, HE2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
⊢ (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) =
    -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
have h2 : k = 2 * (k / 2 - 1 + 1)
Tactic: have h2 : k = 2 * (k / 2 - 1 + 1) := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) =
    -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
have rw : (HPow.hPow (α := ℂ) (-1) (m + 1 + 1) * HPow.hPow (α := ℂ) 2 (2 * m + 1) * (↑π : ℂ) ^ (2 * (m + 1)) *
            (↑(bernoulli (2 * (m + 1))) : ℂ) /
          (↑(2 * (m + 1) * (2 * m + 1)!) : ℂ))⁻¹ *
      (HPow.hPow (α := ℂ) (-2) (2 * (m + 1)) * (↑π : ℂ) ^ (2 * (m + 1)) * HPow.hPow (α := ℂ) (-1) (m + 1)) /
    (↑(2 * m + 1)! : ℂ) =
  -(2 * HMul.hMul (α := ℂ) 2 (↑(m + 1) : ℂ) / (↑(bernoulli (2 * (m + 1))) : ℂ))
Tactic: rw [h2, Nat.cast_mul 2 (m + 1), Nat.cast_two, riemannZeta_two_mul_nat (show m + 1 ≠ 0 by grind),
    show (2 * (m + 1))! = 2 * (m + 1) * (2 * m + 1)! by grind [Nat.factorial_succ],
    show 2 * (m + 1) - 1 = 2 * m + 1 by grind, mul_pow, mul_pow, pow_mul I, I_sq]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ (HPow.hPow (α := ℂ) (-1) (m + 1 + 1) * HPow.hPow (α := ℂ) 2 (2 * m + 1) * (↑π : ℂ) ^ (2 * (m + 1)) *
              (↑(bernoulli (2 * (m + 1))) : ℂ) /
            (↑(2 * (m + 1) * (2 * m + 1)!) : ℂ))⁻¹ *
        (HPow.hPow (α := ℂ) (-2) (2 * (m + 1)) * (↑π : ℂ) ^ (2 * (m + 1)) * HPow.hPow (α := ℂ) (-1) (m + 1)) /
      (↑(2 * m + 1)! : ℂ) =
    -(2 * HMul.hMul (α := ℂ) 2 (↑(m + 1) : ℂ) / (↑(bernoulli (2 * (m + 1))) : ℂ))
have norm_cast : ((↑(Int.negSucc 0 ^ (m + 1 + 1) * (↑(HPow.hPow (α := ℕ) 2 (2 * m + 1)) : ℤ)) : ℝ) * π ^ (2 * (m + 1)) *
            (↑(bernoulli (2 * (m + 1))) : ℝ) /
          (↑(2 * (m + 1) * (2 * m + 1)!) : ℝ))⁻¹ *
      ((↑(Int.negSucc 1 ^ (2 * (m + 1))) : ℝ) * π ^ (2 * (m + 1)) * (↑(Int.negSucc 0 ^ (m + 1)) : ℝ)) /
    (↑(2 * m + 1)! : ℝ) =
  (↑(-((↑(2 * (2 * (m + 1))) : ℚ) / bernoulli (2 * (m + 1)))) : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
m : ℕ := k / 2 - 1
h2 : k = 2 * (m + 1)
⊢ ((↑(Int.negSucc 0 ^ (m + 1 + 1) * (↑(HPow.hPow (α := ℕ) 2 (2 * m + 1)) : ℤ)) : ℝ) * π ^ (2 * (m + 1)) *
              (↑(bernoulli (2 * (m + 1))) : ℝ) /
            (↑(2 * (m + 1) * (2 * m + 1)!) : ℝ))⁻¹ *
        ((↑(Int.negSucc 1 ^ (2 * (m + 1))) : ℝ) * π ^ (2 * (m + 1)) * (↑(Int.negSucc 0 ^ (m + 1)) : ℝ)) /
      (↑(2 * m + 1)! : ℝ) =
    (↑(-((↑(2 * (2 * (m + 1))) : ℚ) / bernoulli (2 * (m + 1)))) : ℝ)
have simp : HPow.hPow (α := ℝ) 2 (2 * (m + 1)) * HPow.hPow (α := ℝ) (-1) (m + 1) / (↑(bernoulli (2 * (m + 1))) : ℝ) =
  -(2 * HPow.hPow (α := ℝ) (-1) (m + 1 + 1) * HPow.hPow (α := ℝ) 2 (2 * m + 1) / (↑(bernoulli (2 * (m + 1))) : ℝ))
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ (E hk : (a : ℍ) → ℂ) z =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
have h : 1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
  1 +
    (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
Tactic: convert! q_expansion_riemannZeta hk hk2 z using 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
⊢ 1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
have h : 1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
  1 +
    -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ)) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
Tactic: rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
h :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ)) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
⊢ 1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
have h₁ : 1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
  1 +
    -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ))
Tactic: rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
h :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ)) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
h₁ :
  1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
          ∑' (n : ℕ+),
            (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
              HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ))
⊢ 1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
    1 +
      (riemannZeta (↑k : ℂ))⁻¹ * (-2 * (↑π : ℂ) * I) ^ k / (↑(k - 1)! : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
have h₂ : 1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ) =
  1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))) (↑(↑n : ℕ) : ℤ)
Tactic: rw [eisensteinSeries_coeff_identity hk2 (by grind), neg_mul, ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦ (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n
have apply : ∀ (i : ℕ),
  ‖(↑((σ (k - 1) : (a : ℕ) → ℕ) i) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i‖ ≤
    ‖HPow.hPow (α := ℂ) (↑i : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ i‖
Tactic: apply Summable.of_norm_bounded
    (summable_norm_pow_mul_geometric_of_norm_lt_one k (norm_exp_two_pi_I_lt_one z))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ ‖(↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n‖ ≤
    ‖HPow.hPow (α := ℂ) (↑n : ℂ) k * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ n‖
have simp : (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n ≤
  HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n
Tactic: simp only [norm_mul, Complex.norm_natCast, norm_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n ≤
    HPow.hPow (α := ℝ) (↑n : ℝ) k * ‖cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))‖ ^ n
have hbc : (↑((σ (k - 1) : (a : ℕ) → ℕ) n) : ℝ) ≤ HPow.hPow (α := ℝ) (↑n : ℝ) k
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 1 ≤ k
z : ℍ
n : ℕ
⊢ n ^ (k - 1 + 1) = n ^ k
have e_a : k - 1 + 1 = k
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
⊢ (PowerSeries.coeff m : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑(E hk) : (a : ℍ) → ℂ)) =
    if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
have suffices : ∀ (τ : ℍ), HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 1 (↑τ : ℂ) ^ m) ((E hk : (a : ℍ) → ℂ) τ : ℂ)
Tactic: suffices ∀ τ : ℍ, HasSum (fun m ↦ c m • 𝕢 (1 : ℝ) τ ^ m) (E hk τ) from
    (ModularFormClass.qExpansion_coeff_unique one_pos one_mem_strictPeriods_SL this m).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
⊢ HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 1 (↑τ : ℂ) ^ m) ((E hk : (a : ℍ) → ℂ) τ : ℂ)
have hS : Summable (α := ℂ) fun (n : ℕ) ↦
  (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
Tactic: have hS : Summable fun n : ℕ ↦ (σ (k - 1) (n + 1) : ℂ) * cexp (2 * π * I * τ) ^ (n + 1) :=
    (summable_nat_add_iff 1).mpr (summable_sigma_mul_cexp_pow (by omega) τ)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ HasSum (α := ℂ) (fun (m : ℕ) ↦ c m • 𝕢 1 (↑τ : ℂ) ^ m) ((E hk : (a : ℍ) → ℂ) τ : ℂ)
have rw : HasSum (fun (n : ℕ) ↦ c (n + 1) • 𝕢 1 (↑τ : ℂ) ^ (n + 1))
  (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (∑ i ∈ Finset.range 1, c i • 𝕢 1 (↑τ : ℂ) ^ i : ℂ))
Tactic: rw [← hasSum_nat_add_iff' 1]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ HasSum (fun (n : ℕ) ↦ c (n + 1) • 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (∑ i ∈ Finset.range 1, c i • 𝕢 1 (↑τ : ℂ) ^ i : ℂ))
have simp : HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
  (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ))
Tactic: simp only [Nat.add_eq_zero_iff, one_ne_zero, and_false, ↓reduceIte, smul_eq_mul, Finset.range_one,
    ite_mul, one_mul, Finset.sum_singleton, pow_zero, c]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
have this : (E hk : (a : ℍ) → ℂ) τ =
  1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+),
        (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
          HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ))) (↑(↑n : ℕ) : ℤ)
Tactic: have := q_expansion_bernoulli hk hk2 τ
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
this :
  (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+),
          (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) *
            HPow.hPow (β := ℤ) (cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ))) (↑(↑n : ℕ) : ℤ)
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
have this₁ : (E hk : (a : ℍ) → ℂ) τ =
  1 -
    HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
      ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)
Tactic: simp_rw [zpow_natCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
this :
  (E hk : (a : ℍ) → ℂ) τ =
    1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)
⊢ HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
have rw : 1 -
      HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ) *
        ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ) -
    1 =
  β * ∑' (n : ℕ+), (↑((σ (k - 1) : (a : ℕ) → ℕ) (↑n : ℕ)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (↑n : ℕ)
Tactic: rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ))
have hval : HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
  β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
Tactic: have hval : E hk τ - 1 = β * ∑' n : ℕ, (σ (k - 1) (n + 1)) * cexp (2 * π * I * τ) ^ (n + 1) := by
    have := q_expansion_bernoulli hk hk2 τ
    simp_rw [zpow_natCast] at this
    rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]
    ring
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
hval :
  HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ))
have rw : HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
  (β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))
Tactic: rw [hval]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(HMul.hMul (α := ℂ) 2 (↑k : ℂ) / (↑(bernoulli k) : ℂ))
c : ℕ → ℂ := fun (m : ℕ) ↦ if m = 0 then 1 else β * (↑((σ (k - 1) : (a : ℕ) → ℕ) m) : ℂ)
τ : ℍ
hS :
  Summable (α := ℂ) fun (n : ℕ) ↦
    (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
hval :
  HSub.hSub (α := ℂ) (β := ℂ) ((E hk : (a : ℍ) → ℂ) τ : ℂ) (1 : ℂ) =
    β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1)
⊢ HasSum (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1))
    (β * ∑' (n : ℕ), (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (n + 1))
have h : Eq (α := ℕ → ℂ) (fun (n : ℕ) ↦ β * (↑((σ (k - 1) : (a : ℕ) → ℕ) (n + 1)) : ℂ) * 𝕢 1 (↑τ : ℂ) ^ (n + 1)) fun (i : ℕ) ↦
  β * ((↑((σ (k - 1) : (a : ℕ) → ℕ) (i + 1)) : ℂ) * cexp (2 * (↑π : ℂ) * I * (↑τ : ℂ)) ^ (i + 1))
Tactic: convert! (hS.mul_left β).hasSum using 1