Theorem: riemannZeta_isBigO_near_root_horizontal (EulerProducts/PNT.lean)

State before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x
Tactic:
have hy' : 1 + I * y ≠ 1 := by simp [hy]
State after:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x

State before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (1 + ↑x + I * ↑y)) =O[𝓝[>] 0] fun x => ↑x
Tactic:
conv => enter [2, x]; rw [add_comm 1, add_assoc]
State after:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x

State before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
hy' : 1 + I * ↑y ≠ 1
⊢ (fun x => ζ (↑x + (1 + I * ↑y))) =O[𝓝[>] 0] fun x => ↑x
Tactic:
exact (isBigO_comp_ofReal <| (differentiableAt_riemannZeta hy').isBigO_of_eq_zero h).mono
  nhdsWithin_le_nhds
State after:
no goals

State before:
y : ℝ
hy : y ≠ 0
h : ζ (1 + I * ↑y) = 0
⊢ 1 + I * ↑y ≠ 1
Tactic:
simp [hy]
State after:
no goals