English
If f is continuous on a closed rectangle, differentiable almost everywhere in the interior, and ∂f/∂\\bar z is integrable, then the boundary integral equals the double integral of the corresponding derivative term.
Русский
Если f непрерывна на замкнутом прямоугольнике, дифференцируема почти повсюду внутри, и ∂f/∂\\bar z интегрируема, то контурный интеграл по границе равен двойному интегралу от соответствующего производного терма.
LaTeX
$$\\oint_{\\partial R} f(z) \\, dz = \\iint_R (i f_x - f_y) \\, dx dy$$
Lean4
/-- 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. -/
theorem integral_boundary_rect_of_continuousOn_of_hasFDerivAt_real (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ)
(Hc : ContinuousOn f ([[z.re, w.re]] ×ℂ [[z.im, w.im]]))
(Hd : ∀ x ∈ Ioo (min z.re w.re) (max z.re w.re) ×ℂ Ioo (min z.im w.im) (max z.im w.im), HasFDerivAt f (f' x) x)
(Hi : IntegrableOn (fun z => I • f' z 1 - f' z I) ([[z.re, w.re]] ×ℂ [[z.im, w.im]])) :
(∫ x : ℝ in z.re..w.re, f (x + z.im * I)) - (∫ x : ℝ in z.re..w.re, f (x + w.im * I)) +
I • (∫ y : ℝ in z.im..w.im, f (re w + y * I)) -
I • (∫ y : ℝ in z.im..w.im, f (re z + y * I)) =
∫ x : ℝ in z.re..w.re, ∫ y : ℝ in z.im..w.im, I • f' (x + y * I) 1 - f' (x + y * I) I :=
integral_boundary_rect_of_hasFDerivAt_real_off_countable f f' z w ∅ countable_empty Hc (fun x hx => Hd x hx.1) Hi
