-- Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
/-- Most basic version of the "Mellin transform = Dirichlet series" argument. -/
lemma hasSum_mellin {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ}
    (hp : ∀ i, a i = 0 ∨ 0 < p i) (hs : 0 < s.re)
    (hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * rexp (-p i * t)) (F t))
    (h_sum : Summable fun i ↦ ‖a i‖ / (p i) ^ s.re) :
    HasSum (fun i ↦ Gamma s * a i / p i ^ s) (mellin F s)

Proof state:
case h.e'_5.h
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
i : ι
⊢ ‖∫ (a_1 : ℝ) in Ioi 0, ‖(fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i a_1‖ ∂volume‖ =
    Real.Gamma s.re * (‖a i‖ / p i ^ s.re)

Tactic:
simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc, norm_mul (a i), integral_mul_left]

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

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

Tactic:
rcases hp i with hai | hpi

Result:
case h.e'_5.h.inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
⊢ ‖a i‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)

case h.e'_5.h.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ ‖a i‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)

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

Tactic:
have := integral_cpow_mul_exp_neg_mul_Ioi hs hpi

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

Proof state:
case h.e'_5.h.inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
i : ι
hai : a i = 0
⊢ ‖a i‖ * ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)

Tactic:
simp [hai]

Result:
no goals

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

Tactic:
rcases hp i with hai | hpi

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

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

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

Tactic:
simp_rw [mellin, smul_eq_mul, ← setIntegral_congr_fun measurableSet_Ioi
  (fun t ht ↦ congr_arg _ (hF t ht).tsum_eq), ← tsum_mul_left]

Result:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
⊢ HasSum (fun i => Complex.Gamma s * a i / ↑(p i) ^ s)
    (∫ (x : ℝ) in Ioi 0, ∑' (x_1 : ι), ↑x ^ (s - 1) * (a x_1 * ↑(rexp (-p x_1 * x))) ∂volume)

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

Tactic:
rw [← mul_div_assoc, mul_comm (Real.Gamma _), mul_div_assoc, norm_mul ‖a i‖, norm_norm]

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

Proof state:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x => ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / ↑(p i) ^ (s - 1) * (↑(p i) * ↑t) ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-(p i * t)))

Tactic:
rw [mul_cpow_ofReal_nonneg hpi.le ht.le, ← mul_assoc, one_div, inv_mul_cancel₀, one_mul]

Result:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x => ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ ↑(p i) ^ (s - 1) ≠ 0