Integral over a circle in ℂ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define ∮ z in C(c, R), f z to be the integral $\oint_{|z-c|=|R|} f(z)\,dz$ and prove some properties of this integral. We give definition and prove most lemmas for a function f : ℂ → E, where E is a complex Banach space. For this reason, some lemmas use, e.g., (z - c)⁻¹ • f z instead of f z / (z - c).

Main definitions #

• circle_map c R: the exponential map $θ ↦ c + R e^{θi}$;

• circle_integrable f c R: a function f : ℂ → E is integrable on the circle with center c and radius R if f ∘ circle_map c R is integrable on [0, 2π];

• circle_integral f c R: the integral $\oint_{|z-c|=|R|} f(z)\,dz$, defined as $\int_{0}^{2π}(c + Re^{θ i})' f(c+Re^{θ i})\,dθ$;

• cauchy_power_series f c R: the power series that is equal to $\sum_{n=0}^{\infty} \oint_{|z-c|=R} \left(\frac{w-c}{z - c}\right)^n \frac{1}{z-c}f(z)\,dz$ at w - c. The coefficients of this power series depend only on f ∘ circle_map c R, and the power series converges to f w if f is differentiable on the closed ball metric.closed_ball c R and w belongs to the corresponding open ball.

Main statements #

• has_fpower_series_on_cauchy_integral: for any circle integrable function f, the power series cauchy_power_series f c R, R > 0, converges to the Cauchy integral (2 * π * I : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc metric.ball c R;

• circle_integral.integral_sub_zpow_of_undef, circle_integral.integral_sub_zpow_of_ne, and circle_integral.integral_sub_inv_of_mem_ball: formulas for ∮ z in C(c, R), (z - w) ^ n, n : ℤ. These lemmas cover the following cases:

  • circle_integral.integral_sub_zpow_of_undef, n < 0 and |w - c| = |R|: in this case the function is not integrable, so the integral is equal to its default value (zero);

  • circle_integral.integral_sub_zpow_of_ne, n ≠ -1: in the cases not covered by the previous lemma, we have (z - w) ^ n = ((z - w) ^ (n + 1) / (n + 1))', thus the integral equals zero;

  • circle_integral.integral_sub_inv_of_mem_ball, n = -1, |w - c| < R: in this case the integral is equal to 2πi.

  The case n = -1, |w -c| > R is not covered by these lemmas. While it is possible to construct an explicit primitive, it is easier to apply Cauchy theorem, so we postpone the proof till we have this theorem (see #10000).

Notation #

• ∮ z in C(c, R), f z: notation for the integral $\oint_{|z-c|=|R|} f(z)\,dz$, defined as $\int_{0}^{2π}(c + Re^{θ i})' f(c+Re^{θ i})\,dθ$.

Tags #

integral, circle, Cauchy integral

circle_map, a parametrization of a circle #

Integrability of a function on a circle #