awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume

Tactic:
replace hFf : Integrable (𝓕 g) := by
    have h2π : 2 * π ≠ 0 := by simp
    have : Integrable (𝓕 (fun u ↦ rexp (-(σ * u)) • f (rexp (-u)))) := by
      simpa [mellin_eq_fourier, mul_div_cancel_right₀ _ h2π] using hFf.comp_mul_right' h2π
    simp_rw [neg_mul_eq_neg_mul] at this
    exact this
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
⊢ ContinuousAt (Y := ℝ) (fun (u : ℝ) ↦ rexp (-σ * u)) (-Real.log x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
⊢ ContinuousAt (Y := ℝ) (fun (u : ℝ) ↦ rexp (-u)) (-Real.log x)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
refine : ContinuousAt f (rexp (- -Real.log x))
⊢ ContinuousAt g (-Real.log x)

Tactic:
refine ContinuousAt.smul (by fun_prop) (ContinuousAt.comp ?_ (by fun_prop))

Premises used: ContinuousAt.smul, ContinuousAt.comp
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
⊢ ContinuousAt f (rexp (- -Real.log x))

Tactic:
simpa [Real.exp_log hx] using hfx

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
⊢ ContinuousAt g (-Real.log x)

Tactic:
replace hfx : ContinuousAt g (-Real.log x) := by
    refine ContinuousAt.smul (by fun_prop) (ContinuousAt.comp ?_ (by fun_prop))
    simpa [Real.exp_log hx] using hfx
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ mellinInv σ (mellin f) x = mellinInv σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) x

Tactic:
simp [g, mellinInv, mellin_eq_fourier]

Premises used: mellin_eq_fourier, mellinInv
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
rw :
  (↑x : ℂ) ^ (-(↑σ : ℂ)) •
      𝓕⁻ (E := (y : ℝ) → E) (fun (y : ℝ) ↦ 𝓕 g (((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I).im / (2 * π))) (-Real.log x) =
    (↑x : ℂ) ^ (-(↑σ : ℂ)) • 𝓕⁻ (𝓕 g) (-Real.log x)
⊢ mellinInv σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) x = (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-Real.log x)

Tactic:
rw [mellinInv_eq_fourierInv _ _ hx, ← hf.fourierInv_fourier_eq hFf hfx]

Premises used: MeasureTheory.Integrable.fourierInv_fourier_eq, mellinInv_eq_fourierInv
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ 2 * π ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ (↑x : ℂ) ^ (-(↑σ : ℂ)) •
      𝓕⁻ (E := (y : ℝ) → E) (fun (y : ℝ) ↦ 𝓕 g (((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I).im / (2 * π))) (-Real.log x) =
    (↑x : ℂ) ^ (-(↑σ : ℂ)) • 𝓕⁻ (𝓕 g) (-Real.log x)

Tactic:
simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by simp)]

Premises used: mul_div_cancel_left₀
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-Real.log x) = (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log x))

Tactic:
simp [g]
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
norm_cast : (↑x : ℂ) ^ (↑(-σ) : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x
⊢ (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x

Tactic:
norm_cast
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
rw : (↑(x ^ (-σ)) : ℂ) • x ^ σ • f x = f x
⊢ (↑x : ℂ) ^ (↑(-σ) : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x

Tactic:
rw [mul_comm σ, ← rpow_def_of_pos hx, Real.exp_log hx, ← Complex.ofReal_cpow hx.le]

Premises used: Real.rpow_def_of_pos, Complex.ofReal_cpow, LT.lt.le, Real.exp_log, mul_comm
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
norm_cast : x ^ (-σ) • x ^ σ • f x = f x
⊢ (↑(x ^ (-σ)) : ℂ) • x ^ σ • f x = f x

Tactic:
norm_cast
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
rw : (x ^ (-σ) • x ^ σ) • f x = f x
rw₁ : (x ^ (-σ) * x ^ σ) • f x = f x
rw₂ : ((x ^ σ)⁻¹ * x ^ σ) • f x = f x
rw₃ : HSMul.hSMul (α := ℝ) 1 (f x) = f x
rw₄ rw₅ : f x = f x
⊢ x ^ (-σ) • x ^ σ • f x = f x

Tactic:
rw [← smul_assoc, smul_eq_mul, Real.rpow_neg hx.le,
        inv_mul_cancel₀ (ne_of_gt (rpow_pos_of_pos hx σ)), one_smul]

Premises used: Real.rpow_pos_of_pos, smul_assoc, ne_of_gt, LT.lt.le, one_smul, smul_eq_mul, inv_mul_cancel₀, Real.rpow_neg
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
hFf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
mellinInv : _root_.mellinInv σ (mellin f) x = _root_.mellinInv σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) x
mellinInv₁ : _root_.mellinInv σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) x = (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-Real.log x)
mellinInv₂ :
  (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-Real.log x) = (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log x))
