awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
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
⊢ 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

Tactic:
rw [MellinConvergent]

Premises used: MellinConvergent
-- Module: Mathlib.Analysis.MellinTransform
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

Tactic:
integrableOn_congr_fun (fun t ht => ?_) measurableSet_Ioi

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_Ioi
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
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)
⊢ 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:
refine integrableOn_congr_fun (fun t ht => ?_) measurableSet_Ioi

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_Ioi
-- Module: Mathlib.Analysis.MellinTransform
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)
rw₁₂ rw₁₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - 1) • f (t ^ a)
⊢ (↑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]

Premises used: Iff.mpr, add_sub_assoc, Complex.cpow_mul_ofReal_nonneg, mul_sub, Complex.ofReal_cpow, HSub.hSub, le_of_lt, Complex.ofReal_ne_zero, ne_of_gt, Complex.ofReal_one, add_comm, mul_div_cancel₀, HPow.hPow, Complex.coe_smul, Complex.cpow_add, Complex.ofReal_sub, mul_one, OfNat.ofNat, sub_add_cancel, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.MellinTransform
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)

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun, mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
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
⊢ mellin (fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) s = mellin f (s + a)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
𝕜 : Type u_2
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ mellin (fun (t : ℝ) ↦ c • f t) s = c • mellin f s

Tactic:
simp only [mellin, smul_comm, integral_smul]

Premises used: MeasureTheory.integral_smul, SMulCommClass.smul_comm, mellin
-- Module: Mathlib.Analysis.MellinTransform
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
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

Tactic:
simp_rw [mellin, smul_eq_mul, ← mul_div_assoc, integral_div]

Premises used: MeasureTheory.integral_div, mul_div_assoc, smul_eq_mul, mellin
-- Module: Mathlib.Analysis.MellinTransform
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 : ℂ)))
inr : ∀ (ha : a ≠ 0), mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))
⊢ mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))

Tactic:
rcases eq_or_ne a 0 with rfl | ha

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
pos :
  ∀ (hE : CompleteSpace E),
    mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
neg :
  ∀ (hE : ¬CompleteSpace E),
    mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
⊢ mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : CompleteSpace E
⊢ mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))

Tactic:
simp [integral_smul_const, mellin, setIntegral_Ioi_zero_cpow]

Premises used: setIntegral_Ioi_zero_cpow, integral_smul_const, mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hE : ¬CompleteSpace E
⊢ mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))

Tactic:
simp [integral, mellin, hE]

Premises used: MeasureTheory.integral, mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
inr :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (t ^ a)) =
    HSMul.hSMul (β := E) |a|⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s / (↑a : ℂ) - 1) • f t)
⊢ mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))

Tactic:
simp_rw [mellin]

Premises used: mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
rw :
  @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
    |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a)
| HSMul.hSMul (β := E) |a|⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s / (↑a : ℂ) - 1) • f t)

Tactic:
rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]

Premises used: MeasureTheory.integral_smul, MeasureTheory.integral_comp_rpow_Ioi
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
inr :
  Eq.{u_1 + 1} (α := E)
    (@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 (a_1 : ℝ) ↦
      |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (t ^ a)) =
    HSMul.hSMul (β := E) |a|⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s / (↑a : ℂ) - 1) • f t)

Tactic:
conv_rhs => rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]

Premises used: MeasureTheory.integral_smul, MeasureTheory.integral_comp_rpow_Ioi
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := E)
    (@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 (a_1 : ℝ) ↦
      |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a))

Tactic:
setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
inr :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
    (↑t : ℂ) ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
⊢ Eq.{u_1 + 1} (α := E)
    (@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 (a_1 : ℝ) ↦
      |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a))

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_

Premises used: measurableSet_Ioi, MeasureTheory.setIntegral_congr_fun
-- Module: Mathlib.Analysis.MellinTransform
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
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)

Tactic:
rw [← mul_smul, ← mul_assoc, inv_mul_cancel₀ (mt abs_eq_zero.1 ha), one_mul, ← smul_assoc,
    real_smul]

Premises used: Complex.real_smul, smul_assoc, mul_assoc, mt, inv_mul_cancel₀, SemigroupAction.mul_smul, one_mul
-- Module: Mathlib.Analysis.MellinTransform
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
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₅ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
inr₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
inr₇ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + ((↑a : ℂ) - 1)) • f (t ^ a)
inr₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + (↑a : ℂ) - 1) • f (t ^ a)
inr₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + (↑a : ℂ) - 1) • f (t ^ a)
inr₁₀ inr₁₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - 1) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)

Tactic:
rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (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), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]

Premises used: Iff.mpr, add_sub_assoc, Complex.cpow_mul_ofReal_nonneg, mul_sub, Complex.ofReal_cpow, le_of_lt, Complex.ofReal_ne_zero, ne_of_gt, Complex.ofReal_one, add_comm, mul_div_cancel₀, Complex.cpow_add, Complex.ofReal_sub, mul_one, sub_add_cancel
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
simp_rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (a * t)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
⊢ mellin (fun (t : ℝ) ↦ f (a * t)) s = (↑a : ℂ) ^ (-s) • mellin f s

Tactic:
simp_rw [mellin]

Premises used: mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
dsimp : (↑t : ℂ) ^ (s - 1) • f (a * t) = (↑a : ℂ) ^ (1 - s) • (↑(a * t) : ℂ) ^ (s - 1) • f (a * t)
⊢ Eq.{u_1 + 1} (α := E) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) t)
    ((fun (t : ℝ) ↦ HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * t))) t)

Tactic:
dsimp only
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ 1 - s = -(s - 1)

