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 : 0 < a
this :
  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)
rw :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * x))) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₁ :
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * a_1)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
⊢ (@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)
have rw₂ : (↑a : ℂ) ^ (1 - s) •
    HSMul.hSMul (β := E) a⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (a * 0))) fun (x : ℝ) ↦
        (↑x : ℂ) ^ (s - 1) • f x) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr 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 :
  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)
rw :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * x))) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₁ :
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * a_1)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₂ :
  (↑a : ℂ) ^ (1 - s) •
      HSMul.hSMul (β := E) a⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (a * 0))) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1) • f x) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
⊢ (@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)
have rw₃ : (↑a : ℂ) ^ (1 - s) •
    HSMul.hSMul (β := E) a⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑x : ℂ) ^ (s - 1) • f x) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr 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 :
  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)
rw :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * x))) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₁ :
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        (fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * a_1)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₂ :
  (↑a : ℂ) ^ (1 - s) •
      HSMul.hSMul (β := E) a⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi (a * 0))) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1) • f x) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
rw₃ :
  (↑a : ℂ) ^ (1 - s) •
      HSMul.hSMul (β := E) a⁻¹
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
          (↑x : ℂ) ^ (s - 1) • f x) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
⊢ (@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)
have rw₄ : (↑a : ℂ) ^ (1 - s) •
    HSMul.hSMul (β := E) (↑a⁻¹ : ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
        (↑x : ℂ) ^ (s - 1) • f x) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr 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 : ℂ
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw : mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t (-1))) 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₁ : HSMul.hSMul (α := ℝ) |(-1)|⁻¹ (mellin f (s / (↑(-1) : ℂ))) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₂ : HSMul.hSMul (α := ℝ) |1|⁻¹ (mellin f (s / (↑(-1) : ℂ))) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₃ : HSMul.hSMul (α := ℝ) 1⁻¹ (mellin f (s / (↑(-1) : ℂ))) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₄ : HSMul.hSMul (α := ℝ) 1 (mellin f (s / (↑(-1) : ℂ))) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₅ : mellin f (s / (↑(-1) : ℂ)) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₆ : mellin f (s / -(↑1 : ℂ)) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₇ : mellin f (s / -1) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
⊢ mellin (fun (t : ℝ) ↦ f t⁻¹) s = mellin f (-s)
have simp_rw₈ : mellin f (-(s / 1)) = 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]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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)
have refine : ∀ x ∈ T, ContinuousAt (Y := ℂ) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1)) x
Tactic: refine ((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul
      (hfc.mono_set hT)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
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 : ℂ
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) T
      volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume
have this : AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
  (Measure.restrict volume T)
Tactic: have : AEStronglyMeasurable (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) (volume.restrict T) := by
    refine ((continuousOn_of_forall_continuousAt ?_).aestronglyMeasurable hT').smul
      (hfc.mono_set hT)
    exact fun t ht => continuousAt_ofReal_cpow_const _ _ (Or.inr <| ne_of_gt (hT ht))
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
⊢ IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t) T
      volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume
have rw : IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ (s - 1) • f a‖) T volume ↔
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume
Tactic: rw [IntegrableOn, ← integrable_norm_iff this, ← IntegrableOn]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
⊢ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (a : ℝ) ↦ ‖(↑a : ℂ) ^ (s - 1) • f a‖) T volume ↔
    IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ t ^ (s.re - 1) * ‖f t‖) T volume
have refine : ∀ (t : ℝ) (ht : t ∈ T), ‖(↑t : ℂ) ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
Tactic: refine integrableOn_congr_fun (fun t ht => ?_) hT'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
t : ℝ
ht : t ∈ T
⊢ ‖(↑t : ℂ) ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
have simp_rw : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
Tactic: simp_rw [norm_smul, norm_cpow_eq_rpow_re_of_pos (hT ht), sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
t : ℝ
ht : t ∈ T
simp_rw : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
⊢ ‖(↑t : ℂ) ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
have simp_rw₁ : t ^ (s - 1).re * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
Tactic: simp_rw [norm_smul, norm_cpow_eq_rpow_re_of_pos (hT ht), sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
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 : ℂ
this :
  AEStronglyMeasurable.{0, u_1} (β := E) (m₀ := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f t)
    (Measure.restrict volume T)
t : ℝ
ht : t ∈ T
simp_rw : ‖(↑t : ℂ) ^ (s - 1)‖ * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
simp_rw₁ : t ^ (s - 1).re * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
⊢ ‖(↑t : ℂ) ^ (s - 1) • f t‖ = t ^ (s.re - 1) * ‖f t‖
have simp_rw₂ : t ^ (s.re - re 1) * ‖f t‖ = t ^ (s.re - 1) * ‖f t‖
Tactic: simp_rw [norm_smul, norm_cpow_eq_rpow_re_of_pos (hT ht), sub_re, one_re]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
have obtain : ∀ (d : ℝ) (hd' : IsBigOWith (F := ℝ) d atTop f fun (x : ℝ) ↦ x ^ (-a)),
  ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
Tactic: obtain ⟨d, hd'⟩ := hf.isBigOWith
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d : ℝ
hd' : IsBigOWith (F := ℝ) d atTop f fun (x : ℝ) ↦ x ^ (-a)
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
have hd'₁ : ∃ (a_1 : ℝ), ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖
Tactic: simp_rw [IsBigOWith, eventually_atTop] at hd'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d : ℝ
hd' : ∃ (a_1 : ℝ), ∀ b ≥ a_1, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
have obtain : ∀ (e : ℝ) (he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖),
  ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
Tactic: obtain ⟨e, he⟩ := hd'
Cleared hypotheses: hd'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
have he' : 0 < max e 1
Tactic: have he' : 0 < max e 1 := zero_lt_one.trans_le (le_max_right _ _)
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
have refine_1 : AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
  (Measure.restrict volume (Ioi (max e 1)))
Tactic: refine ⟨max e 1, he', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
f : ℝ → ℝ
hfc : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) f (Measure.restrict volume (Ioi 0))
a s : ℝ
hf : IsBigO (F := ℝ) atTop f fun (x : ℝ) ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
refine_1 :
  AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
    (Measure.restrict volume (Ioi (max e 1)))
⊢ ∃ (c : ℝ), 0 < c ∧ IntegrableOn (ε := ℝ) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ t ^ (s - 1) * f t) (Ioi c) volume
have refine_2 : @HasFiniteIntegral _ ℝ _ Real.measurableSpace (fun (t : ℝ) ↦ t ^ (s - 1) * f t)
  (Measure.restrict volume (Ioi (max e 1)))
Tactic: refine ⟨max e 1, he', ?_, ?_⟩