mathlib3 documentation

measure_theory.integral.circle_integral

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 #

noncomputable def circle_map (c : ℂ) (R : ℝ) :

The exponential map $θ ↦ c + R e^{θi}$. The range of this map is the circle in ℂ with center c and radius |R|.

Equations

circle_map c R = λ (θ : ℝ), c + ↑R * cexp (↑θ * complex.I)

theorem periodic_circle_map (c : ℂ) (R : ℝ) :

function.periodic (circle_map c R) (2 * real.pi)

circle_map is 2π-periodic.

theorem set.countable.preimage_circle_map {s : set ℂ} (hs : s.countable) (c : ℂ) {R : ℝ} (hR : R ≠ 0) :

(circle_map c R ⁻¹' s).countable

@[simp]

theorem circle_map_sub_center (c : ℂ) (R θ : ℝ) :

circle_map c R θ - c = circle_map 0 R θ

theorem circle_map_zero (R θ : ℝ) :

circle_map 0 R θ = ↑R * cexp (↑θ * complex.I)

@[simp]

theorem abs_circle_map_zero (R θ : ℝ) :

⇑complex.abs (circle_map 0 R θ) = |R|

theorem circle_map_mem_sphere' (c : ℂ) (R θ : ℝ) :

circle_map c R θ ∈ metric.sphere c |R|

theorem circle_map_mem_sphere (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) :

circle_map c R θ ∈ metric.sphere c R

theorem circle_map_mem_closed_ball (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) :

circle_map c R θ ∈ metric.closed_ball c R

theorem circle_map_not_mem_ball (c : ℂ) (R θ : ℝ) :

circle_map c R θ ∉ metric.ball c R

theorem circle_map_ne_mem_ball {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ metric.ball c R) (θ : ℝ) :

circle_map c R θ ≠ w

@[simp]

theorem range_circle_map (c : ℂ) (R : ℝ) :

set.range (circle_map c R) = metric.sphere c |R|

The range of circle_map c R is the circle with center c and radius |R|.

@[simp]

theorem image_circle_map_Ioc (c : ℂ) (R : ℝ) :

circle_map c R '' set.Ioc 0 (2 * real.pi) = metric.sphere c |R|

The image of (0, 2π] under circle_map c R is the circle with center c and radius |R|.

@[simp]

theorem circle_map_eq_center_iff {c : ℂ} {R θ : ℝ} :

circle_map c R θ = c ↔ R = 0

@[simp]

theorem circle_map_zero_radius (c : ℂ) :

circle_map c 0 = function.const ℝ c

theorem circle_map_ne_center {c : ℂ} {R : ℝ} (hR : R ≠ 0) {θ : ℝ} :

circle_map c R θ ≠ c

theorem has_deriv_at_circle_map (c : ℂ) (R θ : ℝ) :

has_deriv_at (circle_map c R) (circle_map 0 R θ * complex.I) θ

theorem differentiable_circle_map (c : ℂ) (R : ℝ) :

differentiable ℝ (circle_map c R)

@[continuity]

theorem continuous_circle_map (c : ℂ) (R : ℝ) :

continuous (circle_map c R)

@[measurability]

theorem measurable_circle_map (c : ℂ) (R : ℝ) :

measurable (circle_map c R)

@[simp]

theorem deriv_circle_map (c : ℂ) (R θ : ℝ) :

deriv (circle_map c R) θ = circle_map 0 R θ * complex.I

theorem deriv_circle_map_eq_zero_iff {c : ℂ} {R θ : ℝ} :

deriv (circle_map c R) θ = 0 ↔ R = 0

theorem deriv_circle_map_ne_zero {c : ℂ} {R θ : ℝ} (hR : R ≠ 0) :

deriv (circle_map c R) θ ≠ 0

theorem lipschitz_with_circle_map (c : ℂ) (R : ℝ) :

lipschitz_with (⇑real.nnabs R) (circle_map c R)

theorem continuous_circle_map_inv {R : ℝ} {z w : ℂ} (hw : w ∈ metric.ball z R) :

continuous (λ (θ : ℝ), (circle_map z R θ - w)⁻¹)

Integrability of a function on a circle #

def circle_integrable {E : Type u_1} [normed_add_comm_group E] (f : ℂ → E) (c : ℂ) (R : ℝ) :

Prop

We say that a function f : ℂ → E is integrable on the circle with center c and radius R if the function f ∘ circle_map c R is integrable on [0, 2π].

Note that the actual function used in the definition of circle_integral is (deriv (circle_map c R) θ) • f (circle_map c R θ). Integrability of this function is equivalent to integrability of f ∘ circle_map c R whenever R ≠ 0.

Equations

circle_integrable f c R = interval_integrable (λ (θ : ℝ), f (circle_map c R θ)) measure_theory.measure_space.volume 0 (2 * real.pi)

@[simp]

theorem circle_integrable_const {E : Type u_1} [normed_add_comm_group E] (a : E) (c : ℂ) (R : ℝ) :

circle_integrable (λ (_x : ℂ), a) c R

theorem circle_integrable.add {E : Type u_1} [normed_add_comm_group E] {f g : ℂ → E} {c : ℂ} {R : ℝ} (hf : circle_integrable f c R) (hg : circle_integrable g c R) :

circle_integrable (f + g) c R

theorem circle_integrable.neg {E : Type u_1} [normed_add_comm_group E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : circle_integrable f c R) :

circle_integrable (-f) c R

theorem circle_integrable.out {E : Type u_1} [normed_add_comm_group E] {f : ℂ → E} {c : ℂ} {R : ℝ} [normed_space ℂ E] (hf : circle_integrable f c R) :

interval_integrable (λ (θ : ℝ), deriv (circle_map c R) θ • f (circle_map c R θ)) measure_theory.measure_space.volume 0 (2 * real.pi)

The function we actually integrate over [0, 2π] in the definition of circle_integral is integrable.

@[simp]

theorem circle_integrable_zero_radius {E : Type u_1} [normed_add_comm_group E] {f : ℂ → E} {c : ℂ} :

circle_integrable f c 0

theorem circle_integrable_iff {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] {f : ℂ → E} {c : ℂ} (R : ℝ) :

circle_integrable f c R ↔ interval_integrable (λ (θ : ℝ), deriv (circle_map c R) θ • f (circle_map c R θ)) measure_theory.measure_space.volume 0 (2 * real.pi)

theorem continuous_on.circle_integrable' {E : Type u_1} [normed_add_comm_group E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : continuous_on f (metric.sphere c |R|)) :

circle_integrable f c R

theorem continuous_on.circle_integrable {E : Type u_1} [normed_add_comm_group E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (hf : continuous_on f (metric.sphere c R)) :

circle_integrable f c R

@[simp]

theorem circle_integrable_sub_zpow_iff {c w : ℂ} {R : ℝ} {n : ℤ} :

circle_integrable (λ (z : ℂ), (z - w) ^ n) c R ↔ R = 0 ∨ 0 ≤ n ∨ w ∉ metric.sphere c |R|

The function λ z, (z - w) ^ n, n : ℤ, is circle integrable on the circle with center c and radius |R| if and only if R = 0 or 0 ≤ n, or w does not belong to this circle.

@[simp]

theorem circle_integrable_sub_inv_iff {c w : ℂ} {R : ℝ} :

circle_integrable (λ (z : ℂ), (z - w)⁻¹) c R ↔ R = 0 ∨ w ∉ metric.sphere c |R|

noncomputable def circle_integral {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) (R : ℝ) :

E

Definition for $\oint_{|z-c|=R} f(z)\,dz$.

Equations

circle_integral f c R = ∫ (θ : ℝ) in 0..2 * real.pi, deriv (circle_map c R) θ • f (circle_map c R θ)

theorem circle_integral_def_Icc {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) (R : ℝ) :

∮ (z : ℂ) in C(c, R), f z = ∫ (θ : ℝ) in set.Icc 0 (2 * real.pi), deriv (circle_map c R) θ • f (circle_map c R θ)

@[simp]

theorem circle_integral.integral_radius_zero {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) :

∮ (z : ℂ) in C(c, 0), f z = 0

theorem circle_integral.integral_congr {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : set.eq_on f g (metric.sphere c R)) :

∮ (z : ℂ) in C(c, R), f z = ∮ (z : ℂ) in C(c, R), g z

theorem circle_integral.integral_sub_inv_smul_sub_smul {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c w : ℂ) (R : ℝ) :

∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z

theorem circle_integral.integral_undef {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ¬circle_integrable f c R) :

∮ (z : ℂ) in C(c, R), f z = 0

theorem circle_integral.integral_sub {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f g : ℂ → E} {c : ℂ} {R : ℝ} (hf : circle_integrable f c R) (hg : circle_integrable g c R) :

∮ (z : ℂ) in C(c, R), f z - g z = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z

theorem circle_integral.norm_integral_le_of_norm_le_const' {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hf : ∀ (z : ℂ), z ∈ metric.sphere c |R| → ‖f z‖ ≤ C) :

‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * real.pi * |R| * C

theorem circle_integral.norm_integral_le_of_norm_le_const {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R) (hf : ∀ (z : ℂ), z ∈ metric.sphere c R → ‖f z‖ ≤ C) :

‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * real.pi * R * C

theorem circle_integral.norm_two_pi_I_inv_smul_integral_le_of_norm_le_const {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R) (hf : ∀ (z : ℂ), z ∈ metric.sphere c R → ‖f z‖ ≤ C) :

‖(2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C

theorem circle_integral.norm_integral_lt_of_norm_le_const_of_lt {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 < R) (hc : continuous_on f (metric.sphere c R)) (hf : ∀ (z : ℂ), z ∈ metric.sphere c R → ‖f z‖ ≤ C) (hlt : ∃ (z : ℂ) (H : z ∈ metric.sphere c R), ‖f z‖ < C) :

‖∮ (z : ℂ) in C(c, R), f z‖ < 2 * real.pi * R * C

If f is continuous on the circle |z - c| = R, R > 0, the ‖f z‖ is less than or equal to C : ℝ on this circle, and this norm is strictly less than C at some point z of the circle, then ‖∮ z in C(c, R), f z‖ < 2 * π * R * C.

@[simp]

theorem circle_integral.integral_smul {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {𝕜 : Type u_2} [is_R_or_C 𝕜] [normed_space 𝕜 E] [smul_comm_class 𝕜 ℂ E] (a : 𝕜) (f : ℂ → E) (c : ℂ) (R : ℝ) :

∮ (z : ℂ) in C(c, R), a • f z = a • ∮ (z : ℂ) in C(c, R), f z

@[simp]

theorem circle_integral.integral_smul_const {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → ℂ) (a : E) (c : ℂ) (R : ℝ) :

∮ (z : ℂ) in C(c, R), f z • a = (∮ (z : ℂ) in C(c, R), f z) • a

@[simp]

theorem circle_integral.integral_const_mul (a : ℂ) (f : ℂ → ℂ) (c : ℂ) (R : ℝ) :

∮ (z : ℂ) in C(c, R), a * f z = a * ∮ (z : ℂ) in C(c, R), f z

@[simp]

theorem circle_integral.integral_sub_center_inv (c : ℂ) {R : ℝ} (hR : R ≠ 0) :

∮ (z : ℂ) in C(c, R), (z - c)⁻¹ = 2 * ↑real.pi * complex.I

theorem circle_integral.integral_eq_zero_of_has_deriv_within_at' {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f f' : ℂ → E} {c : ℂ} {R : ℝ} (h : ∀ (z : ℂ), z ∈ metric.sphere c |R| → has_deriv_within_at f (f' z) (metric.sphere c |R|) z) :

∮ (z : ℂ) in C(c, R), f' z = 0

If f' : ℂ → E is a derivative of a complex differentiable function on the circle metric.sphere c |R|, then ∮ z in C(c, R), f' z = 0.

theorem circle_integral.integral_eq_zero_of_has_deriv_within_at {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f f' : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : ∀ (z : ℂ), z ∈ metric.sphere c R → has_deriv_within_at f (f' z) (metric.sphere c R) z) :

∮ (z : ℂ) in C(c, R), f' z = 0

If f' : ℂ → E is a derivative of a complex differentiable function on the circle metric.sphere c R, then ∮ z in C(c, R), f' z = 0.

theorem circle_integral.integral_sub_zpow_of_undef {n : ℤ} {c w : ℂ} {R : ℝ} (hn : n < 0) (hw : w ∈ metric.sphere c |R|) :

∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

If n < 0 and |w - c| = |R|, then (z - w) ^ n is not circle integrable on the circle with center c and radius (|R|), so the integral ∮ z in C(c, R), (z - w) ^ n is equal to zero.

theorem circle_integral.integral_sub_zpow_of_ne {n : ℤ} (hn : n ≠ -1) (c w : ℂ) (R : ℝ) :

∮ (z : ℂ) in C(c, R), (z - w) ^ n = 0

If n ≠ -1 is an integer number, then the integral of (z - w) ^ n over the circle equals zero.

noncomputable def cauchy_power_series {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) (R : ℝ) :

formal_multilinear_series ℂ ℂ E

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. For any circle integrable function f, this power series converges to the Cauchy integral for f.

Equations

cauchy_power_series f c R = λ (n : ℕ), continuous_multilinear_map.mk_pi_field ℂ (fin n) ((2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ n • (z - c)⁻¹ • f z)

theorem cauchy_power_series_apply {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) (w : ℂ) :

⇑(cauchy_power_series f c R n) (λ (_x : fin n), w) = (2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z

theorem norm_cauchy_power_series_le {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) (R : ℝ) (n : ℕ) :

‖cauchy_power_series f c R n‖ ≤ ((2 * real.pi)⁻¹ * ∫ (θ : ℝ) in 0..2 * real.pi, ‖f (circle_map c R θ)‖) * |R|⁻¹ ^ n

theorem le_radius_cauchy_power_series {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] (f : ℂ → E) (c : ℂ) (R : nnreal) :

↑R ≤ (cauchy_power_series f c ↑R).radius

theorem has_sum_two_pi_I_cauchy_power_series_integral {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : circle_integrable f c R) (hw : ⇑complex.abs w < R) :

has_sum (λ (n : ℕ), ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z) (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

For any circle integrable function f, the power series cauchy_power_series f c R multiplied by 2πI converges to the integral ∮ z in C(c, R), (z - w)⁻¹ • f z on the open disc metric.ball c R.

theorem has_sum_cauchy_power_series_integral {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : circle_integrable f c R) (hw : ⇑complex.abs w < R) :

has_sum (λ (n : ℕ), ⇑(cauchy_power_series f c R n) (λ (_x : fin n), w)) ((2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)

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.

theorem sum_cauchy_power_series_eq_integral {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ} (hf : circle_integrable f c R) (hw : ⇑complex.abs w < R) :

(cauchy_power_series f c R).sum w = (2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z

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.

theorem has_fpower_series_on_cauchy_integral {E : Type u_1} [normed_add_comm_group E] [normed_space ℂ E] [complete_space E] {f : ℂ → E} {c : ℂ} {R : nnreal} (hf : circle_integrable f c ↑R) (hR : 0 < R) :

has_fpower_series_on_ball (λ (w : ℂ), (2 * ↑real.pi * complex.I)⁻¹ • ∮ (z : ℂ) in C(c, ↑R), (z - w)⁻¹ • f z) (cauchy_power_series f c ↑R) c ↑R

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.

theorem circle_integral.integral_sub_inv_of_mem_ball {c w : ℂ} {R : ℝ} (hw : w ∈ metric.ball c R) :

∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 2 * ↑real.pi * complex.I

Integral $\oint_{|z-c|=R} \frac{dz}{z-w}=2πi$ whenever $|w-c|