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

Tactic:
rw [norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)), ← this]

Result:
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
⊢ ∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume = ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-p i * t)

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

Tactic:
exact Or.inl (ofReal_ne_zero.mpr hpi.ne')

Result:
no goals

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)
    (∫ (x : ℝ) in Ioi 0, ∑' (x_1 : ι), ↑x ^ (s - 1) * (a x_1 * ↑(rexp (-p x_1 * x))) ∂volume)

Tactic:
convert hasSum_integral_of_summable_integral_norm
  (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t))) (fun i ↦ ?_) ?_ 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 : ι
⊢ Complex.Gamma s * a i / ↑(p i) ^ s = ∫ (a_1 : ℝ) in Ioi 0, ↑a_1 ^ (s - 1) * (a i * ↑(rexp (-p i * a_1))) ∂volume

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

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

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

Tactic:
congr 1

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

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

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)

Result:
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)