awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
this : a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s = Complex.Gamma s * a i / (↑(π * q i) : ℂ) ^ s
have h : (↑π : ℂ) ^ (-s) * Complex.Gamma s * (a i / (↑(q i) : ℂ) ^ s) =
  Complex.Gamma s * ((↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s)
Tactic: simp_rw [mul_div_assoc, this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
have inl : ∀ (h : a i = 0), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Tactic: rcases hq i with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
inl : ∀ (h : a i = 0), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
have inr : ∀ (h : 0 < q i), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Tactic: rcases hq i with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
have inr : ‖a i‖ / (π ^ s.re * q i ^ s.re) = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Tactic: rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
inr : ‖a i‖ / (π ^ s.re * q i ^ s.re) = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
have inr₁ : ‖a i‖ / π ^ s.re / q i ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Tactic: rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
inr : ‖a i‖ / (π ^ s.re * q i ^ s.re) = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
inr₁ : ‖a i‖ / π ^ s.re / q i ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
have inr₂ : ‖a i‖ / π ^ s.re / q i ^ s.re = (π ^ s.re)⁻¹ * ‖a i‖ / q i ^ s.re
Tactic: rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
i : ι
h : 0 < q i
inr : ‖a i‖ / (π ^ s.re * q i ^ s.re) = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
inr₁ : ‖a i‖ / π ^ s.re / q i ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
inr₂ : ‖a i‖ / π ^ s.re / q i ^ s.re = (π ^ s.re)⁻¹ * ‖a i‖ / q i ^ s.re
⊢ ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
have inr₃ : ‖a i‖ / π ^ s.re / q i ^ s.re = ‖a i‖ / π ^ s.re / q i ^ s.re
Tactic: rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-π * q i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / (π * q i) ^ s.re
have this : ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
Tactic: have (i : _) : ‖a i‖ / ↑(π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re := by
      rcases hq i with h | h
      · simp [h]
      · rw [mul_rpow pi_pos.le h.le, ← div_div, rpow_neg pi_pos.le, ← div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)
have hs' : s ≠ 0
Tactic: have hs' : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := 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
have pos : ∀ (h : p i = 0), Eq (α := ℂ) 0 0 ∨ 0 < p i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := fun (i : ι) ↦ if p i = 0 then 0 else a i
i : ι
pos : ∀ (h : p i = 0), Eq (α := ℂ) 0 0 ∨ 0 < p i
⊢ (if p i = 0 then 0 else a i) = 0 ∨ 0 < p i
have neg : ∀ (h : ¬p i = 0), a i = 0 ∨ 0 < p i
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := fun (i : ι) ↦ if p i = 0 then 0 else a i
i : ι
h : p i = 0
⊢ Eq (α := ℂ) 0 0 ∨ 0 < p i
have pos : ¬Eq (α := ℂ) 0 0 → 0 < p i
Tactic: tauto
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := fun (i : ι) ↦ if p i = 0 then 0 else a i
i : ι
h : p i = 0
⊢ Eq (α := ℂ) 0 0 ∨ 0 < p i
have pos : ¬Eq (α := ℂ) 0 0 → 0 < p i
Tactic: try tauto
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := 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)
have hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
Tactic: have hp' i : a' i = 0 ∨ 0 < p i := by
    simp only [a']
    split_ifs with h <;> try tauto
    exact Or.inr (lt_of_le_of_ne (hp i) (Ne.symm h))
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := fun (i : ι) ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)
have this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
Tactic: have (i t : _) : (if p i = 0 then 0 else a i * rexp (-π * p i * t)) =
      a' i * rexp (-π * p i * t) := by
    simp [a']
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      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' : (i : ι) → ℂ := 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)) : ℂ)
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)
have hF₁ : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
Tactic: simp_rw [this] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)
have h : ∀ (i : ι),
  (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
Tactic: convert! hasSum_mellin_pi_mul hp' hs hF ?_ using 2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
h :
  ∀ (i : ι),
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)
have convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a' i‖ / p i ^ s.re
Tactic: convert! hasSum_mellin_pi_mul hp' hs hF ?_ using 2 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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
have h : ∀ (h : p i = 0),
  (↑π : ℂ) ^ (-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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h :
  ∀ (h : p i = 0),
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    (↑π : ℂ) ^ (-s) * Complex.Gamma s * a' i / (↑(p i) : ℂ) ^ s
have h₁ : ∀ (h : p i ≠ 0),
  (↑π : ℂ) ^ (-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
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a' i‖ / p i ^ s.re
have refine : ∀ (i : ι), ‖‖a' i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
Tactic: refine h_sum.of_norm_bounded (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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
have pos : p i = 0 → ‖Norm.norm (E := ℂ) 0 / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
pos : p i = 0 → ‖Norm.norm (E := ℂ) 0 / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
⊢ ‖‖if p i = 0 then 0 else a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
have neg : ¬p i = 0 → ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : p i = 0
⊢ ‖Norm.norm (E := ℂ) 0 / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
have pos : 0 ≤ ‖a i‖ / p i ^ s.re
Tactic: simp only [norm_zero, zero_div]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : 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' : (i : ι) → ℂ := 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 : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : ¬p i = 0
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
have this₁ : 0 ≤ p i
Tactic: have := hp i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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' : (i : ι) → ℂ := fun (i : ι) ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this_1 :
  ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * (↑(rexp (-π * p i * t)) : ℂ)) = a' i * (↑(rexp (-π * p i * t)) : ℂ)
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a' i * (↑(rexp (-π * p i * t)) : ℂ)) (F t)
i : ι
h : ¬p i = 0
this : 0 ≤ p i
⊢ ‖‖a i‖ / p i ^ s.re‖ ≤ ‖a i‖ / p i ^ s.re
have neg : ‖a i‖ / p i ^ s.re ≤ ‖a i‖ / p i ^ s.re
Tactic: rw [norm_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
⊢ 0 < (s / 2).re
have rw : 0 < s.re / 2
Tactic: rw [div_ofNat_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (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))
have hs' : 0 < (s / 2).re
Tactic: have hs' : 0 < (s / 2).re := by rw [div_ofNat_re]; positivity
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (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))
have hF₁ : ∀ (t : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) t →
    HasSum
      (fun (i : ι) ↦
        if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
Tactic: simp_rw [← sq_eq_zero_iff (a := r _)] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
⊢ HasSum (fun (i : ι) ↦ s.Gammaℝ * a i / (↑|r i| : ℂ) ^ s) (mellin F (s / 2))
have h : ∀ (i : ι), s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
Tactic: convert! hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
h : ∀ (i : ι), s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
⊢ HasSum (fun (i : ι) ↦ s.Gammaℝ * a i / (↑|r i| : ℂ) ^ s) (mellin F (s / 2))
have h₁ : ∀ (i : ι), (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)
Tactic: convert! hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : 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 : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum
        (fun (i : ι) ↦
          if HPow.hPow (β := ℕ) (r i) 2 = 0 then 0 else a i * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
        (F t)
h : ∀ (i : ι), s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
h₁ : ∀ (i : ι), (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)
⊢ HasSum (fun (i : ι) ↦ s.Gammaℝ * a i / (↑|r i| : ℂ) ^ s) (mellin F (s / 2))
have convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re
Tactic: convert! hasSum_mellin_pi_mul₀ (fun i ↦ sq_nonneg (r i)) hs' hF ?_ using 3 with i