-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
theorem eisensteinSeries_tendstoLocallyUniformly {k : ℤ} (hk : 3 ≤ k) {N : ℕ} (a : Fin 2 → ZMod N) :
    TendstoLocallyUniformly (fun (s : Finset (gammaSet N a)) ↦ (∑ x ∈ s, eisSummand k x ·))
      (eisensteinSeries a k ·) Filter.atTop

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ 0 ≤ ↑k

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
    (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K

Tactic:
refine (tendstoUniformlyOn_tsum (hu := p_sum.mul_left <| r ⟨⟨A, B⟩, hB⟩ ^ (-k : ℝ))
  (fun p z hz ↦ ?_)).mono HABK

Result:
case intro.intro.intro
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ ‖eisSummand k (↑p) z‖ ≤ r ⟨{ re := A, im := B }, hB⟩ ^ (-↑k) * ‖↑p‖ ^ (-k)

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
⊢ 2 < ↑k

Tactic:
norm_cast

Result:
no goals

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
⊢ TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop

Tactic:
have p_sum : Summable fun x : gammaSet N a ↦ ‖x.val‖ ^ (-k) :=
  mod_cast (summable_one_div_norm_rpow hk').subtype (gammaSet N a)

Result:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
⊢ TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
⊢ ∀ (K : Set ℍ),
    IsCompact K →
      TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
        (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K

Tactic:
intro K hK

Result:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
⊢ TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
    (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K

Proof state:
case intro.intro.intro
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ ‖eisSummand k (↑p) z‖ ≤ r ⟨{ re := A, im := B }, hB⟩ ^ (-↑k) * ‖↑p‖ ^ (-k)

Tactic:
simpa only [eisSummand, one_div, ← zpow_neg, norm_zpow, ← Real.rpow_intCast,
  Int.cast_neg] using summand_bound_of_mem_verticalStrip (by positivity) p hB hz

Result:
no goals

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast

Result:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
⊢ TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
⊢ TendstoLocallyUniformly (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x => eisensteinSeries a k x) Filter.atTop

Tactic:
simp only [tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries]

Result:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
⊢ ∀ (K : Set ℍ),
    IsCompact K →
      TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
        (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K

Proof state:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
⊢ TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
    (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K

Tactic:
obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact hK

Result:
case intro.intro.intro
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x => ‖↑x‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ TendstoUniformlyOn (fun s x => ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
    (fun x => ∑' (x_1 : ↑(gammaSet N a)), eisSummand k (↑x_1) x) Filter.atTop K