ResidueMult

@[blueprint  (title := "ResidueMult")  (statement := /--  If $f$ has a simple pole at $p$ with residue $A$, and $g$ is holomorphic near $p$, then the  residue of $f \cdot g$ at $p$ is $A \cdot g(p)$. That is, we assume that  $$  f(s) = \frac{A}{s - p} + O(1)$$  near $p$, and that $g$ is holomorphic near $p$. Then  $$  f(s) \cdot g(s) = \frac{A \cdot g(p)}{s - p} + O(1).$$  -/)  (proof := /--  Elementary calculation.  $$  f(s) * g(s) - \frac{A * g(p)}{s - p} =  \left(f(s) * g(s) - \frac{A * g(s)}{s - p}\right)  + \left(\frac{A * g(s) - A * g(p)}{s - p}\right).  $$  The first term is $g(s)(f(s) - \frac{A}{s - p})$, which is bounded near $p$ by the assumption  on $f$   and the fact that $g$ is holomorphic near $p$.  The second term is $A$ times the log derivative of $g$ at $p$, which is bounded by the assumption  that  $g$ is holomorphic.  -/)]theorem ResidueMult {f g : ℂ → ℂ} {p : ℂ} {U : Set ℂ}    (g_holc : HolomorphicOn g U) (U_in_nhds : U ∈ 𝓝 p) {A : ℂ}    (f_near_p : (f - (fun s ↦ A * (s - p)⁻¹)) =O[𝓝[≠] p] (1 : ℂ → ℂ)) :    (f * g - (fun s ↦ A * g p * (s - p)⁻¹)) =O[𝓝[≠] p] (1 : ℂ → ℂ) := by  -- Add and subtract a term  have : (f * g - fun s ↦ A * g p * (s - p)⁻¹)      = (f - A • fun s ↦ (s - p)⁻¹) * g + fun s ↦ (A * (g s - g p) / (s - p)) := by    ext; simp; ring  -- Apply to goal  rw[this]  have p_in_U : p ∈ U := mem_of_mem_nhds U_in_nhds  refine Asymptotics.IsBigO.add ?_ ?_  · rw[← mul_one (1 : ℂ → ℂ)]    refine Asymptotics.IsBigO.mul f_near_p ?_    -- Show g is bounded near p    have g_cont : ContinuousAt g p := by      -- g is holomorphic on U, p ∈ U, so g is continuous at p      exact (g_holc.continuousOn.continuousWithinAt p_in_U).continuousAt U_in_nhds    -- Use continuity to get boundedness    have := g_cont.norm.isBoundedUnder_le.isBigO_one ℂ    exact IsBigO.mono this inf_le_left  · -- Show that (fun s ↦ A * (g s - g p) / (s - p)) =O[𝓝[≠] p] 1     suffices (fun s ↦ A * ((s - p)⁻¹ * (g s - g p))) =O[𝓝[≠] p] 1 by      convert! this using 2      rw[div_eq_mul_inv]      ring    apply Asymptotics.IsBigO.const_mul_left     -- g is differentiable at p since it's holomorphic on U    have g_diff : HasDerivAt g (deriv g p) p :=        (DifferentiableOn.differentiableAt g_holc U_in_nhds).hasDerivAt     rw [hasDerivAt_iff_isLittleO] at g_diff    apply Asymptotics.IsLittleO.isBigO at g_diff    have : (fun x' ↦ deriv g p * (x' - p)) =O[𝓝 p] fun x' ↦ x' - p := by      apply Asymptotics.IsBigO.const_mul_left      exact Asymptotics.isBigO_refl (fun x ↦ x - p) (𝓝 p)    have h1 := g_diff.add this    have h2 : (fun x ↦ g x - g p) =O[𝓝 p] fun x' ↦ x' - p := by      convert! h1 using 2      simp      ring    refine (Asymptotics.isBigO_mul_iff_isBigO_div ?_).mpr ?_    · filter_upwards [self_mem_nhdsWithin] with x hx      simp only [mem_compl_iff, mem_singleton_iff] at hx      exact inv_ne_zero (sub_ne_zero.mpr hx)    · simp only [div_inv_eq_mul]      refine Asymptotics.IsBigO.mono ?_ inf_le_left      simpa