Theorem: PerronInverseMellin_lt (PrimeNumberTheoremAnd/MellinCalculus.lean)

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

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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ 1 / (2 * ↑π * I) * VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Tactic:
simp only [one_div, mul_inv_rev, inv_I, neg_mul, neg_eq_zero, mul_eq_zero, I_ne_zero,
  inv_eq_zero, ofReal_eq_zero, pi_ne_zero, OfNat.ofNat_ne_zero, or_self, false_or]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ VerticalIntegral (fun s => ↑x ^ (-s) * Perron.f t s) σ = 0
Tactic:
convert Perron.formulaLtOne (div_pos tpos xpos) ((div_lt_one xpos).mpr t_lt_x) σpos using 2
State after:
case h.e'_2.h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
⊢ (fun s => ↑x ^ (-s) * Perron.f t s) = Perron.f (t / x)

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

State before:
case h.e'_2.h.e'_4.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
t x : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f (t / x) s
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 : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < 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 : ℝ
tpos : 0 < t
t_lt_x : t < x
σ : ℝ
σpos : 0 < σ
xpos : 0 < x
s : ℂ
⊢ ↑x ^ (-s) * Perron.f t s = Perron.f t s * ↑x ^ (-s)
Tactic:
ring
State after:
no goals