Documentation

Mathlib.MeasureTheory.Integral.CircleIntegral

Integral over a circle in #

In this file we define ∮ z in C(c, R), f z to be the integral |zc|=|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

Facts about circleMap #

@[simp]
theorem range_circleMap (c : ) (R : ) :

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

@[simp]

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

theorem hasDerivAt_circleMap (c : ) (R θ : ) :

The circleMap is real analytic.

theorem contDiff_circleMap (c : ) (R : ) {n : WithTop ℕ∞} :

The circleMap is continuously differentiable.

@[simp]
theorem deriv_circleMap (c : ) (R θ : ) :
theorem deriv_circleMap_eq_zero_iff {c : } {R θ : } :
deriv (circleMap c R) θ = 0 R = 0
theorem deriv_circleMap_ne_zero {c : } {R θ : } (hR : R 0) :
deriv (circleMap c R) θ 0
theorem continuous_circleMap_inv {R : } {z w : } (hw : w Metric.ball z R) :
Continuous fun (θ : ) => (circleMap z R θ - w)⁻¹
theorem circleMap_neg_radius {r x : } {c : } :
circleMap c (-r) x = circleMap c r (x + Real.pi)

Integrability of a function on a circle #

def CircleIntegrable {E : Type u_1} [NormedAddCommGroup E] (f : E) (c : ) (R : ) :

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

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

Equations
@[simp]
theorem circleIntegrable_const {E : Type u_1} [NormedAddCommGroup E] (a : E) (c : ) (R : ) :
CircleIntegrable (fun (x : ) => a) c R
theorem CircleIntegrable.add {E : Type u_1} [NormedAddCommGroup E] {f g : E} {c : } {R : } (hf : CircleIntegrable f c R) (hg : CircleIntegrable g c R) :
theorem CircleIntegrable.neg {E : Type u_1} [NormedAddCommGroup E] {f : E} {c : } {R : } (hf : CircleIntegrable f c R) :
theorem CircleIntegrable.out {E : Type u_1} [NormedAddCommGroup E] {f : E} {c : } {R : } [NormedSpace E] (hf : CircleIntegrable f c R) :
IntervalIntegrable (fun (θ : ) => deriv (circleMap c R) θ f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)

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

@[simp]
theorem circleIntegrable_zero_radius {E : Type u_1} [NormedAddCommGroup E] {f : E} {c : } :
theorem CircleIntegrable.congr_codiscreteWithin {c : } {R : } {f₁ f₂ : } (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hf₁ : CircleIntegrable f₁ c R) :

Circle integrability is invariant when functions change along discrete sets.

theorem circleIntegrable_congr_codiscreteWithin {c : } {R : } {f₁ f₂ : } (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) :

Circle integrability is invariant when functions change along discrete sets.

theorem circleIntegrable_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } (R : ) :
theorem ContinuousOn.circleIntegrable' {E : Type u_1} [NormedAddCommGroup E] {f : E} {c : } {R : } (hf : ContinuousOn f (Metric.sphere c |R|)) :
theorem ContinuousOn.circleIntegrable {E : Type u_1} [NormedAddCommGroup E] {f : E} {c : } {R : } (hR : 0 R) (hf : ContinuousOn f (Metric.sphere c R)) :
@[simp]
theorem circleIntegrable_sub_zpow_iff {c w : } {R : } {n : } :
CircleIntegrable (fun (z : ) => (z - w) ^ n) c R R = 0 0 n wMetric.sphere c |R|

The function fun 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 circleIntegrable_sub_inv_iff {c w : } {R : } :
CircleIntegrable (fun (z : ) => (z - w)⁻¹) c R R = 0 wMetric.sphere c |R|
def circleIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (c : ) (R : ) :
E

Definition for |zc|=Rf(z)dz

Equations

∮ z in C(c, R), f z is the circle integral |zc|=Rf(z)dz.

Equations
  • One or more equations did not get rendered due to their size.

Pretty printer defined by notation3 command.

Equations
  • One or more equations did not get rendered due to their size.
theorem circleIntegral_def_Icc {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (c : ) (R : ) :
( (z : ) in C(c, R), f z) = (θ : ) in Set.Icc 0 (2 * Real.pi), deriv (circleMap c R) θ f (circleMap c R θ)
@[simp]
theorem circleIntegral.integral_radius_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (c : ) :
( (z : ) in C(c, 0), f z) = 0
theorem circleIntegral.integral_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f g : E} {c : } {R : } (hR : 0 R) (h : Set.EqOn f g (Metric.sphere c R)) :
( (z : ) in C(c, R), f z) = (z : ) in C(c, R), g z
theorem circleIntegral.circleIntegral_congr_codiscreteWithin {c : } {R : } {f₁ f₂ : } (hf : f₁ =ᶠ[Filter.codiscreteWithin (Metric.sphere c |R|)] f₂) (hR : R 0) :
( (z : ) in C(c, R), f₁ z) = (z : ) in C(c, R), f₂ z

