-- Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
/-- Version allowing some constant terms (which are omitted from the sums). -/
lemma hasSum_mellin_pi_mul₀ {a : ι → ℂ} {p : ι → ℝ} {F : ℝ → ℂ} {s : ℂ}
    (hp : ∀ i, 0 ≤ p i) (hs : 0 < s.re)
    (hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * rexp (-π * p i * t)) (F t))
    (h_sum : Summable fun i ↦ ‖a i‖ / (p i) ^ s.re) :
    HasSum (fun i ↦ π ^ (-s) * Gamma s * a i / p i ^ s) (mellin F s)

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

Tactic:
positivity

Result:
no goals

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

Tactic:
simp only [a']

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

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

Tactic:
simp [a']

Result:
no goals

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

Tactic:
simp only [a']

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

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

Tactic:
refine h_sum.of_norm_bounded _ (fun i ↦ ?_)

Result:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i => if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ‖‖a' i‖ / p i ^ 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 : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i => if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s = ↑π ^ (-s) * Complex.Gamma s * a' i / ↑(p i) ^ s

Tactic:
rcases eq_or_ne (p i) 0 with h | h <;>
simp [a', h, if_false, ofReal_zero, zero_cpow hs', div_zero]

Result:
no goals

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

Tactic:
let a' i := if p i = 0 then 0 else a i

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

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

Tactic:
split_ifs with h <;> try tauto

Result:
case neg
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i => if p i = 0 then 0 else a i
i : ι
h : ¬p i = 0
⊢ a i = 0 ∨ 0 < p i

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

Tactic:
simp only [norm_zero, zero_div]

Result:
case pos
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i => if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i => a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
h✝ : p i = 0
⊢ 0 ≤ ‖a i‖ / p i ^ s.re