awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
hc : c ≠ 0
⊢ LSeriesSummable (c • f) s ↔ LSeriesSummable f s

Tactic:
⟨of_smul hc, smul c⟩

Premises used: LSeriesSummable.smul, LSeriesSummable.of_smul, Iff.intro
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
f : ℕ → ℂ
c s : ℂ
⊢ LSeries (c • f) s = c * LSeries f s

Tactic:
simp [LSeries, term_smul_apply, tsum_mul_left]

Premises used: tsum_mul_left, LSeries, LSeries.term_smul_apply
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
inl : ∀ (hn : n = 0), term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
inr : ∀ (hn : n ≠ 0), term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

Tactic:
rcases eq_or_ne n 0 with hn | hn

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
hn : n = 0
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

Tactic:
simp [hn, Finset.sum_div]

Premises used: Finset.sum_div
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ term (∑ i ∈ S, f i) s n = ∑ i ∈ S, term (f i) s n

Tactic:
simp [hn, Finset.sum_div]

Premises used: Finset.sum_div
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
x : ℕ
⊢ term (∑ i ∈ S, f i) s x = (∑ i ∈ S, term (f i) s) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
a : ι → ℂ
hf : ∀ i ∈ S, LSeriesHasSum (f i) s (a i)
⊢ LSeriesHasSum (∑ i ∈ S, f i) s (∑ i ∈ S, a i)

Tactic:
simpa [LSeriesHasSum, term_sum, Finset.sum_fn S fun i ↦ term (f i) s] using hasSum_sum hf

Premises used: LSeries.term_sum, hasSum_sum, LSeriesHasSum, Finset.sum_fn, LSeries.term
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeriesSummable (∑ i ∈ S, f i) s

Tactic:
simpa [LSeriesSummable, ← term_sum_apply] using summable_sum hf

Premises used: summable_sum, LSeries.term_sum_apply, LSeriesSummable
-- Module: Mathlib.NumberTheory.LSeries.Linearity
Goal:
ι : Type u_1
f : ι → ℕ → ℂ
S : Finset ι
s : ℂ
hf : ∀ i ∈ S, LSeriesSummable (f i) s
⊢ LSeries (∑ i ∈ S, f i) s = ∑ i ∈ S, LSeries (f i) s

Tactic:
simpa [LSeries, term_sum] using Summable.tsum_finsetSum hf

Premises used: LSeries.term_sum, LSeries, Summable.tsum_finsetSum
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
simp_rw :
  HasSum (α := ℂ) (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∑' (x_1 : ι), (↑x : ℂ) ^ (s - 1) * (a x_1 * (↑(rexp (-p x_1 * x)) : ℂ)))
⊢ HasSum (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s) (mellin F s)

Tactic:
simp_rw [mellin, smul_eq_mul, ← setIntegral_congr_fun measurableSet_Ioi
    (fun t ht ↦ congr_arg _ (hF t ht).tsum_eq), ← tsum_mul_left]

Premises used: tsum_mul_left, measurableSet_Ioi, congr_arg, MeasureTheory.setIntegral_congr_fun, HasSum.tsum_eq, smul_eq_mul, mellin
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
⊢ HasSum (α := ℂ)
    (fun (x : ι) ↦
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) x a_1)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      ∑' (i : ι), (fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)

Tactic:
hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t)))
      (fun i ↦ ?_) ?_

Premises used: MeasureTheory.hasSum_integral_of_summable_integral_norm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
h :
  ∀ (i : ι),
    Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (↑a_1 : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * a_1)) : ℂ))
convert_3 :
  ∀ (i : ι),
    @Integrable ℂ _ _ ℝ Real.measurableSpace
      ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i)
      (Measure.restrict volume (Ioi 0))
