awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
i : ι
⊢ s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
have h : s.Gammaℝ * a i = (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i
Tactic: rw [← neg_div, Gammaℝ_def]
-- 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)
i : ι
h : s.Gammaℝ * a i = (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i
⊢ s.Gammaℝ * a i = (↑π : ℂ) ^ (-(s / 2)) * Complex.Gamma (s / 2) * a i
have h₁ : (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i = (↑π : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) * a i
Tactic: rw [← neg_div, Gammaℝ_def]
-- 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)
i : ι
⊢ (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)
have h : (↑|r i| : ℂ) ^ s = (↑|r i| : ℂ) ^ ((↑2 : ℂ) * (s / 2))
Tactic: rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']
-- 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)
i : ι
h : (↑|r i| : ℂ) ^ s = (↑|r i| : ℂ) ^ ((↑2 : ℂ) * (s / 2))
⊢ (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)
have h₁ : -π < (↑2 : ℝ) * (↑|r i| : ℂ).arg
Tactic: rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']
-- 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)
i : ι
h : (↑|r i| : ℂ) ^ s = (↑|r i| : ℂ) ^ ((↑2 : ℂ) * (s / 2))
h₁ : -π < (↑2 : ℝ) * (↑|r i| : ℂ).arg
⊢ (↑|r i| : ℂ) ^ s = (↑(HPow.hPow (β := ℕ) (r i) 2) : ℂ) ^ (s / 2)
have h₂ : (↑2 : ℝ) * (↑|r i| : ℂ).arg ≤ π
Tactic: rw [← sq_abs, ofReal_pow, ← cpow_nat_mul']
-- 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)
i : ι
⊢ -π < (↑2 : ℝ) * (↑|r i| : ℂ).arg
have h : -π < HMul.hMul (α := ℝ) (↑2 : ℝ) 0
Tactic: rw [arg_ofReal_of_nonneg (abs_nonneg _)]
-- 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)
i : ι
⊢ -π < HMul.hMul (α := ℝ) (↑2 : ℝ) 0
have linarith : HMul.hMul (α := ℝ) (↑2 : ℝ) 0 ≤ -π → HMul.hMul (α := ℝ) (↑2 : ℝ) 0 - -π + (0 - π) = 0
Tactic: linarith [pi_pos]
-- 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)
i : ι
⊢ (↑2 : ℝ) * (↑|r i| : ℂ).arg ≤ π
have h : HMul.hMul (α := ℝ) (↑2 : ℝ) 0 ≤ π
Tactic: rw [arg_ofReal_of_nonneg (abs_nonneg _)]
-- 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)
i : ι
⊢ HMul.hMul (α := ℝ) (↑2 : ℝ) 0 ≤ π
have linarith : π < HMul.hMul (α := ℝ) (↑2 : ℝ) 0 → π - HMul.hMul (α := ℝ) (↑2 : ℝ) 0 + (0 - π) = 0
Tactic: linarith [pi_pos]
-- 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)
⊢ Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re
have h : ∀ (i : ι), HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
Tactic: convert! h_sum 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)
i : ι
⊢ HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
have h : HPow.hPow (β := ℕ) |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']
-- 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)
i : ι
h : HPow.hPow (β := ℕ) |r i| 2 ^ (s / 2).re = |r i| ^ s.re
⊢ HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
have h₁ : |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']
-- 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)
i : ι
h : HPow.hPow (β := ℕ) |r i| 2 ^ (s / 2).re = |r i| ^ s.re
h₁ : |r i| ^ ((↑2 : ℝ) * (s / 2).re) = |r i| ^ s.re
⊢ HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
have h₂ : |r i| ^ ((↑2 : ℝ) * (s.re / 2)) = |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']
-- 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)
i : ι
h : HPow.hPow (β := ℕ) |r i| 2 ^ (s / 2).re = |r i| ^ s.re
h₁ : |r i| ^ ((↑2 : ℝ) * (s / 2).re) = |r i| ^ s.re
h₂ : |r i| ^ ((↑2 : ℝ) * (s.re / 2)) = |r i| ^ s.re
⊢ HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
have h₃ : |r i| ^ (2 * (s.re / 2)) = |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']
-- 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)
i : ι
h : HPow.hPow (β := ℕ) |r i| 2 ^ (s / 2).re = |r i| ^ s.re
h₁ : |r i| ^ ((↑2 : ℝ) * (s / 2).re) = |r i| ^ s.re
h₂ : |r i| ^ ((↑2 : ℝ) * (s.re / 2)) = |r i| ^ s.re
h₃ : |r i| ^ (2 * (s.re / 2)) = |r i| ^ s.re
⊢ HPow.hPow (β := ℕ) (r i) 2 ^ (s / 2).re = |r i| ^ s.re
have h₄ : |r i| ^ s.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']
-- 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 : ι) ↦ a i * (↑(r 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 + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
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 (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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
have hs₂ : 0 < (s + 1).re
Tactic: have hs₂ : 0 < (s + 1).re := by rw [add_re, one_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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
have hs₃ : s + 1 ≠ 0
Tactic: have hs₃ : s + 1 ≠ 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 : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
⊢ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
    if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
have pos : ∀ (h : r i = 0), a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) = 0
Tactic: split_ifs with h
-- 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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
i : ι
t : ℝ
pos : ∀ (h : r i = 0), a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) = 0
⊢ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
    if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
have neg : ∀ (h : ¬r i = 0),
  a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
Tactic: split_ifs with h
-- 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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
have this : ∀ (i : ι) (t : ℝ),
  a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
    if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
Tactic: have (i t : _) : (a i * r i * rexp (-π * r i ^ 2 * t)) =
      if r i = 0 then 0 else (a i * r i * rexp (-π * r i ^ 2 * t)) := by
    split_ifs with h <;> simp [h]
-- 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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
| ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t) (i : ι),
  a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
Tactic: enter [t, ht, 1, 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
hF :
  ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
i : ι
| a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
have h : if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
Tactic: rw [this]
-- 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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
| ∀ (t : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) t →
      HasSum (fun (i : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t) (i : ι),
  if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
Tactic: enter [t, ht, 1, i]; rw [this]
-- 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 : ι) ↦ a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
have hF₁ : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  HasSum (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
    (F t)
Tactic: conv at hF => enter [t, ht, 1, i]; rw [this]
Cleared hypotheses: hF, h_sum, hs₁, hs₂, hs₃, this
-- 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 : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
have h : ∀ (i : ι),
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
Tactic: convert! hasSum_mellin_pi_mul_sq hs₂ hF ?_ using 2 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
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
h :
  ∀ (i : ι),
    (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
      (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
⊢ HasSum (fun (i : ι) ↦ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s)
    (mellin F ((s + 1) / 2))
have convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a i * (↑(r i) : ℂ)‖ / |r i| ^ (s + 1).re
Tactic: convert! hasSum_mellin_pi_mul_sq hs₂ hF ?_ using 2 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
hF :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
i : ι
⊢ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
have h : ∀ (h : r i = 0),
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
Tactic: rcases eq_or_ne (r i) 0 with h | h
-- 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 : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    HasSum
      (fun (i : ι) ↦ if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ))
      (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ) =
      if r i = 0 then 0 else a i * (↑(r i) : ℂ) * (↑(rexp (-π * HPow.hPow (β := ℕ) (r i) 2 * t)) : ℂ)
i : ι
h :
  ∀ (h : r i = 0),
    (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
      (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
⊢ (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
have h₁ : ∀ (h : r i ≠ 0),
  (s + 1).Gammaℝ * a i * (↑((SignType.sign : (a : ℝ) → SignType) (r i)) : ℂ) / (↑|r i| : ℂ) ^ s =
    (s + 1).Gammaℝ * (a i * (↑(r i) : ℂ)) / (↑|r i| : ℂ) ^ (s + 1)
Tactic: rcases eq_or_ne (r i) 0 with h | h