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 $\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

circleMap, a parametrization of a circle #

def circleMap (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
Instances For

    circleMap is -periodic.

    theorem Set.Countable.preimage_circleMap {s : Set } (hs : s.Countable) (c : ) {R : } (hR : R 0) :
    (circleMap c R ⁻¹' s).Countable
    @[simp]
    theorem circleMap_sub_center (c : ) (R : ) (θ : ) :
    circleMap c R θ - c = circleMap 0 R θ
    theorem circleMap_zero (R : ) (θ : ) :
    circleMap 0 R θ = R * Complex.exp (θ * Complex.I)
    @[simp]
    theorem abs_circleMap_zero (R : ) (θ : ) :
    Complex.abs (circleMap 0 R θ) = |R|
    theorem circleMap_mem_sphere' (c : ) (R : ) (θ : ) :
    theorem circleMap_mem_sphere (c : ) {R : } (hR : 0 R) (θ : ) :
    theorem circleMap_mem_closedBall (c : ) {R : } (hR : 0 R) (θ : ) :
    theorem circleMap_not_mem_ball (c : ) (R : ) (θ : ) :
    circleMap c R θMetric.ball c R
    theorem circleMap_ne_mem_ball {c : } {R : } {w : } (hw : w Metric.ball c R) (θ : ) :
    circleMap c R θ w
    @[simp]
    theorem range_circleMap (c : ) (R : ) :

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

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

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

    @[simp]
    theorem circleMap_eq_center_iff {c : } {R : } {θ : } :
    circleMap c R θ = c R = 0
    theorem circleMap_ne_center {c : } {R : } (hR : R 0) {θ : } :
    circleMap c R θ c
    theorem hasDerivAt_circleMap (c : ) (R : ) (θ : ) :
    @[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 lipschitzWith_circleMap (c : ) (R : ) :
    LipschitzWith (Real.nnabs R) (circleMap c R)
    theorem continuous_circleMap_inv {R : } {z : } {w : } (hw : w Metric.ball z R) :
    Continuous fun (θ : ) => (circleMap z R θ - w)⁻¹

    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
    Instances For
      @[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 : E} {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_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {c : } (R : ) :
      CircleIntegrable f c R IntervalIntegrable (fun (θ : ) => deriv (circleMap c R) θ f (circleMap c R θ)) MeasureTheory.volume 0 (2 * Real.pi)
      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 $\oint_{|z-c|=R} f(z)\,dz$.

      Equations
      Instances For

        Pretty printer defined by notation3 command.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            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 : E} {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.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_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {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 : E} {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 : E} {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 $\frac{1}{2πi}\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 ∘ 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
            Instances For
              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 : ) :
              cauchyPowerSeries f c R n ((2 * Real.pi)⁻¹ * ∫ (θ : ) in 0 ..2 * Real.pi, f (circleMap c R θ)) * |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 : Complex.abs 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 : Complex.abs 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 : Complex.abs 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 $\oint_{|z-c|=R} \frac{dz}{z-w} = 2πi$ whenever $|w-c| < R$.