Theorem: PerronInverseMellin_gt (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ MellinInverseTransform (Perron.f t) σ x = 1 - ↑x / ↑t
Tactic:
dsimp [MellinInverseTransform]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
have tpos : 0 < t := by linarith
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
have txinv_gtOne : 1 < t / x := (one_lt_div xpos).mpr x_lt_t
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
rw [← smul_eq_mul]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (1 / (2 * ↑π * I)) • VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 1 - ↑x / ↑t
Tactic:
convert Perron.formulaGtOne txinv_gtOne σpos using 2
State after:
case h.e'_2.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = VerticalIntegral (fun s => ↑(t / x) ^ s / (s * (s + 1))) σ

case h.e'_3.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ ↑x / ↑t = 1 / ↑(t / x)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
⊢ 0 < t
Tactic:
linarith
State after:
no goals

State before:
case h.e'_2.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = VerticalIntegral (fun s => ↑(t / x) ^ s / (s * (s + 1))) σ
Tactic:
congr
State after:
case h.e'_2.h.e'_6.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = fun s => ↑(t / x) ^ s / (s * (s + 1))

State before:
case h.e'_2.h.e'_6.e_f
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = fun s => ↑(t / x) ^ s / (s * (s + 1))
Tactic:
ext1 s
State after:
case h.e'_2.h.e'_6.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = ↑(t / x) ^ s / (s * (s + 1))

State before:
case h.e'_2.h.e'_6.e_f.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = ↑(t / x) ^ s / (s * (s + 1))
Tactic:
convert Perron.f_mul_eq_f tpos xpos s using 1
State after:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)

State before:
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)
Tactic:
ring
State after:
no goals

State before:
case h.e'_3.h.e'_6
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
xpos : 0 < x
x_lt_t : x < t
σ : ℝ
σpos : 0 < σ
tpos : 0 < t
txinv_gtOne : 1 < t / x
⊢ ↑x / ↑t = 1 / ↑(t / x)
Tactic:
field_simp
State after:
no goals