mathlib documentation

measure_theory.integral.circle_integral

Integral over a circle in #

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 #

Main statements #

Notation #

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
theorem periodic_circle_map (c : ) (R : ) :

circle_map is -periodic.

theorem set.countable.preimage_circle_map {s : set } (hs : s.countable) (c : ) {R : } (hR : R 0) :
@[simp]
theorem circle_map_sub_center (c : ) (R θ : ) :
circle_map c R θ - c = circle_map 0 R θ
theorem circle_map_zero (R θ : ) :
@[simp]
theorem abs_circle_map_zero (R θ : ) :
theorem circle_map_mem_sphere' (c : ) (R θ : ) :
theorem circle_map_mem_sphere (c : ) {R : } (hR : 0 R) (θ : ) :
theorem circle_map_mem_closed_ball (c : ) {R : } (hR : 0 R) (θ : ) :
@[simp]
theorem range_circle_map (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 : ) :

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
theorem circle_map_ne_center {c : } {R : } (hR : R 0) {θ : } :
circle_map c R θ c
theorem has_deriv_at_circle_map (c : ) (R θ : ) :
@[continuity]
theorem continuous_circle_map (c : ) (R : ) :
theorem measurable_circle_map (c : ) (R : ) :
@[simp]
theorem deriv_circle_map (c : ) (R θ : ) :
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

Integrability of a function on a circle #

def circle_integrable {E : Type u_1} [normed_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
@[simp]
theorem circle_integrable_const {E : Type u_1} [normed_group E] (a : E) (c : ) (R : ) :
circle_integrable (λ (_x : ), a) c R
theorem circle_integrable.add {E : Type u_1} [normed_group E] {f g : → E} {c : } {R : } (hf : circle_integrable f c R) (hg : circle_integrable g c R) :
theorem circle_integrable.neg {E : Type u_1} [normed_group E] {f : → E} {c : } {R : } (hf : circle_integrable f c R) :
theorem circle_integrable.out {E : Type u_1} [normed_group E] {f : → E} {c : } {R : } [normed_space E] (hf : circle_integrable f c R) :

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_group E] {f : → E} {c : } :
theorem circle_integrable_iff {E : Type u_1} [normed_group E] [normed_space E] {f : → E} {c : } (R : ) :
theorem continuous_on.circle_integrable' {E : Type u_1} [normed_group E] {f : → E} {c : } {R : } (hf : continuous_on f (metric.sphere c |R|)) :
theorem continuous_on.circle_integrable {E : Type u_1} [normed_group E] {f : → E} {c : } {R : } (hR : 0 R) (hf : continuous_on f (metric.sphere 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_group E] [normed_space E] [complete_space E] (f : → E) (c : ) (R : ) :
E

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

Equations
theorem circle_integral_def_Icc {E : Type u_1} [normed_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_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_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_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_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_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_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_group E] [normed_space E] [complete_space E] {f : → E} {c : } {R C : } (hR : 0 R) (hf : ∀ (z : ), z metric.sphere c Rf 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_group E] [normed_space E] [complete_space E] {f : → E} {c : } {R C : } (hR : 0 R) (hf : ∀ (z : ), z metric.sphere c Rf 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_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 Rf 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_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_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_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_group E] [normed_space E] [complete_space E] {f f' : → E} {c : } {R : } (hR : 0 R) (h : ∀ (z : ), z metric.sphere c Rhas_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_group E] [normed_space E] [complete_space E] (f : → E) (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. For any circle integrable function f, this power series converges to the Cauchy integral for f.

Equations
theorem cauchy_power_series_apply {E : Type u_1} [normed_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_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_group E] [normed_space E] [complete_space E] (f : → E) (c : ) (R : nnreal) :
theorem has_sum_two_pi_I_cauchy_power_series_integral {E : Type u_1} [normed_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_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_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_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|