CH2.Phi_diff_bounded_near_pole

lemma Phi_diff_bounded_near_pole (ν ε : ℝ) (hν : ν > 0) :    ∃ U ∈ nhds (z₀_pole ν), BddAbove (norm ∘ (fun z ↦ Phi_circ ν ε z - Phi_star ν ε z) '' (U \ {z₀_pole ν})) := by  let z₀ := z₀_pole ν  let f := fun z ↦ Phi_circ ν ε z - Phi_star ν ε z  have h_mero : MeromorphicAt f z₀ := (Phi_circ.meromorphic ν ε z₀).sub (Phi_star.meromorphic ν ε z₀)  have h_order : meromorphicOrderAt f z₀ ≥ 0 := meromorphicOrderAt_phi_diff_nonneg ν ε hν  obtain ⟨c, h_tendsto⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg h_mero h_order  exact IsBigO_to_BddAbove (h_tendsto.isBigO_one (F := ℂ))