Theorems · Theorem · complex analysis

AnalyticOnNhd.sum_divisor_le

∀ {c : ℂ} {r R M : ℝ} {f : ℂ → ℂ},
  0 < |r| →
    |r| < |R| →
      1 ≤ M →
        AnalyticOnNhd ℂ f (Metric.closedBall c |R|) →
          f c ≠ 0 →
            (∀ z ∈ Metric.sphere c |R|, ‖f z‖ ≤ M) →
              ↑(∑ᶠ (u : ℂ), (MeromorphicOn.divisor f (Metric.closedBall c |r|)) u) ≤
                Real.log (M / ‖f c‖) / Real.log (R / r)

Jensen's Inequality: Estimates the number of zeros of f in a ball of radius r given that f is analytic and bounded by M on a larger ball of radius R.

Defined in

Mathlib.Analysis.Complex.JensenFormula

Cited by

0 results in Mathlib

Foundations

Depth 299 from the axioms · uses propext, Classical.choice, Quot.sound