integral_undef — Mathlib

English

If f' is a derivative within the circle of a complex-differentiable function on the circle, then the circle integral of f' over the circle is zero.

Русский

Если f' является производной внутри круга функции комплексной переменной на окружности, то круговой интеграл f' по окружности равен нулю.

LaTeX

$$$\\forall f,f',\\; (\\forall z\\in sphere c|R|, HasDerivWithinAt f (f' z) (sphere c|R|) z) \\Rightarrow (\\oint z in C(c,R), f'(z)) = 0$$$

Lean4

theorem integral_undef {f : ℂ → E} {c : ℂ} {R : ℝ} (hf : ¬CircleIntegrable f c R) : (∮ z in C(c, R), f z) = 0 :=
  intervalIntegral.integral_undef (mt (circleIntegrable_iff R).mpr hf)

Похожие утверждения