Commit 2025-11-03 21:03 3eea33ec
View on Github →feat(ComplexAnalysis): Cauchy's Integral Formula for Higher Order Derivatives (#30473)
This PR adds the following iteratedDeriv_eq_smul_circleIntegral and norm_iteratedDeriv_le_aux. The first one expresses the n-th order derivative of a differentiable function as a circle integral. The second one proves an estimate for the n-th order derivative.
Zulip discussion: https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Cauchy's.20integral.20formula
#mathlib4 > Different Expressions of Cauchy's integral formula
I also used Cauchy's estimate over here: #mathlib4 > Tychonov's Counterexample for the Heat Equation