Circle integrals are invariant when functions change along discrete sets.

theorem circleIntegral.integral_sub_inv_smul_sub_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 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 circleIntegral.integral_undef {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R : } (hf : ¬CircleIntegrable f c R) :
( (z : ) in C(c, R), f z) = 0
theorem circleIntegral.integral_add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f g : E} {c : } {R : } (hf : CircleIntegrable f c R) (hg : CircleIntegrable 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 circleIntegral.integral_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f g : E} {c : } {R : } (hf : CircleIntegrable f c R) (hg : CircleIntegrable 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 circleIntegral.norm_integral_le_of_norm_le_const' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R C : } (hf : zMetric.sphere c |R|, f z C) :
(z : ) in C(c, R), f z 2 * Real.pi * |R| * C
theorem circleIntegral.norm_integral_le_of_norm_le_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R C : } (hR : 0 R) (hf : zMetric.sphere c R, f z C) :
(z : ) in C(c, R), f z 2 * Real.pi * R * C
theorem circleIntegral.norm_two_pi_i_inv_smul_integral_le_of_norm_le_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R C : } (hR : 0 R) (hf : zMetric.sphere c R, f z C) :
(2 * Real.pi * Complex.I)⁻¹ (z : ) in C(c, R), f z R * C
theorem circleIntegral.norm_integral_lt_of_norm_le_const_of_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R C : } (hR : 0 < R) (hc : ContinuousOn f (Metric.sphere c R)) (hf : zMetric.sphere c R, f z C) (hlt : zMetric.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 circleIntegral.integral_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {𝕜 : Type u_2} [RCLike 𝕜] [NormedSpace 𝕜 E] [SMulCommClass 𝕜 E] (a : 𝕜) (f : E) (c : ) (R : ) :
( (z : ) in C(c, R), a f z) = a (z : ) in C(c, R), f z
@[simp]
theorem circleIntegral.integral_smul_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] (f : ) (a : E) (c : ) (R : ) :
( (z : ) in C(c, R), f z a) = ( (z : ) in C(c, R), f z) a
@[simp]
theorem circleIntegral.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 circleIntegral.integral_sub_center_inv (c : ) {R : } (hR : R 0) :
( (z : ) in C(c, R), (z - c)⁻¹) = 2 * Real.pi * Complex.I
theorem circleIntegral.integral_eq_zero_of_hasDerivWithinAt' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f f' : E} {c : } {R : } (h : zMetric.sphere c |R|, HasDerivWithinAt 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 circleIntegral.integral_eq_zero_of_hasDerivWithinAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] [CompleteSpace E] {f f' : E} {c : } {R : } (hR : 0 R) (h : zMetric.sphere c R, HasDerivWithinAt 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 circleIntegral.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 circleIntegral.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.

The power series that is equal to 12πin=0|zc|=R(wczc)n1zcf(z)dz at w - c. The coefficients of this power series depend only on f ∘ circleMap c R, and the power series converges to f w if f is differentiable on the closed ball Metric.closedBall 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 cauchyPowerSeries_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (c : ) (R : ) (n : ) (w : ) :
((cauchyPowerSeries f c R n) fun (x : Fin n) => w) = (2 * Real.pi * Complex.I)⁻¹ (z : ) in C(c, R), (w / (z - c)) ^ n (z - c)⁻¹ f z
theorem norm_cauchyPowerSeries_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (c : ) (R : ) (n : ) :
theorem le_radius_cauchyPowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] (f : E) (c : ) (R : NNReal) :
R (cauchyPowerSeries f c R).radius
theorem hasSum_two_pi_I_cauchyPowerSeries_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R : } {w : } (hf : CircleIntegrable f c R) (hw : w < R) :
HasSum (fun (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 cauchyPowerSeries 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 hasSum_cauchyPowerSeries_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R : } {w : } (hf : CircleIntegrable f c R) (hw : w < R) :
HasSum (fun (n : ) => (cauchyPowerSeries f c R n) fun (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 cauchyPowerSeries 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_cauchyPowerSeries_eq_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R : } {w : } (hf : CircleIntegrable f c R) (hw : w < R) :
(cauchyPowerSeries 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 cauchyPowerSeries 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 hasFPowerSeriesOn_cauchy_integral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } {R : NNReal} (hf : CircleIntegrable f c R) (hR : 0 < R) :
HasFPowerSeriesOnBall (fun (w : ) => (2 * Real.pi * Complex.I)⁻¹ (z : ) in C(c, R), (z - w)⁻¹ f z) (cauchyPowerSeries f c R) c R

For any circle integrable function f, the power series cauchyPowerSeries 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 circleIntegral.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 |zc|=Rdzzw=2πi whenever |wc|<R.