CH2.Phi_add_bounded_near_pole

lemma Phi_add_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₁).add (Phi_star.meromorphic ν ε z₁)  have h_order : meromorphicOrderAt f z₁ ≥ 0 := meromorphicOrderAt_phi_add_nonneg ν ε hν  obtain ⟨_, h_tendsto⟩ := tendsto_nhds_of_meromorphicOrderAt_nonneg h_mero h_order  exact IsBigO_to_BddAbove (h_tendsto.isBigO_one (F := ℂ))