awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c : ℤ
z : ℂ
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
simpa using linear_isTheta_right_add c 0 z

Premises used: EisensteinSeries.linear_isTheta_right_add, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)
ho : IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z + (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
apply IsTheta.add_isLittleO

Premises used: Asymptotics.IsTheta.add_isLittleO
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
hΘ : IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ z * (↑c : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑c : ℂ) * z) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ IsTheta (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ z * (↑c : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
apply Asymptotics.IsTheta.const_mul_left hz Int.cast_complex_isTheta_cast_real

Premises used: Int.cast_complex_isTheta_cast_real, Asymptotics.IsTheta.const_mul_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ IsLittleO (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ (↑d : ℂ)) fun (n : ℤ) ↦ (↑n : ℝ)

Tactic:
simp only [isLittleO_const_left, Int.cast_eq_zero,
      tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real, or_true]

Premises used: Asymptotics.isLittleO_const_left, Int.isClosedEmbedding_coe_real, Int.cast_eq_zero, or_true, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c e : ℤ
z : ℂ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ ((↑c : ℂ) * z + (↑d : ℂ) + (↑e : ℂ))⁻¹) fun (n : ℤ) ↦ (↑n : ℝ)⁻¹

Tactic:
(linear_isTheta_right_add c e z).inv.isBigO

Premises used: Asymptotics.IsTheta.isBigO, Asymptotics.IsTheta.inv, EisensteinSeries.linear_isTheta_right_add
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
c : ℤ
z : ℂ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (d : ℤ) ↦ ((↑c : ℂ) * z + (↑d : ℂ))⁻¹) fun (n : ℤ) ↦ (↑n : ℝ)⁻¹

Tactic:
grind [add_zero, (linear_isTheta_right_add c 0 z).inv.isBigO]

Premises used: Asymptotics.IsTheta.isBigO, Asymptotics.IsTheta.inv, EisensteinSeries.linear_isTheta_right_add, add_zero, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
d : ℤ
z : ℂ
hz : z ≠ 0
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (c : ℤ) ↦ ((↑c : ℂ) * z + (↑d : ℂ))⁻¹) fun (n : ℤ) ↦ (↑n : ℝ)⁻¹

Tactic:
(linear_isTheta_left d hz).inv.isBigO

Premises used: Asymptotics.IsTheta.isBigO, EisensteinSeries.linear_isTheta_left, Asymptotics.IsTheta.inv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
b : ℤ
apply : IsBigO (E := ℂ) (F := ℝ) atTop (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z + (↑d : ℂ))) fun (n : ℕ) ↦ (↑n : ℝ)⁻¹
⊢ Tendsto (β := ℂ) (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z + (↑d : ℂ))) atTop (𝓝 0)

Tactic:
apply IsBigO.trans_tendsto ?_ tendsto_inv_atTop_nhds_zero_nat (F'' := ℝ)

Premises used: Asymptotics.IsBigO.trans_tendsto, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
b : ℤ
⊢ 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
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
b : ℤ
this : IsBigO (E := ℂ) (F := ℝ) atTop (fun (d : ℤ) ↦ ((↑b : ℂ) * z + (↑d : ℂ))⁻¹) fun (n : ℤ) ↦ (↑n : ℝ)⁻¹
⊢ IsBigO (E := ℂ) (F := ℝ) atTop (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z + (↑d : ℂ))) fun (n : ℕ) ↦ (↑n : ℝ)⁻¹

Tactic:
simpa [← Nat.map_cast_int_atTop, isBigO_map]

Premises used: Asymptotics.isBigO_map, Nat.map_cast_int_atTop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
b : ℤ
⊢ Tendsto (β := ℂ) (fun (d : ℕ) ↦ 1 / ((↑b : ℂ) * z - (↑d : ℂ))) atTop (𝓝 0)

Tactic:
grind [neg_zero, (tendsto_zero_inv_linear z (-b)).neg]

Premises used: Filter.Tendsto.neg, EisensteinSeries.tendsto_zero_inv_linear, neg_zero, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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 : ℤ × ℤ)
rw₁ :
  LE.le (α := ℤ × ℤ → ℝ) 0 ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))
⊢ Summable (α := ℝ) fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)

Tactic:
rw [← (finTwoArrowEquiv _).symm.summable_iff, summable_partition _ Int.existsUnique_mem_box]

Premises used: Int.existsUnique_mem_box, Equiv.summable_iff, Equiv.symm, summable_partition, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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)

Tactic:
⟨fun n ↦ (hasSum_fintype (β := box (α := ℤ × ℤ) n) _).summable, ?_⟩

