Cauchy's integral formula

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

Is there Cauchy's integral formula for higher order derivatives? I found that we have Complex.cderiv_eq_deriv.

[Jireh Loreaux]

I think we only have docs#Complex.deriv_eq_smul_circleIntegral

[Alastair Irving]

There's also docs#Complex.two_pi_I_inv_smul_circleIntegral_sub_sq_inv_smul_of_differentiable which is slightly more general, giving the derivative at any point not just the centre of the ball, but still only the first derivative. Do we really need both results?

[Kenny Lau]

iirc it was very easy to go from 1 to n (just use the formula itself)

[Kenny Lau]

(ok maybe not "that" easy, since you need to differentiate under the integral)

[Kenny Lau]

wait

[Kenny Lau]

DifferentiableOn.hasFPowerSeriesOnBall claims that "the coefficients of the power series are given by Cauchy integral formulas."

[Yongxi Lin (Aaron)]

oh so the keyword is cauchyPowerSeries

[Kenny Lau]

aha

[Yongxi Lin (Aaron)]

thanks for finding it :rolling_on_the_floor_laughing:

[Kenny Lau]

I found that out by:

1. noting that, this result would have already used the "derivative under the integral", because the starting point is actually the 0th derivative
2. so i decided to inspect the Lean code of the theorem given
3. then I found this result

[Yongxi Lin (Aaron)]

But is it really obvious (in lean) to deduce from DifferentiableOn.hasFPowerSeriesOnBall that the n-th derivative of a holomorphic function f is equal to n! * (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z.

[Kenny Lau]

it should be

[Yongxi Lin (Aaron)]

This is what I want:

import Mathlib

open Complex

variable {f : ℂ → ℂ} {z : ℂ} {U : Set ℂ} {n : ℕ} (hf : DifferentiableOn ℂ f U)

theorem citeratedDeriv_eq_iteratedDeriv {r : ℝ} (hr : 0 < r) (hzr : Metric.closedBall z r ⊆ U) :
    iteratedDeriv n f z =
    n.factorial * (2 * π * Complex.I : ℂ)⁻¹ • ∮ w in C(z, r), (z - w)⁻¹ ^ n • (z - w)⁻¹ • f z := by
  sorry

[Kenny Lau]

HasFPowerSeriesOnBall.factorial_smul

[Yury G. Kudryashov]

A PR that adds iteratedDeriv version of the latter lemma and uses it to get the Cauchy's integral formula is very welcome!

[Yongxi Lin (Aaron)]

I created a PR over here: https://github.com/leanprover-community/mathlib4/pull/30473. In this PR, I only generalize the Cauchy's integral formula to n-th order derivatives by assuming that f : ℂ -> F satisfies DiffContOnCl ℂ f (ball c R). I'll make another PR (or maybe just edit this existing PR) very soon to generalize cderiv_eq_deriv to the n-th order derivative (this theorem assumes that f is differentiable on some open set U and some closed ball is contained inside U).

[Yongxi Lin (Aaron)]

I also tried to generalize norm_deriv_le_of_forall_mem_sphere_norm_le for the n-th order derivatives. That is, I want to prove that if f : ℂ -> F is complex differentiable on an open disc of radius R > 0, is continuous on its
closure, and its values on the boundary circle of this disc are bounded from above by C, then the
norm of iteratedDeriv n f c is at most n.factorial * C / R ^ n. I proved this with the assumption [CompleteSpace F]in #30473. Then I tried to remove this assumption by considering the completion of Fand use HasFTaylorSeriesUpToOn.continuousLinearMap_comp and Complex.analyticOn_iff_differentiableOn, but this approach fails because I still need to assume [CompleteSpace F] in order to apply Complex.analyticOn_iff_differentiableOn. It is very weird to me that we can prove Cauchy's estimate for the first order derivatives without the completeness assumption but fails to do so for the higher order derivatives.