awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → HasSum (fun (i : ι) ↦ a i * (↑(rexp (-p i * t)) : ℂ)) (F t)
h_sum : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / p i ^ s.re
i : ι
h :
  ∀ (hai : a i = 0),
    ‖a i‖ *
        Norm.norm (E := ℝ)
          (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
            ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
      ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
⊢ ‖a i‖ *
      Norm.norm (E := ℝ)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
have h₁ : ∀ (hpi : 0 < p i),
  ‖a i‖ *
      Norm.norm (E := ℝ)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
Tactic: rcases hp i with hai | hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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‖ *
      Norm.norm (E := ℝ)
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    ‖a i‖ * (Real.Gamma s.re / p i ^ s.re)
have h : Norm.norm (E := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
      ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
  Real.Gamma s.re / p i ^ s.re
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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
⊢ Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    Real.Gamma s.re / p i ^ s.re
have this : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    t ^ (s.re - 1) * rexp (-(p i * t))) =
  (1 / p i) ^ s.re * Real.Gamma s.re
Tactic: have := Real.integral_rpow_mul_exp_neg_mul_Ioi hs hpi
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (hypothesis)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-(p i * t))) =
    (1 / p i) ^ s.re * Real.Gamma s.re
⊢ Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    Real.Gamma s.re / p i ^ s.re
have this₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    t ^ (s.re - 1) * rexp (-p i * t)) =
  Real.Gamma s.re / p i ^ s.re
Tactic: simp_rw [← neg_mul (p i), one_div, inv_rpow hpi.le, ← div_eq_inv_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
⊢ Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        ‖(↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)‖) =
    Real.Gamma s.re / p i ^ s.re
