English
On a disk, a continuous function with zero wedge integrals over all rectangles has a primitive; equivalently, it is analytic on the disk.
Русский
На диске непрерывная функция с нулевыми в интегралах по всем прямоугольникам имеет примитив, то есть аналитна на диске.
LaTeX
$$$\\text{If } f \\text{ is continuous on } B(c,r) \\text{ and } IsConservativeOn(f, B(c,r)), \\text{ then } f \\text{ is exact on } B(c,r).$$$
Lean4
/-- The `wedgeIntegral` has derivative at `z` equal to `f z`. -/
theorem hasDerivAt_wedgeIntegral (h : IsConservativeOn f (ball c r)) :
HasDerivAt (fun w ↦ wedgeIntegral c w f) (f z) z :=
by
rw [hasDerivAt_iff_isLittleO]
calc
_ =ᶠ[𝓝 z] (fun w ↦ wedgeIntegral z w f - (w - z) • f z) := ?_
_ =
(fun w ↦ (∫ x in z.re..w.re, f (x + z.im * I)) - (w - z).re • f z) +
I • (fun w ↦ (∫ y in z.im..w.im, f (w.re + y * I)) - (w - z).im • f z) :=
?_
_ =o[𝓝 z] fun w ↦ w - z :=
(hasDerivAt_wedgeIntegral_re_aux f_cont hz).add ((hasDerivAt_wedgeIntegral_im_aux f_cont hz).const_smul_left I)
· exact (h.eventually_nhds_wedgeIntegral_sub_wedgeIntegral f_cont hz).mono <| by simp
ext w
set I₁ := ∫ x in z.re..w.re, f (x + z.im * I)
set I₂ := ∫ y in z.im..w.im, f (w.re + y * I)
calc
_ = I₁ + I • I₂ - ((w - z).re + (w - z).im * I) • f z := by congr; rw [re_add_im]
_ = I₁ + I • I₂ - ((w.re - z.re : ℂ) + (w.im - z.im) * I) • f z := by simp
_ = I₁ - (w.re - z.re : ℂ) • f z + I • (I₂ - (w.im - z.im : ℂ) • f z) := ?_
· rw [add_smul, smul_sub, smul_smul, mul_comm I]; abel
· congr <;> simp