Premises used: Norm.norm, Membership.mem, Subtype, hasSum_fintype, Prod.fst, HasSum.summable, HPow.hPow, And.intro, Matrix.vecEmpty, Subtype.val, Prod.snd, Matrix.vecCons, Finset.box, Neg.neg, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
refine :
  Summable (α := ℝ) fun (j : ℕ) ↦
    ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).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)

Tactic:
refine ⟨fun n ↦ (hasSum_fintype (β := box (α := ℤ × ℤ) n) _).summable, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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)

Tactic:
this.congr fun n ↦ tsum_congr fun p ↦ ?_

Premises used: tsum_congr, Summable.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
refine : ∀ (n : ℕ) (p : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k) = ‖![(↑p : ℤ × ℤ).1, (↑p : ℤ × ℤ).2]‖ ^ (-k)
⊢ Summable (α := ℝ) fun (j : ℕ) ↦
    ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-k)

Tactic:
refine this.congr fun n ↦ tsum_congr fun p ↦ ?_

Premises used: tsum_congr, Summable.congr
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
this : Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
n : ℕ
p : ↥(box n)
⊢ HPow.hPow (α := ℝ) (↑n : ℝ) (-k) = ‖![(↑p : ℤ × ℤ).1, (↑p : ℤ × ℤ).2]‖ ^ (-k)

Tactic:
simp only [← Int.mem_box.mp p.2, Nat.cast_max, norm_eq_max_natAbs, Matrix.cons_val_zero,
        Matrix.cons_val_one]

Premises used: Matrix.cons_val_one, Matrix.cons_val_zero, Nat.cast_max, EisensteinSeries.norm_eq_max_natAbs, Iff.mp, Int.mem_box, Subtype.property
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
suffices : Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
⊢ Summable (α := ℝ) fun (j : ℕ) ↦
    ∑' (i : (↑(↑(box j) : Set (ℤ × ℤ)) : Type)), ‖![(↑i : ℤ × ℤ).1, (↑i : ℤ × ℤ).2]‖ ^ (-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]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
simp : Summable (α := ℝ) fun (n : ℕ) ↦ (↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ∑' (x : ↥(box n)), HPow.hPow (α := ℝ) (↑n : ℝ) (-k)

Tactic:
simp only [tsum_fintype, univ_eq_attach, sum_const, card_attach, nsmul_eq_mul]

Premises used: Finset.card_attach, Finset.univ_eq_attach, tsum_fintype, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
linarith : -1 ≤ 1 - k → 2 - k + (-1 - (1 - k)) = 0
⊢ 1 - k < -1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
apply :
  ∀ᶠ (i : ℕ) in atTop,
    ‖(↑(card (α := ℤ × ℤ) (box i)) : ℝ) * HPow.hPow (α := ℝ) (↑i : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑i : ℝ) (1 - k)
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ (↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)

Tactic:
apply ((Real.summable_nat_rpow.mpr (by linarith : 1 - k < -1)).mul_left
      8).of_norm_bounded_eventually_nat

Premises used: Iff.mpr, Summable.mul_left, OfNat.ofNat, Real.summable_nat_rpow, Summable.of_norm_bounded_eventually_nat
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
h :
  ∀ (n : ℕ) (hn : 0 < n),
    ‖(↑(card (α := ℤ × ℤ) (box n)) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑n : ℝ) (1 - k)
⊢ ∀ᶠ (i : ℕ) in atTop,
    ‖(↑(card (α := ℤ × ℤ) (box i)) : ℝ) * HPow.hPow (α := ℝ) (↑i : ℝ) (-k)‖ ≤ 8 * HPow.hPow (α := ℝ) (↑i : ℝ) (1 - k)

Tactic:
filter_upwards [Filter.eventually_gt_atTop 0] with n hn

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ 0 ≤ (↑(8 * n) : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
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))
h₅ :
  HMul.hMul (α := ℝ) (↑8 : ℝ) (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤
    8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₆ :
  HMul.hMul (α := ℝ) 8 (↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k) ≤ 8 * ((↑n : ℝ) * HPow.hPow (α := ℝ) (↑n : ℝ) (-k))
h₇ 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)

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]

Premises used: Iff.mpr, Nat.cast_ofNat, Nat.cast_pos, mul_assoc, sub_eq_add_neg, Int.card_box, Real.rpow_one, LT.lt.ne', Nat.cast_mul, Real.rpow_add, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
⊢ LE.le (α := ℤ × ℤ → ℝ) 0 ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))

Tactic:
fun n ↦ Real.rpow_nonneg (norm_nonneg _) _

