-- Mathlib/Analysis/MellinInversion.lean
theorem mellin_eq_fourierIntegral (f : ℝ → E) {s : ℂ} :
    mellin f s = 𝓕 (fun (u : ℝ) ↦ (Real.exp (-s.re * u) • f (Real.exp (-u)))) (s.im / (2 * π)) :=
  calc
    mellin f s
      = ∫ (u : ℝ), Complex.exp (-s * u) • f (Real.exp (-u))

Proof state:
case e_a.e_z.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ ↑u * -↑s.im = ↑(u * (s.im / (2 * π)) * (-2 * π))

Tactic:
have : 2 * (π : ℂ) ≠ 0 := by norm_num; exact pi_ne_zero

Result:
case e_a.e_z.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
this : 2 * ↑π ≠ 0
⊢ ↑u * -↑s.im = ↑(u * (s.im / (2 * π)) * (-2 * π))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Tactic:
congr

Result:
case e_a.e_z.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ -↑s.im * ↑u = ↑(-2 * π * (u * (s.im / (2 * π))))

Proof state:
case e_a.e_z.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ -↑s.im * ↑u = ↑(-2 * π * (u * (s.im / (2 * π))))

Tactic:
rw [mul_comm (-s.im : ℂ) (u : ℂ), mul_comm (-2 * π)]

Result:
case e_a.e_z.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ ↑u * -↑s.im = ↑(u * (s.im / (2 * π)) * (-2 * π))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ ∫ (x : ℝ) in univ, |(-rexp (-x))| • ↑((rexp ∘ Neg.neg) x) ^ (s - 1) • f ((rexp ∘ Neg.neg) x) =
    ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u))

Tactic:
simp [rexp_cexp_aux]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
push_cast

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ ∫ (u : ℝ), cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u)) =
    𝓕 (fun u => rexp (-s.re * u) • f (rexp (-u))) (s.im / (2 * π))

Tactic:
simp [fourierIntegral_eq']

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ 2 * ↑π ≠ 0

Tactic:
norm_num

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ ¬π = 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Tactic:
norm_cast

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ ¬π = 0

Tactic:
exact pi_ne_zero

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
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]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Proof state:
case e_a.e_z.e_a
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
this : 2 * ↑π ≠ 0
⊢ ↑u * -↑s.im = ↑(u * (s.im / (2 * π)) * (-2 * π))

Tactic:
field_simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin f s = ∫ (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]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ ∫ (x : ℝ) in univ, |(-rexp (-x))| • ↑((rexp ∘ Neg.neg) x) ^ (s - 1) • f ((rexp ∘ Neg.neg) x) =
    ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u))

Proof state:
case e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ (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

Result:
case e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-s * ↑u) • f (rexp (-u)) = cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ ∫ (u : ℝ), cexp (-s * ↑u) • f (rexp (-u)) =
    ∫ (u : ℝ), cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u))

Tactic:
congr

Result:
case e_f
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ (fun u => cexp (-s * ↑u) • f (rexp (-u))) = fun u =>
    cexp (↑(-2 * π * (u * (s.im / (2 * π)))) * I) • rexp (-s.re * u) • f (rexp (-u))

Proof state:
case e_f.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
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)))

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-s * ↑u) • f (rexp (-u)) = cexp (-↑s.im * ↑u * I) • rexp (-s.re * u) • f (rexp (-u))

E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))

Tactic:
rw [neg_add, add_mul, Complex.exp_add, mul_comm, ← smul_eq_mul, smul_assoc]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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))