awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (t ^ a)) s ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ (a - 1) • (↑(x ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (x ^ a)) (Ioi 0) volume
have rw : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (t ^ a))
    (Ioi 0) volume ↔
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ x ^ (a - 1) • (↑(x ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (x ^ a)) (Ioi 0) volume
Tactic: rw [MellinConvergent]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (t ^ a))
      (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ x ^ (a - 1) • (↑(x ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (x ^ a)) (Ioi 0) volume
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
Tactic: refine integrableOn_congr_fun (fun t ht => ?_) measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₇ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₇ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₇ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
rw₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ))) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₇ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
rw₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
rw₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ))) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₁₀ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + ((↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₇ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
rw₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
rw₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ))) • f (t ^ a)
rw₁₀ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + ((↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₁₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + (↑a : ℂ) - 1) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
rw : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑(t ^ (a - 1)) : ℂ) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
rw₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₃ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
rw₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
rw₇ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
rw₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
rw₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ))) • f (t ^ a)
rw₁₀ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + ((↑a : ℂ) - 1)) • f (t ^ a)
rw₁₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + (↑a : ℂ) - 1) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = t ^ (a - 1) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have rw₁₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - 1) • f (t ^ a)
Tactic: rw [← Complex.coe_smul (t ^ (a - 1)), ← mul_smul, ← cpow_mul_ofReal_nonneg (le_of_lt ht),
    ofReal_cpow (le_of_lt ht), ← cpow_add _ _ (ofReal_ne_zero.mpr (ne_of_gt ht)), ofReal_sub,
    ofReal_one, mul_sub, mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), mul_one, add_comm, ←
    add_sub_assoc, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
⊢ mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) s = mellin f (s + a)
have refine : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  HSMul.hSMul (β := E) ((↑t : ℂ) ^ (s - 1)) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) t) = (↑t : ℂ) ^ (s + a - 1) • f t
Tactic: refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℂ
s a : ℂ
⊢ mellin (fun (t : ℝ) ↦ f t / a) s = mellin f s / a
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) • (f t / a)) =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t) /
    a
Tactic: simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℂ
s a : ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • (f t / a)) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t) /
      a
⊢ mellin (fun (t : ℝ) ↦ f t / a) s = mellin f s / a
have simp_rw₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) * (f t / a)) =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * f t) /
    a
Tactic: simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℂ
s a : ℂ
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • (f t / a)) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t) /
      a
simp_rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * (f t / a)) =
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) * f t) /
      a
⊢ mellin (fun (t : ℝ) ↦ f t / a) s = mellin f s / a
have simp_rw₂ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) * f t / a) =
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) * f t) /
    a
Tactic: simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
⊢ mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))
have inl : mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
Tactic: rcases eq_or_ne a 0 with rfl | ha
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
inl : mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
⊢ mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))
have inr : ∀ (ha : a ≠ 0), mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))
Tactic: rcases eq_or_ne a 0 with rfl | ha
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
have pos : ∀ (hE : CompleteSpace E),
  mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
Tactic: by_cases hE : CompleteSpace E