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
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have conv : cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u)) =
  cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: conv => lhs; rw [← re_add_im s]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u)) =
    cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have rw : cexp (-((↑s.im : ℂ) * I) * (↑u : ℂ)) • cexp (-(↑s.re : ℂ) * (↑u : ℂ)) • f (rexp (-u)) =
  cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-((↑s.im : ℂ) * I) * (↑u : ℂ)) • cexp (-(↑s.re : ℂ) * (↑u : ℂ)) • f (rexp (-u)) =
    cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have norm_cast : cexp (-((↑s.im : ℂ) * I) * (↑u : ℂ)) • rexp (-s.re * u) • f (rexp (-u)) =
  cexp ((↑(-s.im * u) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-((↑s.im : ℂ) * I) * (↑u : ℂ)) • rexp (-s.re * u) • f (rexp (-u)) =
    cexp ((↑(-s.im * u) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have push_cast : cexp (-((↑s.im : ℂ) * I) * (↑u : ℂ)) • rexp (-s.re * u) • f (rexp (-u)) =
  cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u)) =
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have e_a : -(↑s.im : ℂ) * (↑u : ℂ) = (↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ mellinInv σ f x =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
have rw : HSMul.hSMul (β := E) |(2 * π)⁻¹|
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
      (↑x : ℂ) ^ (-((↑σ : ℂ) + (↑y : ℂ) * I)) • f ((↑σ : ℂ) + (↑y : ℂ) * I)) =
  HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
      cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
Tactic: rw [mellinInv, one_div, ← abs_of_pos (show 0 < (2 * π)⁻¹ by simp [pi_pos])]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ HSMul.hSMul (β := E) |(2 * π)⁻¹|
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        (↑x : ℂ) ^ (-((↑σ : ℂ) + (↑y : ℂ) * I)) • f ((↑σ : ℂ) + (↑y : ℂ) * I)) =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
have hx0 : (↑x : ℂ) ≠ 0
Tactic: have hx0 : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr (ne_of_gt hx)
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
⊢ HSMul.hSMul (β := E) |(2 * π)⁻¹|
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        (↑x : ℂ) ^ (-((↑σ : ℂ) + (↑y : ℂ) * I)) • f ((↑σ : ℂ) + (↑y : ℂ) * I)) =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
have simp_rw : |(2 * π)⁻¹| •
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
        (↑x : ℂ) ^ (-((↑a : ℂ) * I)) • f ((↑σ : ℂ) + (↑a : ℂ) * I)) =
  HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
      cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
Tactic: simp_rw [neg_add, cpow_add _ _ hx0, mul_smul, integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
⊢ |(2 * π)⁻¹| •
      HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
          (↑x : ℂ) ^ (-((↑a : ℂ) * I)) • f ((↑σ : ℂ) + (↑a : ℂ) * I)) =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
have rw : HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x_1 : ℝ) ↦
      (↑x : ℂ) ^ (-((↑(2 * π * x_1) : ℂ) * I)) • f ((↑σ : ℂ) + (↑(2 * π * x_1) : ℂ) * I)) =
  HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
      cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
Tactic: rw [smul_comm, ← Measure.integral_comp_mul_left]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
⊢ HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x_1 : ℝ) ↦
        (↑x : ℂ) ^ (-((↑(2 * π * x_1) : ℂ) * I)) • f ((↑σ : ℂ) + (↑(2 * π * x_1) : ℂ) * I)) =
    HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I))
have h : ∀ (x_1 : ℝ),
  (↑x : ℂ) ^ (-((↑(2 * π * x_1) : ℂ) * I)) • f ((↑σ : ℂ) + (↑(2 * π * x_1) : ℂ) * I) =
    cexp (2 * (↑π : ℂ) * ((↑x_1 : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑x_1 : ℂ) * I)
Tactic: congr! 3
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
x_1 : ℝ
⊢ (↑x : ℂ) ^ (-((↑(2 * π * x_1) : ℂ) * I)) • f ((↑σ : ℂ) + (↑(2 * π * x_1) : ℂ) * I) =
    cexp (2 * (↑π : ℂ) * ((↑x_1 : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑x_1 : ℂ) * I)
have h : cexp ((↑(Real.log x) : ℂ) * -((↑(2 * π * x_1) : ℂ) * I)) • f ((↑σ : ℂ) + (↑(2 * π * x_1) : ℂ) * I) =
  cexp (2 * (↑π : ℂ) * ((↑x_1 : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑x_1 : ℂ) * I)
Tactic: rw [cpow_def_of_ne_zero hx0, ← Complex.ofReal_log hx.le]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
x_1 : ℝ
⊢ cexp ((↑(Real.log x) : ℂ) * -((↑(2 * π * x_1) : ℂ) * I)) • f ((↑σ : ℂ) + (↑(2 * π * x_1) : ℂ) * I) =
    cexp (2 * (↑π : ℂ) * ((↑x_1 : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑x_1 : ℂ) * I)
have h : cexp ((↑(Real.log x) : ℂ) * -(2 * (↑π : ℂ) * (↑x_1 : ℂ) * I)) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑x_1 : ℂ) * I) =
  cexp (2 * (↑π : ℂ) * ((↑x_1 : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑x_1 : ℂ) * I)
Tactic: push_cast
-- 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
hf : MellinConvergent f (↑σ : ℂ)
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
have rw : ∀
  (hf :
    IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
      (fun (x : ℝ) ↦ |(-rexp (-x))| • (↑((rexp ∘ Neg.neg) x) : ℂ) ^ ((↑σ : ℂ) - 1) • f ((rexp ∘ Neg.neg) x)) univ
      volume)
  (hFf : VerticalIntegrable (mellin f) σ volume) (hfx : ContinuousAt f x),
  let g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u));
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
Tactic: rw [MellinConvergent, ← rexp_neg_image_aux, integrableOn_image_iff_integrableOn_abs_deriv_smul
      MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux] at hf
Cleared hypotheses: hf, hFf, hfx, g
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ |(-rexp (-x))| • (↑((rexp ∘ Neg.neg) x) : ℂ) ^ ((↑σ : ℂ) - 1) • f ((rexp ∘ Neg.neg) x)) univ volume
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
have hf₁ : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ cexp (-(↑σ : ℂ) * (↑x : ℂ)) • f (rexp (-x)))
  volume