Tactic:
ring
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : (↑a : ℂ) ^ (s - 1) ≠ 0
⊢ (↑t : ℂ) ^ (s - 1) • f (a * t) = (↑a : ℂ) ^ (1 - s) • (↑(a * t) : ℂ) ^ (s - 1) • f (a * t)

Tactic:
rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul,
      (by ring : 1 - s = -(s - 1)), cpow_neg, inv_mul_cancel_left₀]

Premises used: inv_mul_cancel_left₀, le_of_lt, Complex.cpow_neg, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, SemigroupAction.mul_smul, Complex.ofReal_mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
h : ¬a = 0 ∨ ¬s - 1 ≠ 0
⊢ (↑a : ℂ) ^ (s - 1) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or]

Premises used: Complex.cpow_eq_zero_iff, Ne, Complex.ofReal_eq_zero, not_and_or
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ¬a = 0 ∨ ¬s - 1 ≠ 0

Tactic:
Or.inl ha.ne'

Premises used: LT.lt.ne', Or.inl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ ¬a = 0 ∨ ¬s - 1 ≠ 0

Tactic:
exact Or.inl ha.ne'

Premises used: LT.lt.ne', Or.inl
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ EqOn.{0, u_1} (β := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
    (fun (t : ℝ) ↦ HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * t))) (Ioi 0)

Tactic:
have : EqOn (fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t))
      (fun t : ℝ => (a : ℂ) ^ (1 - s) • (fun u : ℝ => (u : ℂ) ^ (s - 1) • f u) (a * t))
        (Ioi 0) := fun t ht ↦ by
    dsimp only
    rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul,
      (by ring : 1 - s = -(s - 1)), cpow_neg, inv_mul_cancel_left₀]
    rw [Ne, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or]
    exact Or.inl ha.ne'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ mellin (fun (t : ℝ) ↦ f (t * a)) s = (↑a : ℂ) ^ (-s) • mellin f s

Tactic:
simpa only [mul_comm] using mellin_comp_mul_left f s ha

Premises used: mul_comm, mellin_comp_mul_left
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
simp_rw : mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t (-1))) s = mellin f (-s)
simp_rw₁ : HSMul.hSMul (α := ℝ) |(-1)|⁻¹ (mellin f (s / (↑(-1) : ℂ))) = mellin f (-s)
simp_rw₂ : HSMul.hSMul (α := ℝ) |1|⁻¹ (mellin f (s / (↑(-1) : ℂ))) = mellin f (-s)
simp_rw₃ : HSMul.hSMul (α := ℝ) 1⁻¹ (mellin f (s / (↑(-1) : ℂ))) = mellin f (-s)
simp_rw₄ : HSMul.hSMul (α := ℝ) 1 (mellin f (s / (↑(-1) : ℂ))) = mellin f (-s)
simp_rw₅ : mellin f (s / (↑(-1) : ℂ)) = mellin f (-s)
simp_rw₆ : mellin f (s / -(↑1 : ℂ)) = mellin f (-s)
simp_rw₇ : mellin f (s / -1) = mellin f (-s)
simp_rw₈ : mellin f (-(s / 1)) = mellin f (-s)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)

Tactic:
simp_rw [← rpow_neg_one, mellin_comp_rpow _ _ _, abs_neg, abs_one,
    inv_one, one_smul, ofReal_neg, ofReal_one, div_neg, div_one]

Premises used: abs_neg, Real.rpow_neg_one, inv_one, Complex.ofReal_neg, Complex.ofReal_one, one_smul, mellin_comp_rpow, div_neg, abs_one, div_one
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f t + g t) s

Tactic:
simpa only [MellinConvergent, smul_add] using hf.add hg

Premises used: MeasureTheory.IntegrableOn.add, MellinConvergent, smul_add
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ mellin (fun (t : ℝ) ↦ f t + g t) s = mellin f s + mellin g s

Tactic:
simpa only [mellin, smul_add] using integral_add hf hg

Premises used: mellin, MeasureTheory.integral_add, smul_add
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f t - g t) s

Tactic:
simpa only [MellinConvergent, smul_sub] using hf.sub hg

Premises used: MeasureTheory.IntegrableOn.sub, smul_sub, MellinConvergent
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f g : ℝ → E
s : ℂ
hf : MellinConvergent f s
hg : MellinConvergent g s
⊢ mellin (fun (t : ℝ) ↦ f t - g t) s = mellin f s - mellin g s

Tactic:
simpa only [mellin, smul_sub] using integral_sub hf hg

Premises used: MeasureTheory.integral_sub, smul_sub, mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hf : MellinConvergent f s
R : Type u_2
inst_2 : NormedRing R
inst_3 : Module R E
inst_4 : IsBoundedSMul R E
inst_5 : SMulCommClass ℂ R E
c : R
⊢ mellin (fun (t : ℝ) ↦ c • f t) s = c • mellin f s

Tactic:
simp [mellin, smul_comm, hf.integral_smul]

Premises used: MeasureTheory.Integrable.integral_smul, SMulCommClass.smul_comm, mellin
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)

Tactic:
((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul
      (hfc.mono_set hT)

Premises used: continuousOn_of_forall_continuousAt, MeasureTheory.AEStronglyMeasurable.mono_set, ContinuousOn.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
refine : ∀ x ∈ T, ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1)) x
⊢ AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)

Tactic:
refine ((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul
      (hfc.mono_set hT)

Premises used: continuousOn_of_forall_continuousAt, MeasureTheory.AEStronglyMeasurable.mono_set, ContinuousOn.aestronglyMeasurable, MeasureTheory.AEStronglyMeasurable.smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
s : ℂ
⊢ ∀ x ∈ T, ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1)) x

Tactic:
fun t ht => continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt (hT ht))

Premises used: HSub.hSub, ne_of_gt, OfNat.ofNat, Or.inr, Complex.continuousAt_ofReal_cpow_const