Premises used: Int, Real.rpow_nonneg, Equiv.symm, DFunLike.coe, norm_nonneg, Neg.neg, finTwoArrowEquiv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
k : ℝ
hk : 2 < k
⊢ LE.le (α := ℤ × ℤ → ℝ) 0 ((fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)) ∘ (⇑(finTwoArrowEquiv ℤ).symm : (a : ℤ × ℤ) → Fin 2 → ℤ))

Tactic:
exact fun n ↦ Real.rpow_nonneg (norm_nonneg _) _

Premises used: Real.rpow_nonneg, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
α : Type u_1
inst : NormedField α
inst_1 : CompleteSpace α
f : ℤ → α
a : ℝ
hab : 1 < a
hf :
  IsBigO.{0, u_1, 0} (E := α) (F := ℝ) cofinite (fun (n : ℤ) ↦ (f n)⁻¹) fun (n : ℤ) ↦
    (HPow.hPow (α := ℝ) |(↑n : ℝ)| a)⁻¹
⊢ Summable.{u_1, 0} (α := α) fun (n : ℤ) ↦ (f n)⁻¹

Tactic:
summable_of_isBigO
    ((Real.summable_abs_int_rpow hab).congr fun b ↦ Real.rpow_neg (abs_nonneg ↑b) a) hf

Premises used: Real.summable_abs_int_rpow, Summable.congr, summable_of_isBigO
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c k : ℤ
hk : 2 ≤ k
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < k
⊢ LT.lt (α := ℝ) 1 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c k : ℤ
hk : 2 ≤ k
⊢ 0 ≤ k

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c k : ℤ
hk : 2 ≤ k
lift :
  ∀ (k : ℕ) (hk : LE.le (α := ℤ) 2 (↑k : ℤ)),
    IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑c : ℂ) * z + (↑n : ℂ)) (↑k : ℤ))⁻¹)
      fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c : ℂ) * z + (↑n : ℂ)) ^ k)⁻¹) fun (n : ℤ) ↦
    (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑k : ℝ))⁻¹

Tactic:
lift k to ℕ using by lia
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c : ℤ
k : ℕ
hk : LE.le (α := ℤ) 2 (↑k : ℤ)
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑c : ℂ) * z + (↑n : ℂ)) (↑k : ℤ))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹

Tactic:
grind [(linear_inv_isBigO_right c z).abs_right.pow k,
    zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow]

Premises used: zpow_natCast, Int.cast_natCast, inv_pow, Asymptotics.IsBigO.abs_right, Asymptotics.IsBigO.pow, Real.rpow_natCast, EisensteinSeries.linear_inv_isBigO_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 1 < k
⊢ LT.lt (α := ℝ) 1 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
apply :
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑d : ℂ)) ^ k)⁻¹) fun (n : ℤ) ↦
    (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑k : ℝ))⁻¹
⊢ Summable (α := ℂ) fun (c : ℤ) ↦ (((↑c : ℂ) * z + (↑d : ℂ)) ^ k)⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)

Premises used: EisensteinSeries.summable_inv_of_isBigO_rpow_inv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
⊢ 0 ≤ k

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
d k : ℤ
hk : 2 ≤ k
lift :
  ∀ (k : ℕ) (hk : LE.le (α := ℤ) 2 (↑k : ℤ)),
    IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑n : ℂ) * z + (↑d : ℂ)) (↑k : ℤ))⁻¹)
      fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑d : ℂ)) ^ k)⁻¹) fun (n : ℤ) ↦
    (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑k : ℝ))⁻¹

Tactic:
lift k to ℕ using (by lia)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : LE.le (α := ℤ) 2 (↑k : ℤ)
simp :
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ ((↑n : ℂ) * z + (↑d : ℂ))⁻¹ ^ k) fun (n : ℤ) ↦
    HPow.hPow (α := ℝ) |(↑n : ℝ)⁻¹| k
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (HPow.hPow (β := ℤ) ((↑n : ℂ) * z + (↑d : ℂ)) (↑k : ℤ))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| (↑(↑k : ℤ) : ℝ))⁻¹

Tactic:
simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]

Premises used: zpow_natCast, Int.cast_natCast, abs_inv, inv_pow, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
d : ℤ
k : ℕ
hk : LE.le (α := ℤ) 2 (↑k : ℤ)
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ ((↑n : ℂ) * z + (↑d : ℂ))⁻¹ ^ k) fun (n : ℤ) ↦
    HPow.hPow (α := ℝ) |(↑n : ℝ)⁻¹| k

Tactic:
apply (linear_inv_isBigO_left d hz).abs_right.pow

Premises used: EisensteinSeries.linear_inv_isBigO_left, Asymptotics.IsBigO.abs_right, Asymptotics.IsBigO.pow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c₁ c₂ : ℤ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LT.lt (α := ℕ) 1 2
⊢ LT.lt (α := ℝ) 1 2

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c₁ c₂ : ℤ
apply :
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z - (↑n : ℂ)) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z - (↑n : ℂ)) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)

