Rouche theorem via zero counting

rouche_logCounting_zero_eq

Submitter: Kim Morrison.

Notes: Phrases Rouché's theorem as equality of zero-counting functions for f and f + g.

Source: Classical theorem in complex analysis.

Informal solution: If |g| < |f| on the boundary circle, then f and f + g have the same number of zeros inside, counted with multiplicity.

theorem declaration uses `sorry`rouche_logCounting_zero_eq {f g : ℂ → ℂ} {R : ℝ}
    (hR : 1 ≤ R)
    (hf : Meromorphic f)
    (hg : AnalyticOn ℂ g Set.univ)
    (hbound : ∀ z : ℂ, ‖z‖ = R → ‖g z‖ < ‖f z‖) :
    logCounting (f + g) 0 R = logCounting f 0 R := byf:ℂ → ℂg:ℂ → ℂR:ℝhR:1 ≤ Rhf:Meromorphic fhg:AnalyticOn ℂ g Set.univhbound:∀ (z : ℂ), ‖z‖ = R → ‖g z‖ < ‖f z‖⊢ logCounting (f + g) 0 R = logCounting f 0 R
  sorryAll goals completed! 🐙

Solved by

Not yet solved.