English
Define a wedge-type line integral of a function f: ℂ → E along a rectangular path determined by two complex points z and w, splitting the rectangle into horizontal and vertical sides.
Русский
Определим интеграл-ромб вдоль уголка функции f: ℂ → E вдоль прямоугольной траектории, задаваемой двумя точками z и w, разбивая прямоугольник на горизонтальные и вертикальные стороны.
LaTeX
$$$\\text{wedgeIntegral}(z,w,f) = \\int_{x=z.re}^{w.re} f(x+i z.im) \\, dx \\, + i \\cdot \\int_{y=z.im}^{w.im} f(w.re + i y) \\, dy.$$$
Lean4
/-- The `(z, w)`-wedge-integral of `f`, is the integral of `f` over two sides of the rectangle
determined by `z` and `w`. -/
def wedgeIntegral (z w : ℂ) (f : ℂ → E) : E :=
(∫ x : ℝ in z.re..w.re, f (x + z.im * I)) + I • (∫ y : ℝ in z.im..w.im, f (w.re + y * I))
