awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
rw : cexp (-(↑x : ℂ) * (1 + (s - 1))) • f = cexp (-s * (↑x : ℂ)) • f
⊢ (HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1 * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f

Tactic:
rw [← cpow_add _ _ (Complex.exp_ne_zero _), cpow_def_of_ne_zero (Complex.exp_ne_zero _),
    Complex.log_exp (by simp [pi_pos]) (by simpa using pi_nonneg)]

Premises used: Complex.exp_ne_zero, Complex.log_exp, Complex.cpow_add, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ cexp (-(↑x : ℂ) * (1 + (s - 1))) • f = cexp (-s * (↑x : ℂ)) • f

Tactic:
ring_nf
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
rw :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ) ↦
      |(-rexp (-x))| • (↑((rexp ∘ Neg.neg) x) : ℂ) ^ (s - 1) • f ((rexp ∘ Neg.neg) x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u)))
⊢ mellin f s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u))

Tactic:
rw [mellin, ← rexp_neg_image_aux, integral_image_eq_integral_abs_deriv_smul
        MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux]

Premises used: MeasureTheory.integral_image_eq_integral_abs_deriv_smul, _private.0.rexp_neg_image_aux, _private.0.rexp_neg_injOn_aux, mellin, _private.0.rexp_neg_deriv_aux, MeasurableSet.univ
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ) ↦
      |(-rexp (-x))| • (↑((rexp ∘ Neg.neg) x) : ℂ) ^ (s - 1) • f ((rexp ∘ Neg.neg) x))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u)))

Tactic:
simp [rexp_cexp_aux]

Premises used: _private.0.rexp_cexp_aux
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
e_f :
  Eq.{u_1 + 1} (α := ℝ → E) (fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u))) fun (u : ℝ) ↦
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦
      cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u)))

Tactic:
congr
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
e_f :
  ∀ (u : ℝ),
    cexp (-s * (↑u : ℂ)) • f (rexp (-u)) =
      cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
⊢ Eq.{u_1 + 1} (α := ℝ → E) (fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u))) fun (u : ℝ) ↦
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
ext u
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
trans : cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
trans₁ :
  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))
⊢ cexp (-s * (↑u : ℂ)) • f (rexp (-u)) =
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
trans Complex.exp (-s.im * u * I) • (Real.exp (-s.re * u) • f (Real.exp (-u)))

Premises used: HMul.hMul, Complex.im, Real.exp, Complex.ofReal, Complex.re, Complex.exp, HSMul.hSMul, Neg.neg, Complex.I
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
lhs : cexp (-s * (↑u : ℂ)) • f (rexp (-u))
| cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
lhs
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
rw : cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u))
| cexp (-s * (↑u : ℂ)) • f (rexp (-u))

Tactic:
rw [← re_add_im s]

Premises used: Complex.re_add_im
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
rw : cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u))
| cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
lhs; rw [← re_add_im s]

Premises used: Complex.re_add_im
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
conv :
  cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u)) =
    cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
⊢ cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
conv => lhs; rw [← re_add_im s]

Premises used: Complex.re_add_im
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
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))
⊢ cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑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]

Premises used: add_mul, smul_assoc, Complex.exp_add, neg_add, mul_comm, smul_eq_mul
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
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))
⊢ 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:
norm_cast
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
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))
⊢ 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
-- Module: Mathlib.Analysis.MellinInversion
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))

Tactic:
ring_nf
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
e_a : -(↑s.im : ℂ) * (↑u : ℂ) = (↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ)
⊢ 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))

Tactic:
congr
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ -(↑s.im : ℂ) * (↑u : ℂ) = (↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ)

Tactic:
simp [field]
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦
      cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))) =
    𝓕 (E := (u : ℝ) → E) (fun (u : ℝ) ↦ rexp (-s.re * u) • f (rexp (-u))) (s.im / (2 * π))

Tactic:
simp [fourier_eq', mul_comm (_ / _)]

Premises used: HDiv.hDiv, mul_comm, Real.fourier_eq'
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ 0 < (2 * π)⁻¹

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
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))
⊢ mellinInv σ f x =
    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])]