Premises used: EisensteinSeries.summable_inv_of_isBigO_rpow_inv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c₁ c₂ : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z - (↑n : ℂ)) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹

Tactic:
simpa [pow_two] using (linear_inv_isBigO_right c₂ z).mul
      (linear_inv_isBigO_right c₁ z).comp_neg_int

Premises used: pow_two, Asymptotics.IsBigO.mul, Asymptotics.IsBigO.comp_neg_int, EisensteinSeries.linear_inv_isBigO_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c₁ c₂ : ℤ
apply :
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z + (↑n : ℂ) + 1) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z + (↑n : ℂ) + 1) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)

Premises used: EisensteinSeries.summable_inv_of_isBigO_rpow_inv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
c₁ c₂ : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑c₁ : ℂ) * z + (↑n : ℂ) + 1) * ((↑c₂ : ℂ) * z + (↑n : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹

Tactic:
simpa [pow_two] using (linear_inv_isBigO_right c₂ z).mul
    (linear_inv_isBigO_right_add c₁ 1 z)

Premises used: pow_two, Asymptotics.IsBigO.mul, EisensteinSeries.linear_inv_isBigO_right_add, OfNat.ofNat, EisensteinSeries.linear_inv_isBigO_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : LT.lt (α := ℕ) 1 2
⊢ LT.lt (α := ℝ) 1 2

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
apply :
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹
⊢ Summable (α := ℂ) fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹

Tactic:
apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)

Premises used: EisensteinSeries.summable_inv_of_isBigO_rpow_inv
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
simp :
  IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ))⁻¹
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HPow.hPow (α := ℝ) (β := ℝ) |(↑n : ℝ)| 2)⁻¹

Tactic:
simp only [Real.rpow_two, abs_mul_abs_self, pow_two]

Premises used: pow_two, Real.rpow_two, abs_mul_abs_self
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℂ
hz : z ≠ 0
c₁ c₂ : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite (fun (n : ℤ) ↦ (((↑n : ℂ) * z + (↑c₁ : ℂ)) * ((↑n : ℂ) * z + (↑c₂ : ℂ)))⁻¹)
    fun (n : ℤ) ↦ (HMul.hMul (α := ℝ) (↑n : ℝ) (↑n : ℝ))⁻¹

Tactic:
simpa using (linear_inv_isBigO_left c₂ hz).mul (linear_inv_isBigO_left c₁ hz)

Premises used: EisensteinSeries.linear_inv_isBigO_left, Asymptotics.IsBigO.mul
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
rw :
  ∃ (c : ℝ),
    ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
      ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
        c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite
    (fun (m : Fin 2 → ℤ) ↦ (HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹)
    fun (m : Fin 2 → ℤ) ↦ ‖![m 0 + a, m 1 + b]‖⁻¹

Tactic:
rw [Asymptotics.isBigO_iff]

Premises used: Asymptotics.isBigO_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
⊢ z ∈ verticalStrip |z.re| z.im

Tactic:
simp [mem_verticalStrip_iff]

Premises used: UpperHalfPlane.mem_verticalStrip_iff
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
⊢ z ∈ verticalStrip |z.re| z.im

Tactic:
have h0 : z ∈ verticalStrip |z.re| (z.im) := by simp [mem_verticalStrip_iff]
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
h :
  ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
    ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
      ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖
⊢ ∃ (c : ℝ),
    ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
      ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
        c * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖

Tactic:
use ‖r ⟨⟨|z.re|, z.im⟩, z.2⟩‖⁻¹

Premises used: abs, EisensteinSeries.r, UpperHalfPlane.mk, UpperHalfPlane.im, UpperHalfPlane.re, Complex.mk, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
h :
  ∀ (m : Fin 2 → ℤ),
    ‖(HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
      ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
⊢ ∀ᶠ (x : Fin 2 → ℤ) in cofinite,
    ‖(HAdd.hAdd (α := ℂ) (↑(x 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
      ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![x 0 + a, x 1 + b]‖⁻¹‖

Tactic:
filter_upwards with m
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
    (r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ })⁻¹ * ‖![m 0 + a, m 1 + b]‖⁻¹

Tactic:
simpa [Real.rpow_neg_one, add_assoc] using
    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0

Premises used: EisensteinSeries.summand_bound_of_mem_verticalStrip, Real.rpow_neg_one, add_assoc, zero_le_one, HAdd.hAdd, Matrix.vecEmpty, OfNat.ofNat, Matrix.vecCons, UpperHalfPlane.coe_im_pos