Theorems · Theorem · complex analysis

Complex.integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ),
  ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
    (∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im), HasFDerivAt f (f' x) x) →
      MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (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 • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I

Suppose that a function f : ℂ → E is continuous on a closed rectangle with opposite corners at z w : ℂ, is real differentiable on the corresponding open rectangle, 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