Rouché's theorem

TheoremRouché's theorem on a disc#✓fully proved

Let \(c \in \mathbb{C}\) and \(R > 0\), and let \(f\) and \(g\) be analytic at every point of the closed disc \(|z - c| \le R\). If \(|g(z)| < |f(z)|\) for every \(z\) on the circle \(|z - c| = R\), then \(f\) and \(f + g\) have the same number of zeros in the open disc \(|z - c| < R\), counted with multiplicity: the divisors of \(f\) and of \(f + g\) on the open disc have equal sums.

theorem rouche_closedBall
    {c : ℂ} {R : ℝ} (hR : 0 < R)
    {f g : ℂ → ℂ}
    (hf : AnalyticOnNhd ℂ f (Metric.closedBall c R))
    (hg : AnalyticOnNhd ℂ g (Metric.closedBall c R))
    (hfg : ∀ z ∈ Metric.sphere c R, ‖g z‖ < ‖f z‖) :
    ∑ᶠ z, MeromorphicOn.divisor f (Metric.ball c R) z =
    ∑ᶠ z, MeromorphicOn.divisor (fun z => f z + g z) (Metric.ball c R) z

Sources

• E. Rouché, Mémoire sur la série de Lagrange, J. École Polytechnique 22 (1862), 193-224

TheoremRouché's theorem#●ready to prove

Let \(R > 0\), let \(f : \mathbb{C} \to \mathbb{C}\) be meromorphic on \(\mathbb{C}\) and in normal form (at every point \(f\) is either analytic, or has a pole and takes the value \(0\) there), and let \(g : \mathbb{C} \to \mathbb{C}\) be analytic on \(\mathbb{C}\). If \(|g(z)| < |f(z)|\) for every \(z\) with \(|z| = R\), then \(f + g\) and \(f\) have the same number of zeros in the closed disk \(|z| \le R\), counted with multiplicity: the sum over the points of the disk of the positive part of the order of \(f + g\) equals the same sum for \(f\).

public theorem_wanted 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)

Sources

• E. Rouché, Mémoire sur la série de Lagrange, J. École Polytechnique 22 (1862) (Rouché's theorem). Problem rouche of the lean-eval benchmark.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.