convert_4 :
  Summable (α := ℝ) fun (i : ι) ↦
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)
⊢ HasSum (α := ℂ) (fun (i : ι) ↦ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      ∑' (x_1 : ι), (↑x : ℂ) ^ (s - 1) * (a x_1 * (↑(rexp (-p x_1 * x)) : ℂ)))

Tactic:
convert!
    hasSum_integral_of_summable_integral_norm (F := fun i t ↦ t ^ (s - 1) * (a i * rexp (-p i * t)))
      (fun i ↦ ?_) ?_ using
    2 with i

Premises used: MeasureTheory.hasSum_integral_of_summable_integral_norm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
⊢ Complex.Gamma s * a i / (↑(p i) : ℂ) ^ s =
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      (↑a_1 : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * a_1)) : ℂ))

Tactic:
simp_rw [← mul_assoc, mul_comm _ (a _), mul_assoc (a _), mul_div_assoc, integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, mul_assoc, mul_div_assoc, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
      a i *
        @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
h₁ :
  ∀ (hpi : 0 < p i),
    a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
      a i *
        @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
          (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)

Tactic:
rcases hp i with hai | hpi
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 : ι
hai : a i = 0
h :
  0 * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    HMul.hMul (α := ℂ) 0
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
h₁ :
  0 =
    HMul.hMul (α := ℂ) 0
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ))
h₂ h₃ : Eq (α := ℂ) 0 0
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)

Tactic:
rw [hai, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * cexp (-((↑(p i) : ℂ) * (↑t : ℂ)))) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s

Tactic:
have := integral_cpow_mul_exp_neg_mul_Ioi hs hpi
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 - 1) * cexp (-((↑(p i) : ℂ) * (↑t : ℂ)))) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s

Tactic:
simp_rw [← ofReal_mul, ← ofReal_neg, ← ofReal_exp, ← neg_mul (p i)] at this

Premises used: Complex.ofReal_neg, Complex.ofReal_exp, neg_mul, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 - 1) * (↑(rexp (-p i * t)) : ℂ)) =
    (1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s
h : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((1 / (↑(p i) : ℂ)) ^ s * Complex.Gamma s)
h₁ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * ((↑(p i) : ℂ)⁻¹ ^ s * Complex.Gamma s)
h₂ : a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) = a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s)
h₃ h₄ : a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s) = a i * (((↑(p i) : ℂ) ^ s)⁻¹ * Complex.Gamma s)
⊢ a i * (Complex.Gamma s / (↑(p i) : ℂ) ^ s) =
    a i *
      @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a : ℝ) ↦
        (↑a : ℂ) ^ (s - 1) * (↑(rexp (-p i * a)) : ℂ)

Tactic:
rw [this, one_div, inv_cpow _ _ (arg_ofReal_of_nonneg hpi.le ▸ pi_pos.ne), div_eq_inv_mul]

Premises used: Complex.inv_cpow, one_div, div_eq_inv_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 : ι
convert_3 :
  ∀ (hai : a i = 0),
    @Integrable ℂ _ _ ℝ Real.measurableSpace
      ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i)
      (Measure.restrict volume (Ioi 0))
convert_3₁ :
  ∀ (hpi : 0 < p i),
    @Integrable ℂ _ _ ℝ Real.measurableSpace
      ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i)
      (Measure.restrict volume (Ioi 0))
⊢ @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))

Tactic:
rcases hp i with hai | hpi
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 : ι
hai : a i = 0
⊢ @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))

Tactic:
simp [hai]
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
convert_3 :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
    (Measure.restrict volume (Ioi 0))
⊢ @Integrable ℂ _ _ ℝ Real.measurableSpace
    ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i) (Measure.restrict volume (Ioi 0))

Tactic:
simp_rw [← mul_assoc, mul_comm _ (a i), mul_assoc]

Premises used: mul_assoc, mul_comm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Ioi 0) volume

Tactic:
have := Complex.GammaIntegral_convergent hs
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Ioi 0) volume
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume

Tactic:
rw [← mul_zero (p i), ← integrableOn_Ioi_comp_mul_left_iff _ _ hpi] at this

Premises used: MeasureTheory.integrableOn_Ioi_comp_mul_left_iff, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
    (Measure.restrict volume (Ioi 0))

