ResidueOfTendsTo

@[blueprint  (title := "ResidueOfTendsTo")  (statement := /--  If a function $f$ is holomorphic in a neighborhood of $p$ and  $\lim_{s\to p} (s-p)f(s) = A$, then  $f(s) = \frac{A}{s-p} + O(1)$ near $p$.  -/)  (proof := /--  The function $(s - p)\cdot f(s)$ bounded, so by Theorem  \ref{existsDifferentiableOn_of_bddAbove}, there is a holomorphic function, $g$, say, so that  $(s-p)f(s) = g(s)$ in a neighborhood of $s=p$, and $g(p)=A$. Now because $g$ is holomorphic,  near $s=p$, we have $g(s)=A+O(s-p)$. Then when you divide by $(s-p)$, you get  $f(s) = A/(s-p) + O(1)$.  -/)]theorem ResidueOfTendsTo {f : ℂ → ℂ} {p : ℂ} {U : Set ℂ}    (hU : U ∈ 𝓝 p)    (hf : HolomorphicOn f (U \ {p}))    {A : ℂ}    (h_limit : Tendsto (fun s ↦ (s - p) * f s) (𝓝[≠] p) (𝓝 A)) :    ∃ V ∈ 𝓝 p,    BddAbove (norm ∘ (f - fun s ↦ A * (s - p)⁻¹) '' (V \ {p})) := by  -- Step 1.  `(s-p) f s` is bounded on some punctured nbhd `V`.  have h_event : ∀ᶠ s in 𝓝[≠] p, ‖(s - p) * f s - A‖ < 1 := by    simp_rw [← dist_eq_norm_sub]    exact h_limit.eventually (Metric.ball_mem_nhds _ (by norm_num))  have h_event_nhds :      ∀ᶠ s in 𝓝 p, s ≠ p → ‖(s - p) * f s - A‖ < 1 := by    exact (eventually_nhdsWithin_iff).1 h_event  rcases (eventually_nhds_iff.1 h_event_nhds) with ⟨V₀, hV₀_mem, hV₀_prop⟩  have h_bound :      ∀ s, s ∈ V₀ \ {p} → ‖(s - p) * f s‖ ≤ ‖A‖ + 1 := by    intro s hs    rcases hs with ⟨hV₀, hsne⟩    calc ‖(s - p) * f s‖ = ‖((s - p) * f s - A) + A‖ := by          ring_nf        _ ≤ ‖(s - p) * f s - A‖ + ‖A‖ := norm_add_le ((s - p) * f s - A) A        _ ≤ 1 + ‖A‖ := add_le_add_left (le_of_lt (hV₀_mem s hV₀ hsne)) ‖A‖        _ = ‖A‖ + 1 := add_comm 1 ‖A‖  have h_bdd :      BddAbove (norm ∘ (fun s ↦ (s - p) * f s) '' (V₀ \ {p})) := by    refine ⟨‖A‖ + 1, ?_⟩    rintro _ ⟨s, hs, rfl⟩    exact h_bound s hs  -- From now on work inside `W = V₀ ∩ U`,   still a nbhd of `p`.  set W : Set ℂ := V₀ ∩ U with hW_def  have hW_mem : (W : Set ℂ) ∈ 𝓝 p := inter_mem (IsOpen.mem_nhds hV₀_prop.1 hV₀_prop.2) hU  have h_subset_V₀ : (W \ {p}) ⊆ (V₀ \ {p}) := by    intro z hz; exact ⟨hz.1.1, hz.2⟩  have h_prod_holo : HolomorphicOn (fun z ↦ (z - p) * f z) (W \ {p}) := by    have h_id : HolomorphicOn (fun z : ℂ ↦ z - p) (W \ {p}) :=      Differentiable.differentiableOn (Differentiable.sub_const differentiable_fun_id p)    have hfW : HolomorphicOn f (W \ {p}) := by      apply hf.mono      exact Set.sdiff_subset_sdiff_left inter_subset_right    simpa using! h_id.mul hfW  have h_bdd_W : BddAbove (norm ∘ (fun s ↦ (s - p) * f s) '' (W \ {p})) :=    h_bdd.mono (image_mono h_subset_V₀)  -- Step 2.  Extend the product across `p`; obtain holomorphic `g`.  obtain ⟨g, hg_holo, hg_eq⟩ :=    existsDifferentiableOn_of_bddAbove hW_mem h_prod_holo h_bdd_W  have h_event_eq :      (fun z ↦ g z) =ᶠ[𝓝[≠] p] fun z ↦ (z - p) * f z := by    have hW_diff_mem : (W \ {p} : Set ℂ) ∈ 𝓝[≠] p :=      sdiff_mem_nhdsWithin_compl hW_mem {p}    exact (hg_eq.eventuallyEq_of_mem hW_diff_mem).symm  have h_tendsto_gA : Tendsto g (𝓝[≠] p) (𝓝 A) :=      h_limit.congr' (id (EventuallyEq.symm h_event_eq))  have hpW : p ∈ W := by    exact mem_of_mem_nhds hW_mem  have h_cont_g : ContinuousAt g p := by    apply (hg_holo.continuousOn.continuousWithinAt hpW).continuousAt hW_mem  have h_tendsto_gp : Tendsto g (𝓝[≠] p) (𝓝 (g p)) :=    h_cont_g.tendsto.mono_left inf_le_left  have g_p_eq : g p = A :=    tendsto_nhds_unique' (NormedField.nhdsNE_neBot p) h_tendsto_gp h_tendsto_gA  let q : ℂ → ℂ := fun z ↦ (g z - A) / (z - p)  have h_deriv : HasDerivAt g (deriv g p) p := by    exact DifferentiableOn.hasDerivAt hg_holo hW_mem  have h_q_limit : Tendsto q (𝓝[≠] p) (𝓝 (deriv g p)) := by    rw [hasDerivAt_iff_tendsto_slope] at h_deriv    unfold slope at h_deriv    simp only [vsub_eq_sub, smul_eq_mul, inv_mul_eq_div, g_p_eq] at h_deriv    exact h_deriv  have h_event_q : ∀ᶠ z in 𝓝[≠] p, ‖q z - deriv g p‖ < 1 := by    simp_rw [← dist_eq_norm_sub]    exact h_q_limit.eventually (Metric.ball_mem_nhds _ (by norm_num))  have h_event_q_nhds : ∀ᶠ z in 𝓝 p, z ≠ p → ‖q z - deriv g p‖ < 1 := by    simpa using (eventually_nhdsWithin_iff).1 h_event_q  rcases (eventually_nhds_iff.1 h_event_q_nhds) with    ⟨V₁, hV₁_mem, hV₁_prop⟩  have h_q_bound :      ∀ z, z ∈ V₁ \ {p} → ‖q z‖ ≤ ‖deriv g p‖ + 1 := by    intro z hz    rcases hz with ⟨hV₁, hz_ne⟩    calc ‖q z‖ = ‖(q z - deriv g p) + (deriv g p)‖ := by          ring_nf        _ ≤ ‖q z - deriv g p‖ + ‖deriv g p‖ := norm_add_le (q z - deriv g p) (deriv g p)        _ ≤ 1 + ‖deriv g p‖  := add_le_add_left (le_of_lt (hV₁_mem z hV₁ hz_ne)) ‖deriv g p‖        _ = ‖deriv g p‖ + 1 := add_comm 1 ‖deriv g p‖  -- Step 4.  Relate `f` to `q` and pass the bound.  have h_eq_diff :      EqOn (fun z ↦ f z - A * (z - p)⁻¹) q (W \ {p}) := by    intro z hz    simp only    have hz_ne : (z - p) ≠ 0 := sub_ne_zero.mpr hz.2    have hgz : g z = (z - p) * f z := by      exact id (EqOn.symm hg_eq) hz    simp only [hgz, q]    field_simp  apply IsBigO_to_BddAbove  rw [isBigO_iff]  use ‖deriv g p‖ + 1  apply eventually_nhdsWithin_iff.mpr  filter_upwards [IsOpen.mem_nhds hV₁_prop.1 hV₁_prop.2, hW_mem] with z hV₁ hW z_ne_p  specialize h_eq_diff ⟨ hW, z_ne_p⟩  simp only [Pi.sub_apply, Pi.one_apply, one_mem, CStarRing.norm_of_mem_unitary,    mul_one] at h_eq_diff ⊢  rw [h_eq_diff]  exact h_q_bound _ ⟨hV₁, z_ne_p⟩