Theorem: Perron.tendsto_zero_Upper (PrimeNumberTheoremAnd/PerronFormula.lean)

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)
Tactic:
have hcast : (fun (y : ℝ) ↦ 1 / y ^ 2) =ᶠ[atTop] fun y ↦ y ^ (-2 : ℝ) := by
  filter_upwards [Ici_mem_atTop 0] with y hy using by rw [rpow_neg hy, inv_eq_one_div, rpow_two]
State after:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ Tendsto (fun t => ∫ (σ : ℝ) in σ'..σ'', f x (↑σ + ↑t * I)) atTop (𝓝 0)
Tactic:
refine isBigO_sup.mp (horizontal_integral_isBigO xpos σ' σ'' volume)
  |>.2.trans_eventuallyEq hcast |>.trans_tendsto <| tendsto_rpow_neg_atTop (by norm_num)
State after:
no goals

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
⊢ (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
Tactic:
filter_upwards [Ici_mem_atTop 0] with y hy using by rw [rpow_neg hy, inv_eq_one_div, rpow_two]
State after:
no goals

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' y : ℝ
hy : y ∈ Ici 0
⊢ 1 / y ^ 2 = y ^ (-2)
Tactic:
rw [rpow_neg hy, inv_eq_one_div, rpow_two]
State after:
no goals

State before:
x σ σ'✝ σ''✝ T : ℝ
xpos : 0 < x
σ' σ'' : ℝ
hcast : (fun y => 1 / y ^ 2) =ᶠ[atTop] fun y => y ^ (-2)
⊢ 0 < 2
Tactic:
norm_num
State after:
no goals