-- Mathlib/NumberTheory/LSeries/MellinEqDirichlet.lean
/-- Tailored version for even Jacobi theta functions. -/
lemma hasSum_mellin_pi_mul_sq {a : ι → ℂ} {r : ι → ℝ} {F : ℝ → ℂ} {s : ℂ} (hs : 0 < s.re)
    (hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * rexp (-π * r i ^ 2 * t)) (F t))
    (h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re) :
    HasSum (fun i ↦ Gammaℝ s * a i / |r i| ^ s) (mellin F (s / 2))

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

Tactic:
rw [← neg_div, Gammaℝ_def]

Result:
no goals

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

Tactic:
convert hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i

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

case h.e'_5.h.h.e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑(r i ^ 2) ^ (s / 2)

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

Proof state:
case h.e'_5.h.h.e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * 0 ≤ π

Tactic:
linarith [pi_pos]

Result:
no goals

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

Tactic:
have hs' : 0 < (s / 2).re := by rw [div_ofNat_re]; positivity

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

Proof state:
case h.e'_5.h.h.e'_6.hlt
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ -π < ↑2 * (↑|r i|).arg

case h.e'_5.h.h.e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π

Tactic:
all_goals rw [arg_ofReal_of_nonneg (abs_nonneg _)]; linarith [pi_pos]

Result:
no goals

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

Tactic:
rw [div_ofNat_re]

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

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

Tactic:
simp_rw [← sq_eq_zero_iff (a := r _)] at hF

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

Proof state:
case h.e'_5.h.h.e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ (r i ^ 2) ^ (s / 2).re = |r i| ^ s.re

Tactic:
rw [← sq_abs, ← rpow_natCast_mul (abs_nonneg _), div_ofNat_re, Nat.cast_ofNat,
  mul_div_cancel₀ _ two_pos.ne']

Result:
no goals

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

Tactic:
convert h_sum using 3 with i

Result:
case h.e'_5.h.h.e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ (r i ^ 2) ^ (s / 2).re = |r i| ^ s.re

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

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_5.h.h.e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * (↑|r i|).arg ≤ π

Tactic:
rw [arg_ofReal_of_nonneg (abs_nonneg _)]

Result:
case h.e'_5.h.h.e'_6.hle
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i => ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i => if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑2 * 0 ≤ π