awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
rw :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) * (↑z : ℂ) / (↑‖x‖ : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
⊢ (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
have rw₁ : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) / (↑‖x‖ : ℂ) * (↑‖x‖ : ℂ)
Tactic: rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
rw :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) * (↑z : ℂ) / (↑‖x‖ : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
rw₁ : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = ((↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)) / (↑‖x‖ : ℂ) * (↑‖x‖ : ℂ)
⊢ (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
have rw₂ : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
Tactic: rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
⊢ r z * ‖x‖ ≤ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖
have h11 : (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) = ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
Tactic: have h11 : x 0 * (z : ℂ) + x 1 = (x 0 / ‖x‖ * z + x 1 / ‖x‖) * ‖x‖ := by
    rw [div_mul_eq_mul_div, ← add_div, div_mul_cancel₀ _ (mod_cast hn0)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
⊢ r z * ‖x‖ ≤ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖
have rw : r z * (↑(max (x 0).natAbs (x 1).natAbs) : ℝ) ≤
  ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖ *
    (↑(max (x 0).natAbs (x 1).natAbs) : ℝ)
Tactic: rw [norm_eq_max_natAbs, h11, norm_mul, norm_real, norm_norm, norm_eq_max_natAbs]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
⊢ r z * (↑(max (x 0).natAbs (x 1).natAbs) : ℝ) ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
          (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖ *
      (↑(max (x 0).natAbs (x 1).natAbs) : ℝ)
have hbc : r z ≤
  ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
      (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
⊢ r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
have hbc : ∀ (H1 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2),
  r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
Tactic: rcases div_max_sq_ge_one x hx with H1 | H2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
x : Fin 2 → ℤ
hx : x ≠ 0
hn0 : ‖x‖ ≠ 0
h11 :
  (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) =
    ((↑(x 0) : ℂ) / (↑‖x‖ : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) / (↑‖x‖ : ℂ)) * (↑‖x‖ : ℂ)
hbc :
  ∀ (H1 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 0) : ℝ) / ‖x‖) 2),
    r z ≤
      ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
          (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
⊢ r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
have hbc₁ : ∀ (H2 : 1 ≤ HPow.hPow (β := ℕ) ((↑(x 1) : ℝ) / ‖x‖) 2),
  r z ≤
    ‖(↑(x 0) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ) * (↑z : ℂ) +
        (↑(x 1) : ℂ) / (↑(↑(max (x 0).natAbs (x 1).natAbs) : ℝ) : ℂ)‖
Tactic: rcases div_max_sq_ge_one x hx with H1 | H2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
have pos : ∀ (hx : x = 0), ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
pos : ∀ (hx : x = 0), ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
have neg : ∀ (hx : ¬x = 0), ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
have pos : HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
Tactic: simp only [hx, Pi.zero_apply, Int.cast_zero, zero_mul, add_zero, norm_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have pos : ∀ (h : -k = 0), HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
Tactic: by_cases h : -k = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
pos : ∀ (h : -k = 0), HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have neg : ∀ (h : ¬-k = 0), HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
Tactic: by_cases h : -k = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have pos : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (β := ℝ) (r z) 0 * HPow.hPow (α := ℝ) (β := ℝ) 0 0
Tactic: rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
pos : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (β := ℝ) (r z) 0 * HPow.hPow (α := ℝ) (β := ℝ) 0 0
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have pos₁ : 1 ≤ HPow.hPow (β := ℝ) (r z) 0 * 1
Tactic: rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
pos : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (β := ℝ) (r z) 0 * HPow.hPow (α := ℝ) (β := ℝ) 0 0
pos₁ : 1 ≤ HPow.hPow (β := ℝ) (r z) 0 * 1
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have pos₂ : 1 ≤ HMul.hMul (α := ℝ) 1 1
Tactic: rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : -k = 0
pos : HPow.hPow (α := ℝ) (β := ℝ) 0 0 ≤ HPow.hPow (β := ℝ) (r z) 0 * HPow.hPow (α := ℝ) (β := ℝ) 0 0
pos₁ : 1 ≤ HPow.hPow (β := ℝ) (r z) 0 * 1
pos₂ : 1 ≤ HMul.hMul (α := ℝ) 1 1
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have pos₃ : LE.le (α := ℝ) 1 1
Tactic: rw [h, Real.rpow_zero, Real.rpow_zero, one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have neg : 0 ≤ r z ^ (-k) * 0
Tactic: rw [Real.zero_rpow h, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : x = 0
h : ¬-k = 0
neg : 0 ≤ r z ^ (-k) * 0
⊢ HPow.hPow (α := ℝ) 0 (-k) ≤ r z ^ (-k) * HPow.hPow (α := ℝ) 0 (-k)
have neg₁ : LE.le (α := ℝ) 0 0
Tactic: rw [Real.zero_rpow h, mul_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
hx : ¬x = 0
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ r z ^ (-k) * ‖x‖ ^ (-k)
have neg : ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤ (r z * ‖x‖) ^ (-k)
Tactic: rw [← Real.mul_rpow (r_pos _).le (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ ‖(↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤
    r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-k) * ‖x‖ ^ (-k)
have refine : r z ^ (-k) ≤ r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ } ^ (-k)
Tactic: refine (summand_bound z hk x).trans (mul_le_mul_of_nonneg_right ?_ (by positivity))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
c e : ℤ
z : ℂ
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: apply IsTheta.add_isLittleO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
c e : ℤ
z : ℂ
hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have ho : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: apply IsTheta.add_isLittleO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
c e : ℤ
z : ℂ
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have hΘ : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
c e : ℤ
z : ℂ
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have hΘ : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: apply IsTheta.add_isLittleO <;>
  [refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real); skip]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
c e : ℤ
z : ℂ
hΘ : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have ho : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑e : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: apply IsTheta.add_isLittleO <;>
  [refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real); skip]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: apply IsTheta.add_isLittleO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
have ho : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: apply IsTheta.add_isLittleO
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
have hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ z * (↑c : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
z : ℂ
b : ℤ
⊢ Tendsto (β := ℂ) (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z + (↑d : ℂ))) atTop (𝓝 0)
have apply : IsBigO (E := ℂ) (F := ℝ) atTop (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z + (↑d : ℂ))) fun (n : ℕ) ↦ (↑n : ℝ)⁻¹
Tactic: apply IsBigO.trans_tendsto ?_ tendsto_inv_atTop_nhds_zero_nat (F'' := ℝ)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (hypothesis)
Goal:
z : ℂ
b : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z + (↑d : ℂ))) fun (n : ℕ) ↦ (↑n : ℝ)⁻¹
have this : IsBigO (E := ℂ) (F := ℝ) atTop (fun (d : ℤ) ↦ ((↑b : ℂ) * z + (↑d : ℂ))⁻¹) fun (n : ℤ) ↦ (↑n : ℝ)⁻¹
Tactic: have := (isBigO_sup.mp (Int.cofinite_eq ▸ linear_inv_isBigO_right b z)).2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ Summable (α := ℝ) fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)
have rw : (∀ (j : ℕ),
    Summable (α := ℝ) fun (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)) ↦
      ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ)) (↑i : ℤ × ℤ)) ∧
  Summable (α := ℝ) fun (j : ℕ) ↦
    ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)),
      ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ)) (↑i : ℤ × ℤ)
