-- 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 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
⊢ Integrable ((fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i) (volume.restrict (Ioi 0))

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

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
⊢ Integrable (fun t => a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

Proof state:
case convert_4.hf
ι : 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
⊢ Summable fun a_1 => ‖∫ (a_2 : ℝ) in Ioi 0, ‖(fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) a_1 a_2‖ ∂volume‖

Tactic:
convert h_sum.mul_left (Real.Gamma s.re) using 2 with i

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_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)

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 * (Complex.Gamma s / ↑(p i) ^ s) = a i * ∫ (a : ℝ) in Ioi 0, ↑a ^ (s - 1) * ↑(rexp (-p i * a)) ∂volume

Tactic:
rw [hai, zero_mul, zero_mul]

Result:
no goals

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
⊢ Integrable (fun t => a i * (↑t ^ (s - 1) * ↑(rexp (-p i * t)))) (volume.restrict (Ioi 0))

Tactic:
refine (IntegrableOn.congr_fun (this.const_mul (1 / p i ^ (s - 1)))
  (fun t (ht : 0 < t) ↦ ?_) measurableSet_Ioi).const_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
⊢ 1 / ↑(p i) ^ (s - 1) * (↑(rexp (-(p i * t))) * ↑(p i * t) ^ (s - 1)) = ↑t ^ (s - 1) * ↑(rexp (-p i * t))

Proof state:
case h.e'_5.h.inr.e_a
ι : 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.re - 1) * rexp (-p i * t) = Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : t ∈ Ioi 0
⊢ ‖↑t ^ (s - 1) * ↑(rexp (-p i * t))‖ = t ^ (s.re - 1) * rexp (-p i * t)

Tactic:
rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
  norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]

Result:
no goals

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
⊢ ↑(p i) ^ (s - 1) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or]

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) = 0 ∨ ¬s - 1 ≠ 0

Proof state:
case convert_3
ι : 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 : ι
⊢ Integrable ((fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i) (volume.restrict (Ioi 0))

Tactic:
rcases hp i with hai | hpi

Result:
case convert_3.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
⊢ Integrable ((fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i) (volume.restrict (Ioi 0))

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
⊢ Integrable ((fun i t => ↑t ^ (s - 1) * (a i * ↑(rexp (-p i * t)))) i) (volume.restrict (Ioi 0))

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
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

Tactic:
simp_rw [← ofReal_mul, ← ofReal_neg, ← ofReal_exp, ← neg_mul (p i)] at this

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) * ↑(rexp (-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