Different Expressions of Cauchy's integral formula

Stream: mathlib4

[Yongxi Lin (Aaron)]

@David Loeffler and I made two separates PRs #30473 and #30512 for Cauchy's integral formula for higher order derivatives. I am now trying to merge these two PRs. I want to ask what is the preferred expression of this formula by the Mathlib community. Let f : ℂ → F be a differentiable function and c a point in the complex plane. We currently have at least two options:

1. iteratedDeriv n f c = n.factorial • (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z. This is the formulation used by cauchyPowerSeries.

2. iteratedDeriv n f c = n.factorial • (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (- (n + 1)) • f z. I think this is more common on the standard textbook and it appears on the Wikipedia page (https://en.wikipedia.org/wiki/Cauchy%27s_integral_formula).

There are potentially many more options. e.g. ((z - c)⁻¹ )^(n + 1) or (1/(z - c ))^(n + 1). Is there a convention adopted by the Mathlib community that can help me decide which form I should pick?

[Jireh Loreaux]

Does simp have a preferred surviving here? This wild at least rule out the 1 / ... spelling.

[Yongxi Lin (Aaron)]

simp at the first one gives iteratedDeriv n f c = -(n.factorial • (I * ((↑π)⁻¹ * 2⁻¹)) • ∮ (z : ℂ) in C(c, R), ((z - c) ^ n)⁻¹ • (z - c)⁻¹ • f z).

[Weiyi Wang]

Asking about history here, is there a particular reason cauchyPowerSeries is defined with(z - c)⁻¹ ^ n • (z - c)⁻¹ • ?

[David Loeffler]

So simpapplies a bunch of other transformations, which seem undesirable here, but it looks like it does not transform 1. into 2. or vice versa. My vote is with 2. I don’t know why the existing CauchyPowerSeries code uses 1. but it is not indicative of any general mathlib convention AFAIK.