-- 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
⊢ Integrable (𝓕 g) volume

Tactic:
have h2π : 2 * π ≠ 0 := by norm_num; exact pi_ne_zero

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
⊢ Integrable (𝓕 g) volume

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
this : Integrable (𝓕 fun u => rexp (-σ * u) • f (rexp (-u))) volume
⊢ Integrable (𝓕 g) volume

Tactic:
exact this

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)
⊢ ↑x ^ (-↑σ) • rexp (σ * Real.log x) • f (rexp (Real.log x)) = f x

Tactic:
norm_cast

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 ^ ↑(-σ) • rexp (σ * Real.log x) • f (rexp (Real.log 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
⊢ 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
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
⊢ ¬π = 0

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

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : IntegrableOn (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 : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
⊢ Integrable g volume

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 (fun u => rexp (-u)) (-Real.log x)

Tactic:
fun_prop

Result:
no goals

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

Tactic:
replace hf : Integrable fun (x : ℝ) ↦ cexp (-↑σ * ↑x) • f (rexp (-x)) := by
  simpa [rexp_cexp_aux] using hf

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 (fun x => cexp (-↑σ * ↑x) • f (rexp (-x))) 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:
norm_cast

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 ^ (-σ) • x ^ σ • 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
⊢ mellinInv σ (mellin f) x = f x

Tactic:
replace hFf : Integrable (𝓕 g) := by
  have h2π : 2 * π ≠ 0 := by norm_num; exact pi_ne_zero
  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π
  simp_rw [neg_mul_eq_neg_mul] at this
  exact this

Result:
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
⊢ 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
hfx : ContinuousAt f x
g : ℝ → E := fun u => rexp (-σ * u) • f (rexp (-u))
hf : Integrable g volume
hFf : Integrable (𝓕 g) volume
⊢ ContinuousAt (fun u => rexp (-σ * u)) (-Real.log x)

Tactic:
fun_prop

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
σ : ℝ
f : ℝ → E
x : ℝ
hx : 0 < x
hf : MellinConvergent f ↑σ
hFf : VerticalIntegrable (mellin f) σ volume
hfx : ContinuousAt f x
⊢ mellinInv σ (mellin f) x = f x

Tactic:
let g := fun (u : ℝ) => Real.exp (-σ * u) • f (Real.exp (-u))

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