Tactic: rw [← (finTwoArrowEquiv _).symm.summable_iff, summable_partition _ Int.existsUnique_mem_box]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
rw :
  (∀ (j : ℕ),
      Summable (α := ℝ) fun (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)) ↦
        ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ)) (↑i : ℤ × ℤ)) ∧
    Summable (α := ℝ) fun (j : ℕ) ↦
      ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)),
        ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ)) (↑i : ℤ × ℤ)
⊢ Summable (α := ℝ) fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)
have rw₁ : LE.le (α := ℤ × ℤ → ℝ) 0 ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
Tactic: rw [← (finTwoArrowEquiv _).symm.summable_iff, summable_partition _ Int.existsUnique_mem_box]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ),
      Summable (α := ℝ) fun (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)) ↦ ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-k)) ∧
    Summable (α := ℝ) fun (j : ℕ) ↦
      ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-k)
have refine : Summable (α := ℝ) fun (j : ℕ) ↦ ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-k)
Tactic: refine ⟨fun n ↦ (hasSum_fintype (β := box (α := ℤ × ℤ) n) _).summable, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
⊢ Summable (α := ℝ) fun (j : ℕ) ↦
    ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-k)
have refine : ∀ (n : ℕ) (p : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k) = ‖![(↑p : ℤ × ℤ).1, (↑p : ℤ × ℤ).2]‖ ^ (-k)
Tactic: refine this.congr fun n ↦ tsum_congr fun p ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ Summable (α := ℝ) fun (j : ℕ) ↦
    ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-k)
have suffices : Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
Tactic: suffices Summable fun n : ℕ ↦ ∑' (_ : box (α := ℤ × ℤ) n), (n : ℝ) ^ (-k) by
      refine this.congr fun n ↦ tsum_congr fun p ↦ ?_
      simp only [← Int.mem_box.mp p.2, Nat.cast_max, norm_eq_max_natAbs, Matrix.cons_val_zero,
        Matrix.cons_val_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
have simp : Summable (α := ℝ) fun (n : ℕ) ↦ (↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
Tactic: simp only [tsum_fintype, univ_eq_attach, sum_const, card_attach, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ 1 - k < -1
have linarith : -1 ≤ 1 - k → 2 - k + (-1 - (1 - k)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
have apply : ∀ᶠ (i : ℕ) in atTop,
  ‖(↑(card (α := ℤ × ℤ) (box i)) : ℝ) * HPow.hPow (α := ℝ) (↑i : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑i : ℝ) (1 - k)
Tactic: apply ((Real.summable_nat_rpow.mpr (by linarith : 1 - k < -1)).mul_left
      8).of_norm_bounded_eventually_nat
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
⊢ ∀ᶠ (i : ℕ) in atTop,
    ‖(↑(card (α := ℤ × ℤ) (box i)) : ℝ) * HPow.hPow (α := ℝ) (↑i : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑i : ℝ) (1 - k)
have h : ∀ (n : ℕ) (hn : 0 < n),
  ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
Tactic: filter_upwards [Filter.eventually_gt_atTop 0] with n hn
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₂ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 + -k)
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₂ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 + -k)
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₃ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
  8 * (HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₂ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 + -k)
h₃ :
  (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * (HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₄ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable (goal)
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
h : ‖(↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₁ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
h₂ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 + -k)
h₃ :
  (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * (HPow.hPow (α := ℝ) (β := ℝ) (↑n : ℝ) 1 * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₄ : (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
⊢ ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
have h₅ : HMul.hMul (α := ℝ) (↑8 : ℝ) (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
  8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
Tactic: rw [Int.card_box hn.ne', Real.norm_of_nonneg (by positivity), sub_eq_add_neg,
      Real.rpow_add (Nat.cast_pos.mpr hn), Real.rpow_one, Nat.cast_mul, Nat.cast_ofNat, mul_assoc]