mellinInv₃ : (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x
⊢ _root_.mellinInv σ (mellin f) x = f x

Tactic:
calc
    mellinInv σ (mellin f) x
      = mellinInv σ (fun s ↦ 𝓕 g (s.im / (2 * π))) x := by
      simp [g, mellinInv, mellin_eq_fourier]
    _ = (x : ℂ) ^ (-σ : ℂ) • g (-Real.log x) := by
      rw [mellinInv_eq_fourierInv _ _ hx, ← hf.fourierInv_fourier_eq hFf hfx]
      simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by simp)]
    _ = (x : ℂ) ^ (-σ : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) := by simp [g]
    _ = f x := by
      norm_cast
      rw [mul_comm σ, ← rpow_def_of_pos hx, Real.exp_log hx, ← Complex.ofReal_cpow hx.le]
      norm_cast
      rw [← smul_assoc, smul_eq_mul, Real.rpow_neg hx.le,
        inv_mul_cancel₀ (ne_of_gt (rpow_pos_of_pos hx σ)), one_smul]

Premises used: Real.pi, HMul.hMul, mellinInv, Complex.im, HDiv.hDiv, Real.exp, Complex.ofReal, Real.log, FourierTransform.fourier, mellin, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
hf : MellinConvergent f s
𝕜 : Type u_2
inst_2 : NormedAddCommGroup 𝕜
inst_3 : SMulZeroClass 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
inst_5 : SMulCommClass ℂ 𝕜 E
c : 𝕜
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ c • f t) s

Tactic:
simpa only [MellinConvergent, smul_comm] using hf.smul c

Premises used: MeasureTheory.Integrable.smul, MellinConvergent, SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s a : ℂ
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) s ↔ MellinConvergent f (s + a)

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

Premises used: MeasureTheory.integrableOn_congr_fun, measurableSet_Ioi, MellinConvergent
-- 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) s ↔ MellinConvergent f (s + a)

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 : ℂ
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
simp_rw simp_rw₁ : (↑t : ℂ) ^ (s - 1) • (↑t : ℂ) ^ a • f t = (↑t : ℂ) ^ (s + a - 1) • f t
simp_rw₂ : (↑t : ℂ) ^ (s - 1) • (↑t : ℂ) ^ a • f t = (↑t : ℂ) ^ (s - 1 + a) • f t
simp_rw₃ : (↑t : ℂ) ^ (s - 1) • (↑t : ℂ) ^ a • f t = ((↑t : ℂ) ^ (s - 1) * (↑t : ℂ) ^ a) • f t
⊢ HSMul.hSMul (β := E) ((↑t : ℂ) ^ (s - 1)) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) t) = (↑t : ℂ) ^ (s + a - 1) • f t

Tactic:
simp_rw [← sub_add_eq_add_sub, cpow_add _ _ (ofReal_ne_zero.2 <| ne_of_gt ht), mul_smul]

