-- Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
/-- Shortcut version for the commonly arising special case when `p i = π * q i` for some other
sequence `q`. -/
lemma hasSum_mellin_pi_mul {a : ι → ℂ} {q : ι → ℝ} {F : ℝ → ℂ} {s : ℂ}
    (hq : ∀ i, a i = 0 ∨ 0 < q i) (hs : 0 < s.re)
    (hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * rexp (-π * q i * t)) (F t))
    (h_sum : Summable fun i ↦ ‖a i‖ / (q i) ^ s.re) :
    HasSum (fun i ↦ π ^ (-s) * Gamma s * a i / q i ^ s) (mellin F s)

Proof state:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]

Result:
no goals

Proof state:
case h.e'_5.h
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
this : a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s = Complex.Gamma s * a i / ↑(π * q i) ^ s

Tactic:
simp_rw [mul_div_assoc, this]

Result:
case h.e'_5.h
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
this : a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
⊢ ↑π ^ (-s) * Complex.Gamma s * (a i / ↑(q i) ^ s) = Complex.Gamma s * (↑π ^ (-s) * a i / ↑(q i) ^ s)

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

Tactic:
rcases hq i with h | h

Result:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
⊢ HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)

Tactic:
have hp i : a i = 0 ∨ 0 < π * q i := by rcases hq i with h | h <;> simp [h, pi_pos]

Result:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)

Proof state:
case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

Tactic:
rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
  ← div_eq_inv_mul]

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
rcases hq i with h | h

Result:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ HasSum (fun i => ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s) (mellin F s)

Tactic:
convert hasSum_mellin hp hs (by simpa using hF) ?_ using 2 with i

Result:
case h.e'_5.h
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(q i) ^ s = Complex.Gamma s * a i / ↑(π * q i) ^ s

ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ Summable fun i => ‖a i‖ / (π * q i) ^ s.re

Proof state:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
this : ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ Summable fun i => ‖a i‖ / (π * q i) ^ s.re

Tactic:
simpa only [this, mul_div_assoc] using h_sum.mul_left _

Result:
no goals

Proof state:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s

Tactic:
simp [h]

Result:
no goals

Proof state:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : a i = 0
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re

Tactic:
simp [h]

Result:
no goals