isExactOn_ball — Mathlib

English

If a differentiable function on a disk is conservative, then it has a primitive on that disk.

Русский

Если функция на диске является консервативной, то на диске она имеет примитив.

LaTeX

$$$\\text{If } f \\text{ is differentiable on } \\mathrm{ball}(c,r) \\text{ then } IsExactOn(f, \\mathrm{ball}(c,r)).$$$

Lean4

/-- **Morera's theorem for a disk** On a disk, a continuous function whose integrals on rectangles
  vanish, has primitives. -/
theorem isExactOn_ball (hf' : ContinuousOn f (ball c r)) (hf : IsConservativeOn f (ball c r)) :
    IsExactOn f (ball c r) :=
  ⟨fun z ↦ wedgeIntegral c z f, fun _ ↦ hf.hasDerivAt_wedgeIntegral hf'⟩

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