Premises used: mellinInv, one_div, abs_of_pos
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ (↑x : ℂ) ≠ 0

Tactic:
have hx0 : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr (ne_of_gt hx)
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
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))
⊢ 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:
simp_rw [neg_add, cpow_add _ _ hx0, mul_smul, integral_smul]

Premises used: MeasureTheory.integral_smul, neg_add, Complex.cpow_add, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
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))
⊢ |(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:
rw [smul_comm, ← Measure.integral_comp_mul_left]

Premises used: MeasureTheory.Measure.integral_comp_mul_left, SMulCommClass.smul_comm
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
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)
⊢ 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:
congr! 3
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
x_1 : ℝ
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)
⊢ (↑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]

Premises used: Complex.ofReal_log, LT.lt.le, Complex.cpow_def_of_ne_zero
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
hx0 : (↑x : ℂ) ≠ 0
x_1 : ℝ
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)
⊢ 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
-- Module: Mathlib.Analysis.MellinInversion
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)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.MellinInversion
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
σ : ℝ
f : ℂ → E
x : ℝ
hx : 0 < x
⊢ HSMul.hSMul (β := E) ((↑x : ℂ) ^ (-(↑σ : ℂ)))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
        cexp (2 * (↑π : ℂ) * ((↑y : ℂ) * -(↑(Real.log x) : ℂ)) * I) • f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I)) =
    (↑x : ℂ) ^ (-(↑σ : ℂ)) •
      𝓕⁻ (E := (y : ℝ) → E) (fun (y : ℝ) ↦ f ((↑σ : ℂ) + 2 * (↑π : ℂ) * (↑y : ℂ) * I)) (-Real.log x)

Tactic:
simp [fourierInv_eq', mul_comm (Real.log _)]

Premises used: Real.log, mul_comm, Real.fourierInv_eq'
-- 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
hf : MellinConvergent f (↑σ : ℂ)
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : (u : ℝ) → E := fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u))
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
⊢ @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

Premises used: _private.0.rexp_neg_image_aux, MeasureTheory.integrableOn_image_iff_integrableOn_abs_deriv_smul, MellinConvergent, _private.0.rexp_neg_injOn_aux, _private.0.rexp_neg_deriv_aux, MeasurableSet.univ
-- 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
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.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-(↑σ : ℂ) * (↑x : ℂ)) • f (rexp (-x))) volume

Tactic:
simpa [rexp_cexp_aux] using hf

Premises used: _private.0.rexp_cexp_aux
-- 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
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.{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
-- 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.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ cexp (-(↑σ : ℂ) * (↑x : ℂ)) • f (rexp (-x))) volume
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  ∀
    (hf :
      @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-σ * x) • f (rexp (-x))) volume),
    @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g volume

Tactic:
norm_cast at hf
-- 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
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

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
-- 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
⊢ 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
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
⊢ 2 * π ≠ 0

Tactic:
have h2π : 2 * π ≠ 0 := by 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
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
    (𝓕 (E := (u : ℝ) → E) fun (u : ℝ) ↦ rexp (-(σ * u)) • f (rexp (-u))) volume

Tactic:
simpa [mellin_eq_fourier, mul_div_cancel_right₀ _ h2π] using hFf.comp_mul_right' h2π

Premises used: mellin_eq_fourier, MeasureTheory.Integrable.comp_mul_right', mul_div_cancel_right₀
-- 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
h2π : 2 * π ≠ 0
⊢ @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π
-- 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
h2π : 2 * π ≠ 0
this :
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace
    (𝓕 (E := (u : ℝ) → E) fun (u : ℝ) ↦ rexp (-(σ * u)) • f (rexp (-u))) volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 (E := (u : ℝ) → E) fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u)))
    volume

Tactic:
simp_rw [neg_mul_eq_neg_mul] at this

Premises used: neg_mul_eq_neg_mul
-- 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
h2π : 2 * π ≠ 0
this :
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 (E := (u : ℝ) → E) fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u)))
    volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume

Tactic:
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
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
this :
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 (E := (u : ℝ) → E) fun (u : ℝ) ↦ rexp (-σ * u) • f (rexp (-u)))
    volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (𝓕 g) volume

Tactic:
exact this