Area inside a curve

Stream: Is there code for X?

[Geoffrey Irving]

I'm trying to prove the Koebe quarter theorem via the area theorem, and the main piece of machinery I need is expressing the area inside a (simple, analytic) curve in terms of a path integral along the curve. This is just a special case of Green's theorem, but I can't find Green's or Stokes' theorem.

Do we have these?

[Geoffrey Irving]

Actually I think I can get away with dealing purely in terms of (1) measurable sets and (2) the area within disks, since I can express the area in question as "very large disk \ nicely parameterized region" with an arbitrarily small error term.

[Junyan Xu]

Yury Kudryashov formalized the divergence/Green's theorem, but apparently only for rectangular boxes.
image.png

However, I think what you really need for the area theorem is Green's formula for the disk together with the change of variable formula for integrals, which has been formalized in great generality by Sébastien Gouëzel. If your analytic function is $f(z)=u(z)+iv(z)$, then the integration of $L\,dx+M\,dy$ along the image $f(\gamma)$ of the unit circle $\gamma$ is the same as the integral of $((L\circ f)u_x+(M\circ f)v_x)\,dx+((L\circ f)u_y+(M\circ f)v_y)\,dy$ along $\gamma$. In particular for computing the area within $f(\gamma)$ you'd take $L=0$ and $M=x$, and you get $uv_x\,dx+uv_y\,dy$, and Green's formula says its integral along $\gamma$ is the integral of $(g_x h_y - g_y h_x)\,dx\,dy$ on the unit disk, and the integrand is exactly the determinant of the Jacobian. And it's easy to prove Green's formula for the disk by hand (for the particular $e^{i\theta}$ parametrization that you need): apply Fubini to the two terms $\partial M/\partial x$ and $\partial L/\partial y$ in different order, use the fundamental theorem of calculus, and apply a (co)sine change of variable for interval integrals converting the interval [-1,1] to [0,π] and [π,2π], and you should be done. (This is basically the same as the first proof on Wikipedia for "simple regions".)