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](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Different.20Expressions.20of.20Cauchy's.20integral.20formula/with/545945033)

I also used Cauchy's estimate over here: [#mathlib4 > Tychonov's Counterexample for the Heat Equation](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Tychonov's.20Counterexample.20for.20the.20Heat.20Equation/with/547367912)

Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Author: CoolRmal

Mathlib/Analysis/Complex/CauchyIntegral.lean

@@ -25,6 +25,8 @@ Banach space with second countable topology.
 In the following theorems, if the name ends with `off_countable`, then the actual theorem assumes
 differentiability at all but countably many points of the set mentioned below.
 
+### Rectangle integrals
+
 * `Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable`: If a function
   `f : ℂ → E` is continuous on a closed rectangle and *real* differentiable on its interior, then
   its integral over the boundary of this rectangle is equal to the integral of
@@ -35,6 +37,8 @@ differentiability at all but countably many points of the set mentioned below.
   `f : ℂ → E` is continuous on a closed rectangle and is *complex* differentiable on its interior,
   then its integral over the boundary of this rectangle is equal to zero.
 
+### Annuli and circles
+
 * `Complex.circleIntegral_sub_center_inv_smul_eq_of_differentiable_on_annulus_off_countable`: If a
   function `f : ℂ → E` is continuous on a closed annulus `{z | r ≤ |z - c| ≤ R}` and is complex
   differentiable on its interior `{z | r < |z - c| < R}`, then the integrals of `(z - c)⁻¹ • f z`
@@ -55,6 +59,8 @@ differentiability at all but countably many points of the set mentioned below.
   disc the integral of `(z - w)⁻¹ • f z` over the boundary of the disc is equal to `2πif(w)`.
   Two versions of the lemma put the multiplier `2πi` at the different sides of the equality.
 
+### Analyticity
+
 * `Complex.hasFPowerSeriesOnBall_of_differentiable_off_countable`: If `f : ℂ → E` is continuous
   on a closed disc of positive radius and is complex differentiable on the corresponding open disc,
   then it is analytic on the corresponding open disc, and the coefficients of the power series are
@@ -72,6 +78,13 @@ differentiability at all but countably many points of the set mentioned below.
   `cauchyPowerSeries f z R` is a formal power series representing `f` at `z` with infinite
   radius of convergence (this holds for any choice of `0 < R`).
 
+### Higher derivatives
+
+* `Complex.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable`
+  **Cauchy integral formula for derivatives**: formula for the higher derivatives of `f` at the
+  centre `c` of a disc in terms of circle integrals of `f w / (w - c) ^ (n + 1)` around the
+  boundary circle.
+
 ## Implementation details
 
 The proof of the Cauchy integral formula in this file is based on a very general version of the
@@ -155,6 +168,11 @@ variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E]
 
 namespace Complex
 
+section rectangle
+/-!
+## Functions on rectangles
+-/
+
 /-- Suppose that a function `f : ℂ → E` is continuous on a closed rectangle with opposite corners at
 `z w : ℂ`, is *real* differentiable at all but countably many points of the corresponding open
 rectangle, and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the
@@ -280,6 +298,13 @@ theorem integral_boundary_rect_eq_zero_of_differentiableOn (f : ℂ → E) (z w
     H.mono <|
       inter_subset_inter (preimage_mono Ioo_subset_Icc_self) (preimage_mono Ioo_subset_Icc_self)
 
+end rectangle
+
+section annulus
+/-!
+## Functions on annuli
+-/
+
 /-- If `f : ℂ → E` is continuous on the closed annulus `r ≤ ‖z - c‖ ≤ R`, `0 < r ≤ R`,
 and is complex differentiable at all but countably many points of its interior,
 then the integrals of `f z / (z - c)` (formally, `(z - c)⁻¹ • f z`)
@@ -334,8 +359,15 @@ theorem circleIntegral_eq_of_differentiable_on_annulus_off_countable {c : ℂ} {
         (differentiableAt_id.sub_const _).smul (hd z hz))
     _ = ∮ z in C(c, r), f z := circleIntegral.integral_sub_inv_smul_sub_smul _ _ _ _
 
+end annulus
+
 variable [CompleteSpace E]
 
+section circle
+/-!
+## Circle integrals
+-/
+
 /-- **Cauchy integral formula** for the value at the center of a disc. If `f` is continuous on a
 punctured closed disc of radius `R`, is differentiable at all but countably many points of the
 interior of this disc, and has a limit `y` at the center of the disc, then the integral
@@ -533,6 +565,13 @@ theorem circleIntegral_div_sub_of_differentiable_on_off_countable {R : ℝ} {c w
   simpa only [smul_eq_mul, div_eq_inv_mul] using
     circleIntegral_sub_inv_smul_of_differentiable_on_off_countable hs hw hc hd
 
+end circle
+
+section analyticity
+/-!
+## Applications to analyticity
+-/
+
 /-- If `f : ℂ → E` is continuous on a closed ball of positive radius and is differentiable at all
 but countably many points of the corresponding open ball, then it is analytic on the open ball with
 coefficients of the power series given by Cauchy integral formulas. -/
@@ -650,4 +689,71 @@ theorem analyticAt_iff_eventually_differentiableAt {f : ℂ → E} {c : ℂ} :
       exact (d z m).differentiableWithinAt
     exact h _ m
 
+end analyticity
+
+section derivatives
+/-!
+## Circle integrals for higher derivatives
+
+TODO: add a version for `w ∈ Metric.ball c R`.
+-/
+
+variable {R : ℝ} {f : ℂ → E} {c : ℂ} {s : Set ℂ}
+
+/-- **Cauchy integral formula for derivatives**, assuming `f` is continuous on a closed ball and
+differentiable on its interior away from a countable set. -/
+lemma circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable
+    (h0 : 0 < R) (n : ℕ) (hs : s.Countable)
+    (hc : ContinuousOn f (closedBall c R)) (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
+    ∮ z in C(c, R), (1 / (z - c) ^ (n + 1)) • f z
+      = (2 * π * I / n.factorial) • iteratedDeriv n f c := by
+  have := hasFPowerSeriesOnBall_of_differentiable_off_countable (R := ⟨R, h0.le⟩) hs hc hd h0
+      |>.factorial_smul 1 n
+  rw [iteratedFDeriv_apply_eq_iteratedDeriv_mul_prod, Finset.prod_const_one, one_smul] at this
+  rw [← this, cauchyPowerSeries_apply, ← Nat.cast_smul_eq_nsmul ℂ, ← mul_smul, ← mul_smul,
+    div_mul_cancel₀ _ (mod_cast n.factorial_ne_zero), mul_inv_cancel₀ two_pi_I_ne_zero]
+  simp [← mul_smul, pow_succ, mul_comm]
+
+/-- **Cauchy integral formula for the first order derivative**, assuming `f` is continuous on a
+closed ball and differentiable on its interior away from a countable set. -/
+lemma differentiable_on_off_countable_deriv_eq_smul_circleIntegral
+    (h0 : 0 < R) (hs : s.Countable) (hc : ContinuousOn f (closedBall c R))
+    (hd : ∀ z ∈ ball c R \ s, DifferentiableAt ℂ f z) :
+    ∮ z in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * π * I) • deriv f c := by
+  simpa using circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable
+    h0 1 hs hc hd
+
+/-- **Cauchy integral formula for derivatives**, assuming `f` is continuous on a closed ball and
+differentiable on its interior. -/
+lemma _root_.DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul
+    (h0 : 0 < R) (n : ℕ) (hc : DiffContOnCl ℂ f (ball c R)) :
+    ∮ z in C(c, R), (1 / (z - c) ^ (n + 1)) • f z
+      = (2 * π * I / n.factorial) • iteratedDeriv n f c :=
+  c.circleIntegral_one_div_sub_center_pow_smul_of_differentiable_on_off_countable h0 n
+    Set.countable_empty hc.continuousOn_ball fun _ hx ↦ hc.differentiableAt isOpen_ball hx.1
+
+/-- **Cauchy integral formula for the first order derivative**, assuming `f` is continuous on a
+closed ball and differentiable on its interior. -/
+lemma _root_.DiffContOnCl.deriv_eq_smul_circleIntegral (h0 : 0 < R)
+    (hc : DiffContOnCl ℂ f (ball c R)) :
+    ∮ z in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * π * I) • deriv f c := by
+  simpa using DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul h0 1 hc
+
+/-- **Cauchy integral formula for derivatives**, assuming `f` is differentiable on a closed ball. -/
+lemma _root_.DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul (h0 : 0 < R) (n : ℕ)
+    (hc : DifferentiableOn ℂ f (closedBall c R)) :
+    ∮ z in C(c, R), (1 / (z - c) ^ (n + 1)) • f z
+      = (2 * π * I / n.factorial) • iteratedDeriv n f c :=
+  (hc.mono closure_ball_subset_closedBall).diffContOnCl
+    |>.circleIntegral_one_div_sub_center_pow_smul h0 n
+
+/-- **Cauchy integral formula for the first order derivative**, assuming `f` is differentiable on
+a closed ball. -/
+lemma _root_.DifferentiableOn.deriv_eq_smul_circleIntegral (h0 : 0 < R)
+    (hc : DifferentiableOn ℂ f (closedBall c R)) :
+    ∮ z in C(c, R), (1 / (z - c) ^ 2) • f z = (2 * π * I) • deriv f c := by
+  simpa using DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul h0 1 hc
+
+end derivatives
+
 end Complex

Mathlib/Analysis/Complex/Liouville.lean

@@ -33,37 +33,42 @@ local postfix:100 "̂" => UniformSpace.Completion
 
 namespace Complex
 
-/-- If `f` is complex differentiable on an open disc with center `c` and radius `R > 0` and is
-continuous on its closure, then `f' c` can be represented as an integral over the corresponding
-circle.
-
-TODO: add a version for `w ∈ Metric.ball c R`.
-
-TODO: add a version for higher derivatives. -/
-theorem deriv_eq_smul_circleIntegral [CompleteSpace F] {R : ℝ} {c : ℂ} {f : ℂ → F} (hR : 0 < R)
-    (hf : DiffContOnCl ℂ f (ball c R)) :
-    deriv f c = (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z := by
-  lift R to ℝ≥0 using hR.le
-  refine (hf.hasFPowerSeriesOnBall hR).hasFPowerSeriesAt.deriv.trans ?_
-  simp only [cauchyPowerSeries_apply, one_div, zpow_neg, pow_one, smul_smul, zpow_two, mul_inv]
-
-theorem norm_deriv_le_aux [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
+/-- **Cauchy's estimate for derivatives**:  If `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 its `n`-th derivative at the center is at most
+`n.factorial * C / R ^ n`. -/
+theorem norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le [CompleteSpace F] {c : ℂ} {R C : ℝ}
+    {f : ℂ → F} (n : ℕ) (hR : 0 < R) (hf : DiffContOnCl ℂ f (ball c R))
+    (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) :
+    ‖iteratedDeriv n f c‖ ≤ n.factorial * C / R ^ n := by
+  have hp (z) (hz : ‖z - c‖ = R) : ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n  * R) := by
+    simpa [norm_smul, norm_pow, norm_inv, hz, ← div_eq_inv_mul] using
+      (div_le_div_iff_of_pos_right (mul_pos (pow_pos hR n) hR)).2 (hC z hz)
+  have hq : iteratedDeriv n f c = n.factorial • (2 * π * I)⁻¹ •
+    ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z := by
+    have : (2 * π * I / n.factorial) ≠ 0 := by simp [Nat.factorial_ne_zero]
+    rw [← inv_smul_smul₀ this (iteratedDeriv n f c), inv_div, div_eq_inv_mul, mul_comm,
+      ← nsmul_eq_mul, smul_assoc]
+    simp [← DiffContOnCl.circleIntegral_one_div_sub_center_pow_smul hR n hf]
+  calc
+    ‖iteratedDeriv n f c‖ = ‖n.factorial • (2 * π * I)⁻¹ •
+      ∮ z in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z‖ := by rw [hq]
+    _ ≤ n.factorial * (R * (C / (R ^ (n + 1)))) := by
+      rw [RCLike.norm_nsmul (K := ℂ), nsmul_eq_mul, mul_le_mul_iff_right₀ (by positivity)]
+      exact circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le hp
+    _ = n.factorial * C / R ^ n := by
+      grind
+
+private theorem norm_deriv_le_aux [CompleteSpace F] {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
     (hf : DiffContOnCl ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) :
     ‖deriv f c‖ ≤ C / R := by
-  have : ∀ z ∈ sphere c R, ‖(z - c) ^ (-2 : ℤ) • f z‖ ≤ C / (R * R) :=
-    fun z (hz : ‖z - c‖ = R) => by
-    simpa [-mul_inv_rev, norm_smul, hz, zpow_two, ← div_eq_inv_mul] using
-      (div_le_div_iff_of_pos_right (mul_pos hR hR)).2 (hC z hz)
-  calc
-    ‖deriv f c‖ = ‖(2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-2 : ℤ) • f z‖ :=
-      congr_arg norm (deriv_eq_smul_circleIntegral hR hf)
-    _ ≤ R * (C / (R * R)) :=
-      (circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const hR.le this)
-    _ = C / R := by rw [mul_div_left_comm, div_self_mul_self', div_eq_mul_inv]
-
-/-- If `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 its derivative at the center is at most `C / R`. -/
+  simpa using norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le 1 hR hf hC
+
+/-- **Cauchy's estimate for the first order derivative**: If `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 its derivative at the center is at
+most `C / R`. Note that this theorem does not require the completeness of the codomain of `f`. In
+constrast, the completeness is needed for `norm_iteratedDeriv_le_of_forall_mem_sphere_norm_le`. -/
 theorem norm_deriv_le_of_forall_mem_sphere_norm_le {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
     (hd : DiffContOnCl ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) :
     ‖deriv f c‖ ≤ C / R := by

Mathlib/MeasureTheory/Integral/CircleIntegral.lean

@@ -326,7 +326,7 @@ def circleIntegral (f : ℂ → E) (c : ℂ) (R : ℝ) : E :=
   ∫ θ : ℝ in 0..2 * π, deriv (circleMap c R) θ • f (circleMap c R θ)
 
 /-- `∮ z in C(c, R), f z` is the circle integral $\oint_{|z-c|=R} f(z)\,dz$. -/
-notation3 "∮ "(...)" in ""C("c", "R")"", "r:(scoped f => circleIntegral f c R) => r
+notation3 "∮ "(...)" in ""C("c", "R")"", "r:60:(scoped f => circleIntegral f c R) => r
 
 theorem circleIntegral_def_Icc (f : ℂ → E) (c : ℂ) (R : ℝ) :
     (∮ z in C(c, R), f z) = ∫ θ in Icc 0 (2 * π),