Formal target: Corpus.WikipediaMeanValueProblem.mean_value_problem

Given a complex polynomial $p$ of degree $d ≥ 2$ and a complex number $z$ there is a critical point $c$ of $p$, such that $|p(z)-p(c)|/|z-c| ≤ |p'(z)|$.

Exact formal statement

∀ (p : Polynomial.{0} Complex),
  LE.le.{0} 2 (Polynomial.degree.{0} p) →
    ∀ (z : Complex) (K : Real),
      Exists.{1} fun c =>
        And (Eq.{1} (Polynomial.eval.{0} c (DFunLike.coe.{1, 1, 1} Polynomial.derivative.{0} p)) 0)
          (LE.le.{0}
            (HDiv.hDiv.{0, 0, 0}
              (Norm.norm.{0} (HSub.hSub.{0, 0, 0} (Polynomial.eval.{0} z p) (Polynomial.eval.{0} c p)))
              (Norm.norm.{0} (HSub.hSub.{0, 0, 0} z c)))
            (Norm.norm.{0} (Polynomial.eval.{0} z (DFunLike.coe.{1, 1, 1} Polynomial.derivative.{0} p))))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record