-- Mathlib/Analysis/MellinInversion.lean
theorem mellin_inversion (σ : ℝ) (f : ℝ → E) {x : ℝ} (hx : 0 < x) (hf : MellinConvergent f σ)
    (hFf : VerticalIntegrable (mellin f) σ) (hfx : ContinuousAt f x) :
    mellinInv σ (mellin f) x = f x

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
⊢ Integrable (𝓕 g) volume

Tactic:
have : Integrable (𝓕 (fun u ↦ rexp (-(σ * u)) • f (rexp (-u)))) := by
  simpa [mellin_eq_fourierIntegral, mul_div_cancel_right₀ _ h2π] using hFf.comp_mul_right' h2π

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
h2π : 2 * π ≠ 0
this : Integrable (𝓕 fun u => rexp (-(σ * u)) • f (rexp (-u))) volume
⊢ Integrable (𝓕 g) volume

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ 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]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ mellinInv σ (fun s => 𝓕 g (s.im / (2 * π))) x = ↑x ^ (-↑σ) • g (-Real.log x)

Tactic:
rw [mellinInv_eq_fourierIntegralInv _ _ hx, ← hf.fourier_inversion hFf hfx]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ↑x ^ (-↑σ) • 𝓕⁻ (fun y => 𝓕 g ((↑σ + 2 * ↑π * ↑y * I).im / (2 * π))) (-Real.log x) =
    ↑x ^ (-↑σ) • 𝓕⁻ (𝓕 g) (-Real.log x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hfx : ContinuousAt f x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
⊢ ContinuousAt f (rexp (- -Real.log x))

Tactic:
simpa [Real.exp_log hx] using hfx

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ¬π = 0

Tactic:
exact pi_ne_zero

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ 2 * π ≠ 0

Tactic:
norm_num

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ¬π = 0

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
hfx : ContinuousAt g (-Real.log x)
⊢ ↑x ^ (-↑σ) • 𝓕⁻ (fun y => 𝓕 g ((↑σ + 2 * ↑π * ↑y * I).im / (2 * π))) (-Real.log x) =
    ↑x ^ (-↑σ) • 𝓕⁻ (𝓕 g) (-Real.log x)

Tactic:
simp [mul_div_cancel_left₀ _ (show 2 * π ≠ 0 by norm_num; exact pi_ne_zero)]

Result:
no goals