Tactic: replace hf : Integrable fun (x : ℝ) ↦ cexp (-↑σ * ↑x) • f (rexp (-x)) := by
      simpa [rexp_cexp_aux] using hf
Cleared hypotheses: hf
-- 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
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
hf :
  @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-(↑σ : ℂ) * (↑x : ℂ)) • f (rexp (-x))) volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
have norm_cast : ∀
  (hf :
    @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-σ * x) • f (rexp (-x))) volume),
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
Tactic: norm_cast at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
inst_2 : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : MellinConvergent f (↑σ : ℂ)
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
⊢ mellinInv σ (mellin f) x = f x
have hf₁ : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
Tactic: replace hf : Integrable g := by
    rw [MellinConvergent, ← rexp_neg_image_aux, integrableOn_image_iff_integrableOn_abs_deriv_smul
      MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux] at hf
    replace hf : Integrable fun (x : ℝ) ↦ cexp (-↑σ * ↑x) • f (rexp (-x)) := by
      simpa [rexp_cexp_aux] using hf
    norm_cast at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
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
have h2π : 2 * π ≠ 0
Tactic: have h2π : 2 * π ≠ 0 := by simp
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
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
h2π : 2 * π ≠ 0
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume
have this : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 (E := (u : ℝ) → E) fun (u : ℝ) ↦ rexp (-(σ * u)) • f (rexp (-u)))
  volume
Tactic: 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π
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
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
⊢ mellinInv σ (mellin f) x = f x
have hFf₁ : @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
Cleared hypotheses: hFf
-- 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
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)
have refine : ContinuousAt f (rexp (- -Real.log x))
Tactic: refine ContinuousAt.smul (by fun_prop) (ContinuousAt.comp ?_ (by fun_prop))
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (hypothesis)
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
⊢ mellinInv σ (mellin f) x = f x
have hfx₁ : 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
Cleared hypotheses: hfx
-- 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 σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) x = (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-Real.log x)
have rw : (↑x : ℂ) ^ (-(↑σ : ℂ)) •
    𝓕⁻ (E := (y : ℝ) → E) (fun (y : ℝ) ↦ 𝓕 g (((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I).im / (2 * π))) (-Real.log x) =
  (↑x : ℂ) ^ (-(↑σ : ℂ)) • 𝓕⁻ (𝓕 g) (-Real.log x)
Tactic: rw [mellinInv_eq_fourierInv _ _ hx, ← hf.fourierInv_fourier_eq hFf hfx]
-- 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)
⊢ (↑x : ℂ) ^ (-(↑σ : ℂ)) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x
have norm_cast : (↑x : ℂ) ^ (↑(-σ) : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x
Tactic: norm_cast
-- 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)
⊢ (↑x : ℂ) ^ (↑(-σ) : ℂ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x
have rw : (↑(x ^ (-σ)) : ℂ) • x ^ σ • f x = f x
Tactic: rw [mul_comm σ, ← rpow_def_of_pos hx, Real.exp_log hx, ← Complex.ofReal_cpow hx.le]
-- 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)
⊢ (↑(x ^ (-σ)) : ℂ) • x ^ σ • f x = f x
have norm_cast : x ^ (-σ) • x ^ σ • f x = f x
Tactic: norm_cast
-- 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)
⊢ x ^ (-σ) • x ^ σ • f x = f x
have rw : (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]
-- 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)
rw : (x ^ (-σ) • x ^ σ) • f x = f x
⊢ x ^ (-σ) • x ^ σ • f x = f x
have rw₁ : (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]
-- 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)
rw : (x ^ (-σ) • x ^ σ) • f x = f x
rw₁ : (x ^ (-σ) * x ^ σ) • f x = f x
⊢ x ^ (-σ) • x ^ σ • f x = f x
have rw₂ : ((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]
-- 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)
rw : (x ^ (-σ) • x ^ σ) • f x = f x
rw₁ : (x ^ (-σ) * x ^ σ) • f x = f x
rw₂ : ((x ^ σ)⁻¹ * x ^ σ) • f x = f x
⊢ x ^ (-σ) • x ^ σ • f x = f x
have rw₃ : HSMul.hSMul (α := ℝ) 1 (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]
-- 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)
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
⊢ x ^ (-σ) • x ^ σ • f x = f x
have rw₄ : 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]
-- 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 σ (mellin f) x = f x
have mellinInv : mellinInv σ (mellin f) x = mellinInv σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) 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
⊢ _root_.mellinInv σ (mellin f) x = f x
have mellinInv₁ : _root_.mellinInv σ (fun (s : ℂ) ↦ 𝓕 g (s.im / (2 * π))) x = (↑x : ℂ) ^ (-(↑σ : ℂ)) • g (-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]