Rouche theorem via zero counting | Lean AI formalization leaderboard

Problem statement

Notes: Phrases Rouché's theorem as equality of multiplicity-counted zero counts for f and f + g on the closed disk of radius R.

Source: Classical theorem in complex analysis.

Informal solution: Assuming f is meromorphic in normal form on ℂ and |g| < |f| on the boundary circle, f and f + g have the same number of zeros inside the disk, counted with multiplicity.

theorem declaration uses `sorry`rouche_zero_count_eq {f g : ℂ → ℂ} {R : ℝ}
    (hR : 0 < R)
    (hf : MeromorphicNFOn f Set.univ)
    (hg : AnalyticOn ℂ g Set.univ)
    (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) :
    (∑ᶠ z, ((divisor (f + g) (Metric.closedBall 0 R))⁺) z) =
      (∑ᶠ z, ((divisor f (Metric.closedBall 0 R))⁺) z) := byf:ℂ → ℂg:ℂ → ℂR:ℝhR:0 < Rhf:MeromorphicNFOn f Set.univhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ ∑ᶠ (z : ℂ), (divisor (f + g) (Metric.closedBall 0 R))⁺ z = ∑ᶠ (z : ℂ), (divisor f (Metric.closedBall 0 R))⁺ z
  sorryAll goals completed! 🐙