Theorem: MellinInverseTransform_eq (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ MellinInverseTransform f σ = mellinInv σ f
Tactic:
unfold mellinInv MellinInverseTransform VerticalIntegral' VerticalIntegral
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), (fun s => ↑x ^ (-s) * f s) (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), (fun s => ↑x ^ (-s) * f s) (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
beta_reduce
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
⊢ (fun x => (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I)) = fun x =>
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
ext x
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I)) • I • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
rw [← smul_assoc, smul_eq_mul (a' := I), div_mul]
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I / I)) • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
σ : ℝ
f : ℂ → ℂ
x : ℝ
⊢ (1 / (2 * ↑π * I / I)) • ∫ (t : ℝ), ↑x ^ (-(↑σ + ↑t * I)) * f (↑σ + ↑t * I) =
    (1 / (2 * π)) • ∫ (y : ℝ), ↑x ^ (-(↑σ + ↑y * I)) • f (↑σ + ↑y * I)
Tactic:
simp
State after:
no goals