Mathlib.Analysis.Argument­Principle­Circle

theorem normalizedLogDerivCircleIntegral_centeredMonomial {c a : ℂ} {R : ℝ} {n : ℕ} (hR : 0 < R) (ha : a ∈ ball c R) : normalizedLogDerivCircleIntegral (fun z ↦ (z - a) ^ n) c R = (n : ℂ) := by have hlogDeriv : logDeriv (fun z : ℂ ↦ (z - a) ^ n) = fun z ↦ (n : ℂ) * (z - a)⁻¹ := by funext z rw [logDeriv_fun_pow (by fun_prop)] simp [logDeriv_apply, div_eq_mul_inv] rw [normalizedLogDerivCircleIntegral, hlogDeriv, circleIntegral.integral_const_mul, circleIntegral.integral_sub_inv_of_mem_ball ha] field_simp

theorem argumentPrinciple_circle {f : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hf : AnalyticOnNhd ℂ f (closedBall c R)) (hboundary : ∀ z ∈ sphere c R, f z ≠ 0) : normalizedLogDerivCircleIntegral f c R = (zeroMultiplicityCount f c R : ℂ) := by classical let U := closedBall c R let D := MeromorphicOn.divisor f U let P : ℂ → ℂ := ∏ᶠ u, (· - u) ^ D u let w : ℂ := c + R have hwS : w ∈ sphere c R := by simp [w, abs_of_pos hR] have hwU : w ∈ U := sphere_subset_closedBall hwS have hmw : meromorphicOrderAt f w ≠ ⊤ := by rw [(hf w hwU).meromorphicOrderAt_eq, (hf w hwU).analyticOrderAt_eq_zero.2 (hboundary w hwS)] simp have hfinite : ∀ z ∈ U, meromorphicOrderAt f z ≠ ⊤ := fun z hz ↦ hf.meromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected (convex_closedBall c R).isPreconnected hwU hz hmw have hDfinite : D.support.Finite := (MeromorphicOn.divisor f U).finiteSupport (isCompact_closedBall c R) obtain ⟨g, hg, hgne, hfg⟩ := hf.meromorphicOn.extract_zeros_poles (fun z ↦ hfinite z z.property) hDfinite have hDnonneg : 0 ≤ D := by simpa [D, U] using MeromorphicOn.AnalyticOnNhd.divisor_nonneg hf have hPan : AnalyticOnNhd ℂ P U := by intro z hz exact Function.FactorizedRational.analyticAt (hDnonneg z) have hPgan : AnalyticOnNhd ℂ (fun z ↦ P z * g z) U := hPan.mul hg have hfg' : f =ᶠ[codiscreteWithin U] fun z ↦ P z * g z := by have h0 : f =ᶠ[codiscreteWithin U] P * g := by simpa [P, U, smul_eq_mul] using hfg exact h0 have hcU : c ∈ U := by simp [U, hR.le] have hlocal : f =ᶠ[𝓝[≠] c] fun z ↦ P z * g z := by change {z | f z = P z * g z} ∈ codiscreteWithin U at hfg' rw [mem_codiscreteWithin_iff_forall_mem_nhdsNE] at hfg' filter_upwards [hfg' c hcU, mem_nhdsWithin_of_mem_nhds (closedBall_mem_nhds c hR)] with z hz hzU exact hz.resolve_right (by simpa [U] using hzU) have heq : EqOn f (fun z ↦ P z * g z) U := hf.eqOn_of_preconnected_of_frequently_eq hPgan (convex_closedBall c R).isPreconnected hcU hlocal.frequently have hDz (z : ℂ) (hz : z ∈ sphere c R) : D z = 0 := by have hzU : z ∈ U := sphere_subset_closedBall hz dsimp [D] rw [MeromorphicOn.divisor_apply hf.meromorphicOn hzU, (hf z hzU).meromorphicOrderAt_eq, (hf z hzU).analyticOrderAt_eq_zero.2 (hboundary z hz)] simp have hlogeq : EqOn (logDeriv f) (fun z ↦ (∑ u ∈ hDfinite.toFinset, (D u : ℂ) * (z - u)⁻¹) + logDeriv g z) (sphere c R) := by intro z hz have hzU : z ∈ U := sphere_subset_closedBall hz have hznb : z ∉ ball c R := by rw [mem_ball, mem_sphere] at * exact not_lt_of_ge hz.ge have hzcl : z ∈ closure (ball c R) := by rw [closure_ball c hR.ne'] exact hzU have hfreq : ∃ᶠ y in 𝓝[≠] z, f y = P y * g y := (mem_closure_ne_iff_frequently_within.mp (by rw [diff_singleton_eq_self hznb] exact hzcl)).mono fun y hy ↦ heq (by exact ball_subset_closedBall hy) have hnear : f =ᶠ[𝓝 z] fun y ↦ P y * g y := ((hf z hzU).frequently_eq_iff_eventually_eq (hPgan z hzU)).mp hfreq calc logDeriv f z = logDeriv (fun y ↦ P y * g y) z := by simp only [logDeriv_apply, hnear.eq_of_nhds, hnear.deriv_eq] _ = logDeriv P z + logDeriv g z := logDeriv_mul z (Function.FactorizedRational.ne_zero (hDz z hz)) (hgne ⟨z, hzU⟩) (hPan z hzU).differentiableAt (hg z hzU).differentiableAt _ = _ := by rw [logDeriv_factorizedRational_eq_sum hDfinite (hDz z hz)] have hloggan : AnalyticOnNhd ℂ (logDeriv g) U := by intro z hz exact (hg.deriv z hz).div (hg z hz) (hgne ⟨z, hz⟩) have hloggzero : circleIntegral (logDeriv g) c R = 0 := (hloggan.differentiableOn.diffContOnCl_ball (by simp [U])).circleIntegral_eq_zero hR.le have hterm (u : ℂ) (hu : u ∈ hDfinite.toFinset) : CircleIntegrable (fun z ↦ (D u : ℂ) * (z - u)⁻¹) c R := by have huD : D u ≠ 0 := by simpa using hu have huS : u ∉ sphere c R := by intro hus exact huD (hDz u hus) exact ((circleIntegrable_sub_inv_iff.mpr (.inr (by simpa [abs_of_pos hR] using huS))).const_mul _) have hsumInt : circleIntegral (fun z ↦ ∑ u ∈ hDfinite.toFinset, (D u : ℂ) * (z - u)⁻¹) c R = ∑ u ∈ hDfinite.toFinset, (D u : ℂ) * (2 * (Real.pi : ℂ) * I) := by rw [circleIntegral.integral_fun_sum hterm] apply Finset.sum_congr rfl intro u hu rw [circleIntegral.integral_const_mul, circleIntegral.integral_sub_inv_of_mem_ball] have huSupp : u ∈ D.support := by simpa using hu have huU : u ∈ U := (MeromorphicOn.divisor f U).supportWithinDomain huSupp have huNS : u ∉ sphere c R := by intro hus exact (show D u ≠ 0 by simpa using hu) (hDz u hus) have huUdist : dist u c ≤ R := by simpa [U, mem_closedBall] using huU have hdistne : dist u c ≠ R := by intro h apply huNS exact h rw [mem_ball] exact lt_of_le_of_ne huUdist hdistne have hloggCI : CircleIntegrable (logDeriv g) c R := hloggan.continuousOn.mono (sphere_subset_closedBall : sphere c R ⊆ U) |>.circleIntegrable hR.le have hcircle : circleIntegral (logDeriv f) c R = ∑ u ∈ hDfinite.toFinset, (D u : ℂ) * (2 * (Real.pi : ℂ) * I) := by rw [circleIntegral.integral_congr hR.le hlogeq, circleIntegral.integral_add (CircleIntegrable.fun_sum _ hterm) hloggCI, hsumInt, hloggzero, add_zero] have hsum : (∑ u ∈ hDfinite.toFinset, (D u : ℂ)) = (zeroMultiplicityCount f c R : ℂ) := by unfold zeroMultiplicityCount rw [finsum_eq_sum_of_support_subset (s := hDfinite.toFinset) (fun u ↦ if u ∈ ball c R then analyticOrderNatAt f u else 0)] · push_cast apply Finset.sum_congr rfl intro u hu have huSupp : u ∈ D.support := by simpa using hu have huU : u ∈ U := (MeromorphicOn.divisor f U).supportWithinDomain huSupp have huNS : u ∉ sphere c R := by intro hus exact (show D u ≠ 0 by simpa using hu) (hDz u hus) have huB : u ∈ ball c R := by have huUdist : dist u c ≤ R := by simpa [U, mem_closedBall] using huU have hdistne : dist u c ≠ R := by intro h apply huNS exact h rw [mem_ball] exact lt_of_le_of_ne huUdist hdistne simp only [huB, if_true] congr 1 dsimp [D] rw [MeromorphicOn.divisor_apply hf.meromorphicOn huU, (hf u huU).meromorphicOrderAt_eq] have haufinite : analyticOrderAt f u ≠ ⊤ := by have hm := hfinite u huU rw [(hf u huU).meromorphicOrderAt_eq] at hm simpa using hm rw [← Nat.cast_analyticOrderNatAt haufinite] simp · intro u hu rw [Function.mem_support] at hu by_cases huB : u ∈ ball c R · have huU : u ∈ U := ball_subset_closedBall huB have haufinite : analyticOrderAt f u ≠ ⊤ := by have hm := hfinite u huU rw [(hf u huU).meromorphicOrderAt_eq] at hm simpa using hm have hDu : D u = (analyticOrderNatAt f u : ℤ) := by dsimp [D] rw [MeromorphicOn.divisor_apply hf.meromorphicOn huU, (hf u huU).meromorphicOrderAt_eq, ← Nat.cast_analyticOrderNatAt haufinite] simp have hnat : analyticOrderNatAt f u ≠ 0 := by simpa [huB] using hu have hDne : D u ≠ 0 := by rw [hDu] exact_mod_cast hnat rw [hDfinite.coe_toFinset, Function.mem_support] exact hDne · simp [huB] at hu rw [normalizedLogDerivCircleIntegral, hcircle, ← Finset.sum_mul, hsum] have hK : (2 * (Real.pi : ℂ) * I) ≠ 0 := by norm_num [Real.pi_ne_zero] rw [mul_comm (zeroMultiplicityCount f c R : ℂ), inv_mul_cancel_left₀ hK]

theorem rouche_circle {f g : ℂ → ℂ} {c : ℂ} {R : ℝ} (hR : 0 < R) (hf : AnalyticOnNhd ℂ f (closedBall c R)) (hg : AnalyticOnNhd ℂ g (closedBall c R)) (hrouche : ∀ z ∈ sphere c R, ‖g z - f z‖ < ‖f z‖) : zeroMultiplicityCount f c R = zeroMultiplicityCount g c R := by apply zeroMultiplicityCount_eq_of_straightLineHomotopy hR hf hg intro t ht z hz hzero have hzero' : f z + (t : ℂ) * (g z - f z) = 0 := by rw [← hzero] simp only [straightLineHomotopy] ring have hfeq : f z = -(t : ℂ) * (g z - f z) := by linear_combination hzero' have hnorm : ‖f z‖ = t * ‖g z - f z‖ := by calc ‖f z‖ = ‖-(t : ℂ) * (g z - f z)‖ := congrArg norm hfeq _ = t * ‖g z - f z‖ := by rw [norm_mul, norm_neg, Complex.norm_real, Real.norm_eq_abs, abs_of_nonneg ht.1] have hle : ‖f z‖ ≤ ‖g z - f z‖ := by rw [hnorm] simpa only [one_mul] using mul_le_mul_of_nonneg_right ht.2 (norm_nonneg (g z - f z)) exact (not_lt_of_ge hle) (hrouche z hz)