Theorem: ZetaNear1BndFilter (PrimeNumberTheoremAnd/ZetaBounds.lean)

State before:
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
have := Tendsto_nhdsWithin_punctured_add (a := -1) (x := 1)
State after:
this : Tendsto (fun y => y + -1) (𝓝[>] 1) (𝓝[>] (1 + -1))
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)

State before:
this : Tendsto (fun y => y + -1) (𝓝[>] 1) (𝓝[>] (1 + -1))
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
simp only [add_right_neg, ← sub_eq_add_neg] at this
State after:
this : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)

State before:
this : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
have := riemannZeta_isBigO_near_one_horizontal.comp_tendsto this
State after:
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)

State before:
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => ζ ↑σ) =O[𝓝[>] 1] fun σ => 1 / (↑σ - 1)
Tactic:
convert this using 1 <;> {ext; simp}
State after:
no goals

State before:
case h.e'_8
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
⊢ (fun σ => 1 / (↑σ - 1)) = (fun x => 1 / ↑x) ∘ fun y => y - 1
Tactic:
ext
State after:
case h.e'_8.h
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
x✝ : ℝ
⊢ 1 / (↑x✝ - 1) = ((fun x => 1 / ↑x) ∘ fun y => y - 1) x✝

State before:
case h.e'_8.h
this✝ : Tendsto (fun y => y - 1) (𝓝[>] 1) (𝓝[>] 0)
this : ((fun x => ζ (1 + ↑x)) ∘ fun y => y - 1) =O[𝓝[>] 1] ((fun x => 1 / ↑x) ∘ fun y => y - 1)
x✝ : ℝ
⊢ 1 / (↑x✝ - 1) = ((fun x => 1 / ↑x) ∘ fun y => y - 1) x✝
Tactic:
simp
State after:
no goals