-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ+} (a : Fin 2 → ZMod N) {k : ℤ} (hk : 3 ≤ k)
    (A : SL(2, ℤ)) : IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A)

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
x : Fin 2 → ℤ
⊢ ‖eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
simp_rw [eisSummand, norm_zpow]

Result:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
x : Fin 2 → ℤ
⊢ ‖↑(x 0) * ↑(ModularGroup.T ^ (↑↑N * n) • z) + ↑(x 1)‖ ^ (-k) ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
x : Fin 2 → ℤ
⊢ ‖↑(x 0) * ↑(ModularGroup.T ^ (↑↑N * n) • z) + ↑(x 1)‖ ^ (-k) ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
exact_mod_cast
  summand_bound_of_mem_verticalStrip (lt_trans two_pos hk').le x two_pos
  (verticalStrip_anti_right N hz hn)

Result:
no goals

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∀ (z : ℍ),
    2 ≤ z.im → ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
intro z hz

Result:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
⊢ ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
apply tsum_le_tsum _ (summable_norm_eisSummand hk _)

Result:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
⊢ Summable fun i => r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖i‖ ^ (-k)

N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
⊢ ∀ (i : Fin 2 → ℤ),
    ‖eisSummand k i (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖i‖ ^ (-k)

Proof state:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
⊢ Summable fun i => r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖i‖ ^ (-k)

Tactic:
exact_mod_cast (summable_one_div_norm_rpow hk').mul_left <| r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k)

Result:
no goals

Proof state:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ ‖(eisensteinSeries_SIF (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod ↑N))) A)) k)
        (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)

Result:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A)

Tactic:
simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeries_SIF] at *

Result:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∃ M A_1, ∀ (z : ℍ), A_1 ≤ z.im → ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ M

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ 2 < ↑k

Tactic:
norm_cast

Result:
no goals

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
⊢ ∀ (i : Fin 2 → ℤ),
    ‖eisSummand k i (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖i‖ ^ (-k)

Tactic:
intro x

Result:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
x : Fin 2 → ℤ
⊢ ‖eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤ r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
rw [eisensteinSeries_slash_apply, ← eisensteinSeries_SIF_apply,
  ← T_zpow_width_invariant N k n (eisensteinSeries_SIF (a ᵥ* A) k) z]

Result:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ ‖(eisensteinSeries_SIF (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod ↑N))) A)) k)
        (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∃ M A_1, ∀ (z : ℍ), A_1 ≤ z.im → ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ M

Tactic:
refine ⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩

Result:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∀ (z : ℍ),
    2 ≤ z.im → ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
⊢ ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z N.2)

Result:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ ‖(eisensteinSeries a k ∣[k] A) z‖ ≤ ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)

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

Result:
case intro
N : ℕ+
a : Fin 2 → ZMod ↑N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑↑N * n) • z ∈ verticalStrip (↑↑N) z.im
hk' : 2 < ↑k
⊢ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ (↑↑N * n) • z)‖ ≤
    ∑' (x : Fin 2 → ℤ), r ⟨{ re := ↑↑N, im := 2 }, ⋯⟩ ^ (-k) * ‖x‖ ^ (-k)