Source indexedtheorem · leanprover/lean4:v4.32.0

Polynomial.logDeriv_exp_eval

PrimeNumberTheoremAnd.Mathlib.Analysis.Calculus.Deriv.Polynomial · PrimeNumberTheoremAnd/Mathlib/Analysis/Calculus/Deriv/Polynomial.lean:20 to 29

Source documentation

The logarithmic derivative of the exponential of a complex polynomial is the polynomial derivative.

Exact Lean statement

theorem logDeriv_exp_eval (P : ℂ[X]) (z : ℂ) :
    logDeriv (fun w : ℂ => Complex.exp (Polynomial.eval w P)) z =
      Polynomial.eval z P.derivative

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem logDeriv_exp_eval (P : ℂ[X]) (z : ℂ) :    logDeriv (fun w : ℂ => Complex.exp (Polynomial.eval w P)) z =      Polynomial.eval z P.derivative := by  have hderiv :      deriv (fun w : ℂ => Complex.exp (Polynomial.eval w P)) z =        Complex.exp (Polynomial.eval z P) * Polynomial.eval z P.derivative := by    simpa [Function.comp_def, mul_comm] using      ((Complex.hasDerivAt_exp (Polynomial.eval z P)).comp z (P.hasDerivAt z)).deriv  rw [logDeriv_apply, hderiv]  field_simp [Complex.exp_ne_zero (Polynomial.eval z P)]