Premises used: Iff.mpr, Complex.ofReal_ne_zero, ne_of_gt, Complex.cpow_add, sub_add_eq_add_sub, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
f : ℝ → ℂ
s : ℂ
hf : MellinConvergent f s
a : ℂ
⊢ MellinConvergent (E := ℂ) (fun (t : ℝ) ↦ f t / a) s

Tactic:
simpa only [MellinConvergent, smul_eq_mul, ← mul_div_assoc] using hf.div_const a

Premises used: mul_div_assoc, MellinConvergent.div_const, MellinConvergent, smul_eq_mul
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi (a * 0)) volume

Tactic:
have := integrableOn_Ioi_comp_mul_left_iff (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) 0 ha
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi (a * 0)) volume
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume

Tactic:
rw [mul_zero] at this

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t)) t =
    HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) t

Tactic:
simp only [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), mul_smul, Pi.smul_apply]

Premises used: le_of_lt, LT.lt.le, Complex.mul_cpow_ofReal_nonneg, SemigroupAction.mul_smul, Complex.ofReal_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
⊢ EqOn (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0)

Tactic:
have h1 : EqOn (fun t : ℝ => (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
      ((a : ℂ) ^ (s - 1) • fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0) := fun t ht ↦ by
    simp only [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), mul_smul, Pi.smul_apply]
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
h1 :
  EqOn (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0)
rw : ¬a = 0 ∨ ¬s - 1 ≠ 0
⊢ (↑a : ℂ) ^ (s - 1) ≠ 0

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

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
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
h1 :
  EqOn (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬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
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
h1 :
  EqOn (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬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
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
h1 :
  EqOn (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ (↑a : ℂ) ^ (s - 1) ≠ 0

Tactic:
have h2 : (a : ℂ) ^ (s - 1) ≠ 0 := by
    rw [Ne, cpow_eq_zero_iff, not_and_or, ofReal_eq_zero]
    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
this :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
h1 :
  EqOn (fun (t : ℝ) ↦ (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : (↑a : ℂ) ^ (s - 1) ≠ 0
rw :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Ioi 0) volume ↔
    MellinConvergent f s
rw₁ :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
      (Ioi 0) volume
rw₂ :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Ioi 0) volume ↔
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) (a * x)) (Ioi 0) volume
rw₃ :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Ioi 0) volume ↔
    IntegrableOn (mα := Real.measurableSpace)
      (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0) volume
rw₄ :
  @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Measure.restrict volume (Ioi 0)) ↔
    IntegrableOn (mα := Real.measurableSpace)
      (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0) volume
rw₅ :
  @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Measure.restrict volume (Ioi 0)) ↔
    @Integrable _ _ _ _ Real.measurableSpace
      (HSMul.hSMul (β := (t : ℝ) → E) ((↑a : ℂ) ^ (s - 1)) fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Measure.restrict volume (Ioi 0))
rw₆ rw₇ :
  @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Measure.restrict volume (Ioi 0)) ↔
    @Integrable.{u_1, 0} E _ _ _ Real.measurableSpace (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
      (Measure.restrict volume (Ioi 0))
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s

Tactic:
rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]

Premises used: MeasureTheory.integrableOn_congr_fun, MeasureTheory.IntegrableOn, measurableSet_Ioi, MellinConvergent, MeasureTheory.integrable_smul_iff
-- Module: Mathlib.Analysis.MellinTransform
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 ↔ MellinConvergent f (s / (↑a : ℂ))

Tactic:
Iff.trans ?_ (integrableOn_Ioi_comp_rpow_iff' _ ha)

Premises used: Iff.trans, MeasureTheory.integrableOn_Ioi_comp_rpow_iff'
-- Module: Mathlib.Analysis.MellinTransform
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
refine :
  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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (t ^ a)) s ↔ MellinConvergent f (s / (↑a : ℂ))

Tactic:
refine Iff.trans ?_ (integrableOn_Ioi_comp_rpow_iff' _ ha)

Premises used: Iff.trans, MeasureTheory.integrableOn_Ioi_comp_rpow_iff'