Tactic:
(IntegrableOn.congr_fun (this.const_mul (1 / p i ^ (s - 1)))
      (fun t (ht : 0 < t) ↦ ?_) measurableSet_Ioi).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, HSub.hSub, HDiv.hDiv, measurableSet_Ioi, Complex.ofReal, HPow.hPow, OfNat.ofNat, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
convert_3 :
  ∀ (t : ℝ) (ht : 0 < t),
    1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(rexp (-(p i * t))) : ℂ) * (↑(p i * t) : ℂ) ^ (s - 1)) =
      (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ a i * ((↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)))
    (Measure.restrict volume (Ioi 0))

Tactic:
refine (IntegrableOn.congr_fun (this.const_mul (1 / p i ^ (s - 1)))
      (fun t (ht : 0 < t) ↦ ?_) measurableSet_Ioi).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, HSub.hSub, HDiv.hDiv, measurableSet_Ioi, Complex.ofReal, HPow.hPow, OfNat.ofNat, MeasureTheory.IntegrableOn.congr_fun
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
convert_3 :
  1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(p i) : ℂ) * (↑t : ℂ)) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ) =
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ)
⊢ 1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(rexp (-(p i * t))) : ℂ) * (↑(p i * t) : ℂ) ^ (s - 1)) =
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-p i * t)) : ℂ)

Tactic:
simp_rw [mul_comm (↑(rexp _) : ℂ), ← mul_assoc, neg_mul, ofReal_mul]

Premises used: mul_assoc, Real.exp, Complex.ofReal, mul_comm, neg_mul, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
convert_3 : (↑(p i) : ℂ) ^ (s - 1) ≠ 0
⊢ 1 / (↑(p i) : ℂ) ^ (s - 1) * ((↑(p i) : ℂ) * (↑t : ℂ)) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ) =
    (↑t : ℂ) ^ (s - 1) * (↑(rexp (-(p i * t))) : ℂ)

Tactic:
rw [mul_cpow_ofReal_nonneg hpi.le ht.le, ← mul_assoc, one_div, inv_mul_cancel₀, one_mul]

Premises used: mul_assoc, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, one_div, inv_mul_cancel₀, one_mul
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
convert_3 : ¬(↑(p i) : ℂ) = 0 ∨ ¬s - 1 ≠ 0
⊢ (↑(p i) : ℂ) ^ (s - 1) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or]

Premises used: Complex.cpow_eq_zero_iff, Ne, not_and_or
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ ¬(↑(p i) : ℂ) = 0 ∨ ¬s - 1 ≠ 0

Tactic:
Or.inl (ofReal_ne_zero.mpr hpi.ne')

Premises used: Iff.mpr, Complex.ofReal_ne_zero, LT.lt.ne', Or.inl
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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 :
  IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-(p i * x))) : ℂ) * (↑(p i * x) : ℂ) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ ¬(↑(p i) : ℂ) = 0 ∨ ¬s - 1 ≠ 0

Tactic:
exact Or.inl (ofReal_ne_zero.mpr hpi.ne')

Premises used: Iff.mpr, Complex.ofReal_ne_zero, LT.lt.ne', Or.inl
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
convert_4 :
  Summable (α := ℝ) fun (a_1 : ι) ↦
    Norm.norm (E := ℝ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_2 : ℝ) ↦
        Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) a_1 a_2))
⊢ Summable (α := ℝ) fun (i : ι) ↦
    @integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      Norm.norm (E := ℂ) ((fun (i : ι) (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) * (a i * (↑(rexp (-p i * t)) : ℂ))) i a_1)

Tactic:
apply Summable.of_norm

Premises used: Summable.of_norm
-- Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet
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
⊢ Summable (α := ℝ) fun (i : ι) ↦ Real.Gamma s.re * (‖a i‖ / p i ^ s.re)

Tactic:
h_sum.mul_left (Real.Gamma s.re)

Premises used: Complex.re, Summable.mul_left, Real.Gamma