have h : Eq (α := ℝ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    ‖(↑x : ℂ) ^ (s - 1) * (↑(rexp (-p i * x)) : ℂ)‖)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    t ^ (s.re - 1) * rexp (-p i * t))
Tactic: rw [norm_of_nonneg (integral_nonneg (fun _ ↦ norm_nonneg _)), ← this]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ‖(↑x : ℂ) ^ (s - 1) * (↑(rexp (-p i * x)) : ℂ)‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t))
have h : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h₂ : ‖(↑t : ℂ) ^ (s - 1)‖ * |rexp (-p i * t)| = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₂ : ‖(↑t : ℂ) ^ (s - 1)‖ * |rexp (-p i * t)| = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h₃ : ‖(↑t : ℂ) ^ (s - 1)‖ * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₂ : ‖(↑t : ℂ) ^ (s - 1)‖ * |rexp (-p i * t)| = t ^ (s.re - 1) * rexp (-p i * t)
h₃ : ‖(↑t : ℂ) ^ (s - 1)‖ * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h₄ : t ^ (s - 1).re * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₂ : ‖(↑t : ℂ) ^ (s - 1)‖ * |rexp (-p i * t)| = t ^ (s.re - 1) * rexp (-p i * t)
h₃ : ‖(↑t : ℂ) ^ (s - 1)‖ * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
h₄ : t ^ (s - 1).re * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h₅ : t ^ (s.re - re 1) * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.MellinEqDirichlet (goal)
Goal:
ι : Type u_1
inst : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) t → 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 :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      t ^ (s.re - 1) * rexp (-p i * t)) =
    Real.Gamma s.re / p i ^ s.re
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖(↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₁ : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖rexp (-p i * t)‖ = t ^ (s.re - 1) * rexp (-p i * t)
h₂ : ‖(↑t : ℂ) ^ (s - 1)‖ * |rexp (-p i * t)| = t ^ (s.re - 1) * rexp (-p i * t)
h₃ : ‖(↑t : ℂ) ^ (s - 1)‖ * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
h₄ : t ^ (s - 1).re * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
h₅ : t ^ (s.re - re 1) * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
⊢ ‖(↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)‖ = t ^ (s.re - 1) * rexp (-p i * t)
have h₆ : t ^ (s.re - 1) * rexp (-p i * t) = t ^ (s.re - 1) * rexp (-p i * t)
Tactic: rw [norm_mul, norm_real, Real.norm_eq_abs, Real.abs_exp,
      norm_cpow_eq_rpow_re_of_pos ht, sub_re, one_re]
-- 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
i : ι
⊢ a i = 0 ∨ 0 < π * q i
have inl : ∀ (h : a i = 0), a i = 0 ∨ 0 < π * q i
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
i : ι
inl : ∀ (h : a i = 0), a i = 0 ∨ 0 < π * q i
⊢ a i = 0 ∨ 0 < π * q i
have inr : ∀ (h : 0 < q i), a i = 0 ∨ 0 < π * q i
Tactic: rcases hq i with h | h
-- 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
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s) (mellin F s)
have hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
Tactic: have hp i : a i = 0 ∨ 0 < π * q i := by rcases hq i with h | h <;> simp [h, pi_pos]
-- 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
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s) (mellin F s)
have h : ∀ (i : ι), (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s = Complex.Gamma s * a i / (↑(π * q i) : ℂ) ^ s
Tactic: convert! hasSum_mellin hp hs (by simpa using hF) ?_ using 2 with i
-- 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
h : ∀ (i : ι), (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s = Complex.Gamma s * a i / (↑(π * q i) : ℂ) ^ s
⊢ HasSum (fun (i : ι) ↦ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s) (mellin F s)
have convert! : Summable (α := ℝ) fun (i : ι) ↦ ‖a i‖ / (π * q i) ^ s.re
Tactic: convert! hasSum_mellin hp hs (by simpa using hF) ?_ using 2 with i
-- 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 = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inl : ∀ (h : a i = 0), a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
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 = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inr : ∀ (h : 0 < q i), a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
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 = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inr : a i / ((↑π : ℂ) * (↑(q i) : ℂ)) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
Tactic: rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← 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 / ((↑π : ℂ) * (↑(q i) : ℂ)) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inr₁ : a i / ((↑π : ℂ) ^ s * (↑(q i) : ℂ) ^ s) = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
Tactic: rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← 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 / ((↑π : ℂ) * (↑(q i) : ℂ)) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₁ : a i / ((↑π : ℂ) ^ s * (↑(q i) : ℂ) ^ s) = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inr₂ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
Tactic: rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← 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 / ((↑π : ℂ) * (↑(q i) : ℂ)) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₁ : a i / ((↑π : ℂ) ^ s * (↑(q i) : ℂ) ^ s) = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₂ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inr₃ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = ((↑π : ℂ) ^ s)⁻¹ * a i / (↑(q i) : ℂ) ^ s
Tactic: rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← 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 / ((↑π : ℂ) * (↑(q i) : ℂ)) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₁ : a i / ((↑π : ℂ) ^ s * (↑(q i) : ℂ) ^ s) = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₂ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
inr₃ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = ((↑π : ℂ) ^ s)⁻¹ * a i / (↑(q i) : ℂ) ^ s
⊢ a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
have inr₄ : a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s = a i / (↑π : ℂ) ^ s / (↑(q i) : ℂ) ^ s
Tactic: rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← 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
i : ι
⊢ (↑π : ℂ) ^ (-s) * Complex.Gamma s * a i / (↑(q i) : ℂ) ^ s = Complex.Gamma s * a i / (↑(π * q i) : ℂ) ^ s
have this : a i / (↑(π * q i) : ℂ) ^ s = (↑π : ℂ) ^ (-s) * a i / (↑(q i) : ℂ) ^ s
Tactic: have : a i / ↑(π * q i) ^ s = π ^ (-s) * a i / q i ^ s := by
      rcases hq i with h | h
      · simp [h]
      · rw [ofReal_mul, mul_cpow_ofReal_nonneg pi_pos.le h.le, ← div_div, cpow_neg,
          ← div_eq_inv_mul]