English
For a rectangle, the contour integral of a function differentiable on the rectangle is zero.
Русский
Для прямоугольника контура интеграла функции, дифференцируемой на прямоугольнике, равен нулю.
LaTeX
$$∮_{\\partial R} f = 0$$
Lean4
/-- **Cauchy-Goursat theorem** for a rectangle: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if `f` is complex differentiable on a
closed rectangle, then its integral over the boundary of the rectangle equals zero. -/
theorem integral_boundary_rect_eq_zero_of_differentiableOn (f : ℂ → E) (z w : ℂ)
(H : DifferentiableOn ℂ f ([[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)) =
0 :=
integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn f z w H.continuousOn <|
H.mono <| inter_subset_inter (preimage_mono Ioo_subset_Icc_self) (preimage_mono Ioo_subset_Icc_self)
