awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
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)
⊢ _root_.mellinInv σ (mellin f) x = f x
have mellinInv₂ : (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-Real.log x) = (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
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))
⊢ _root_.mellinInv σ (mellin f) x = f x
have mellinInv₃ : (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log 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]
-- 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 : ℂ
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) s ↔ MellinConvergent 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 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 : ℂ
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
⊢ HSMul.hSMul (β := E) ((↑t : ℂ) ^ (s - 1)) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) t) = (↑t : ℂ) ^ (s + a - 1) • f t
have simp_rw₂ : (↑t : ℂ) ^ (s - 1) • (↑t : ℂ) ^ a • f t = (↑t : ℂ) ^ (s - 1 + a) • f t
Tactic: simp_rw [← sub_add_eq_add_sub, cpow_add _ _ (ofReal_ne_zero.2 <| ne_of_gt ht), mul_smul]
-- 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 : ℂ
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
⊢ HSMul.hSMul (β := E) ((↑t : ℂ) ^ (s - 1)) ((fun (t : ℝ) ↦ (↑t : ℂ) ^ a • f t) t) = (↑t : ℂ) ^ (s + a - 1) • f t
have simp_rw₃ : (↑t : ℂ) ^ (s - 1) • (↑t : ℂ) ^ a • f t = ((↑t : ℂ) ^ (s - 1) * (↑t : ℂ) ^ a) • f t
Tactic: simp_rw [← sub_add_eq_add_sub, cpow_add _ _ (ofReal_ne_zero.2 <| ne_of_gt ht), mul_smul]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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
Tactic: have := integrableOn_Ioi_comp_mul_left_iff (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) 0 ha
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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
Tactic: rw [mul_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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)
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]
-- 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 : 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
have rw : ¬a = 0 ∨ ¬s - 1 ≠ 0
Tactic: rw [Ne, cpow_eq_zero_iff, not_and_or, ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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)
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have h2 : (↑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'
-- 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 : 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have rw : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
    (Ioi 0) volume ↔
  MellinConvergent f s
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 : 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 : 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 : 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 : 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 : 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
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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))
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 : 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))
⊢ MellinConvergent.{u_1} (E := E) (fun (t : ℝ) ↦ f (a * t)) s ↔ MellinConvergent f s
have 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))
Tactic: rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
    IntegrableOn, IntegrableOn, integrable_smul_iff h2]
-- 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 ↔ MellinConvergent f (s / (↑a : ℂ))
have 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
Tactic: refine Iff.trans ?_ (integrableOn_Ioi_comp_rpow_iff' _ ha)