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

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

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

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

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

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