Theorems · Theorem · complex analysis

Complex.integral_boundary_rect_of_differentiableOn_real

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ),
  DifferentiableOn ℝ f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
    MeasureTheory.IntegrableOn (fun z => Complex.I • (fderiv ℝ f z) 1 - (fderiv ℝ f z) Complex.I)
        (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume →
      (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
            Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
          Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
        ∫ (x : ℝ) in z.re..w.re,
          ∫ (y : ℝ) in z.im..w.im,
            Complex.I • (fderiv ℝ f (↑x + ↑y * Complex.I)) 1 - (fderiv ℝ f (↑x + ↑y * Complex.I)) Complex.I

Suppose that a function f : ℂ → E is real differentiable on a closed rectangle with opposite corners at z w : ℂ and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the integral of f over the boundary of the rectangle is equal to the integral of $2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$ over the rectangle.

Defined in

Mathlib.Analysis.Complex.CauchyIntegral

Cited by

0 results in Mathlib

Foundations

Depth 268 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace