English
For any z,w ∈ ℂ and f: ℂ → E, the sum of the wedgeIntegral in both orders equals a combination of two horizontal and two vertical integrals along the sides of the rectangle determined by z and w.
Русский
Для любых z, w ∈ ℂ и f: ℂ → E сумма wedgeIntegral в двух направлениях равна комбинации горизонтальных и вертикальных интегралов по сторонам прямоугольника, заданного z и w.
LaTeX
$$$$z.wedgeIntegral(w,f) + w.wedgeIntegral(z,f) = \\left(\\int_{z.re}^{w.re} f(x+z.im\,i)\\,dx\\right) - \\left(\\int_{z.re}^{w.re} f(x+w.im\,i)\\,dx\\right) + i\\Big(\\int_{z.im}^{w.im} f(w.re+y\,i)\\,dy - \\int_{z.im}^{w.im} f(z.re+y\,i)\\,dy\\Big).$$$$
Lean4
theorem wedgeIntegral_add_wedgeIntegral_eq (z w : ℂ) (f : ℂ → E) :
wedgeIntegral z w f + wedgeIntegral w z f =
(∫ 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 (w.re + y * I)) -
I • (∫ y : ℝ in z.im..w.im, f (z.re + y * I)) :=
by
simp only [wedgeIntegral, intervalIntegral.integral_symm z.re w.re, intervalIntegral.integral_symm z.im w.im,
smul_neg]
abel
