-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
/-- The function `ℤ ^ 2 → ℝ` given by `x ↦ ‖x‖ ^ (-k)` is summable if `2 < k`. We prove this by
splitting into boxes using `Finset.box`. -/
lemma summable_one_div_norm_rpow {k : ℝ} (hk : 2 < k) :
    Summable fun (x : Fin 2 → ℤ) ↦ ‖x‖ ^ (-k)

Proof state:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i => ((fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i) ∧
    Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ((fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i

Tactic:
simp only [finTwoArrowEquiv_symm_apply, Function.comp_def]

Result:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i => ‖![(↑i).1, (↑i).2]‖ ^ (-k)) ∧
    Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

Proof state:
case h
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ‖↑(#(box n)) * ↑n ^ (-k)‖ ≤ 8 * ↑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]

Result:
no goals

Proof state:
k : ℝ
hk : 2 < k
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖↑(#(box i)) * ↑i ^ (-k)‖ ≤ 8 * ↑i ^ (1 - k)

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

Result:
case h
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ ‖↑(#(box n)) * ↑n ^ (-k)‖ ≤ 8 * ↑n ^ (1 - k)

Proof state:
k : ℝ
hk : 2 < k
⊢ Summable fun n => ∑' (x : { x // x ∈ box n }), ↑n ^ (-k)

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

Result:
k : ℝ
hk : 2 < k
⊢ Summable fun n => ↑(#(box n)) * ↑n ^ (-k)

Proof state:
k : ℝ
hk : 2 < k
n : ℕ
hn : 0 < n
⊢ 0 ≤ ↑(8 * n) * ↑n ^ (-k)

Tactic:
positivity

Result:
no goals

Proof state:
k : ℝ
hk : 2 < k
⊢ 1 - k < -1

Tactic:
linarith

Result:
no goals

Proof state:
k : ℝ
hk : 2 < k
⊢ 0 ≤ (fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm

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

Result:
no goals

Proof state:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i => ‖![(↑i).1, (↑i).2]‖ ^ (-k)) ∧
    Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

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

Result:
k : ℝ
hk : 2 < k
⊢ Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

Proof state:
k : ℝ
hk : 2 < k
⊢ Summable fun n => ↑(#(box n)) * ↑n ^ (-k)

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

Result:
k : ℝ
hk : 2 < k
⊢ ∀ᶠ (i : ℕ) in Filter.atTop, ‖↑(#(box i)) * ↑i ^ (-k)‖ ≤ 8 * ↑i ^ (1 - k)

Proof state:
k : ℝ
hk : 2 < k
⊢ Summable fun x => ‖x‖ ^ (-k)

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

Result:
k : ℝ
hk : 2 < k
⊢ (∀ (j : ℕ), Summable fun i => ((fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i) ∧
    Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ((fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm) ↑i

k : ℝ
hk : 2 < k
⊢ 0 ≤ (fun x => ‖x‖ ^ (-k)) ∘ ⇑(finTwoArrowEquiv ℤ).symm

Proof state:
k : ℝ
hk : 2 < k
⊢ Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ‖![(↑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, Matrix.head_cons]

Result:
k : ℝ
hk : 2 < k
⊢ Summable fun n => ∑' (x : { x // x ∈ box n }), ↑n ^ (-k)

Proof state:
k : ℝ
hk : 2 < k
this : Summable fun n => ∑' (x : { x // x ∈ box n }), ↑n ^ (-k)
⊢ Summable fun j => ∑' (i : ↑(Membership.mem (box j).val)), ‖![(↑i).1, (↑i).2]‖ ^ (-k)

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

Result:
k : ℝ
hk : 2 < k
this : Summable fun n => ∑' (x : { x // x ∈ box n }), ↑n ^ (-k)
n : ℕ
p : { x // x ∈ box n }
⊢ ↑n ^ (-k) = ‖![(↑p).1, (↑p).2]‖ ^ (-k)

Proof state:
k : ℝ
hk : 2 < k
this : Summable fun n => ∑' (x : { x // x ∈ box n }), ↑n ^ (-k)
n : ℕ
p : { x // x ∈ box n }
⊢ ↑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, Matrix.head_cons]

Result:
no goals