divthm.tex

\documentclass[a4paper, UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}

\bibliographystyle{plainurl}% the mandatory bibstyle

\author{Yury Kudryashov}{University of Toronto at Mississauga, Canada (till July 2022); Texas A\&M University, USA (since August 2022)}{urkud@urkud.name}{https://orcid.org/0000-0003-4286-9276}{}
% TODO mandatory, please use full name; only 1 author per \author macro; first two parameters are mandatory, other parameters can be empty. Please provide at least the name of the affiliation and the country. The full address is optional. Use additional curly braces to indicate the correct name splitting when the last name consists of multiple name parts.

\authorrunning{Yu. Kudryashov} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'

\Copyright{Yury Kudryashov} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/

\ccsdesc[500]{Mathematics of computing~Integral calculus}
\ccsdesc[500]{Security and privacy~Logic and verification}

\keywords{divergence theorem, Green's theorem, Gauge integral, Cauchy integral formula, Cauchy-Goursat theorem, complex analysis} %TODO mandatory; please add comma-separated list of keywords

\category{} %optional, e.g. invited paper

\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
%\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional

% \supplement{TODO}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
\supplementdetails[linktext={Github wiki page}]{Documentation website}{https://github.com/leanprover-community/mathlib/wiki/Project:-formalization-of-the-divergence-theorem} %linktext, cite, and subcategory are optional

%\funding{(Optional) general funding statement \dots}%optional, to capture a funding statement, which applies to all authors. Please enter author specific funding statements as fifth argument of the \author macro.

\acknowledgements{I want to thank Patrick Massot for bringing up an
  idea of formalizing a sufficiently general version of the divergence
  theorem, Sébastien Gouëzel for fruitful discussions and peer review
  of most of the code, and my wife Nataliya Goncharuk for constant
  support. I also want to thank Anne Baanen, Johan Commelin, Nataliya
  Goncharuk, and Robert Y. Lewis for valuable comments on the draft
  versions of this paper and I thank my son Konstantin for finding
  lots of typos. I am also grateful to the anonymous referees for
  their valuable comments.}%optional

% \nolinenumbers %uncomment to disable line numbering

\usepackage{csquotes,braket,upgreek,MnSymbol}

\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
\definecolor{errorcolor}{rgb}{1, 0, 0}           % bright red
\definecolor{stringcolor}{rgb}{0.5, 0.3, 0.2}    % brown
\usepackage{listings}
\def\lstlanguagefiles{lstlean.tex}
\lstset{language=lean}

\newcommand{\bbR}{\mathbb{R}}
\newcommand{\bbC}{\mathbb{C}}
\newcommand{\bbN}{\mathbb{N}}
\newcommand{\eps}{\varepsilon}
\DeclareMathOperator{\divg}{div}
\DeclareMathOperator{\const}{const}
\undef\Re\DeclareMathOperator{\Re}{Re}
\undef\Im\DeclareMathOperator{\Im}{Im}

\AtBeginDocument{%
\def\sectionautorefname{Sec.}
\def\subsectionautorefname{Sec.}
\def\subsubsectionautorefname{Sec.}}

\title{Formalizing the divergence theorem and the Cauchy integral formula in Lean}

\newcommand{\mathlibref}[2]{\href{https://leanprover-community.github.io/mathlib_docs/find/#1}{#2}}

%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\EventEditors{June Andronick and Leonardo de Moura}
\EventNoEds{2}
\EventLongTitle{13th International Conference on Interactive Theorem Proving (ITP 2022)}
\EventShortTitle{ITP 2022}
\EventAcronym{ITP}
\EventYear{2022}
\EventDate{August 7--10, 2022}
\EventLocation{Haifa, Israel}
\EventLogo{}
\SeriesVolume{237}
\ArticleNo{31}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\maketitle
\sloppy

\begin{abstract}
  I formalize a version of the divergence theorem for a function on a
  rectangular box that does not assume regularity of individual
  partial derivatives, only Fréchet differentiability of the vector
  field and integrability of its divergence. Then I use this theorem
  to prove the Cauchy-Goursat theorem (for some simple domains) and
  bootstrap complex analysis in the Lean mathematical library. The
  main tool is the GP-integral, a version of the Henstock-Kurzweil
  integral introduced by J. Mawhin in 1981. The divergence theorem for
  this integral does not require integrability of the divergence.
\end{abstract}

\section{Introduction}\label{sec:introduction}
The divergence theorem says that, under certain assumptions, the
integral of the divergence of a vector field over a region is equal to
the flow of this vector field through the boundary of the region. For
a rectangular region on the plane, this can be written as
\begin{multline}
  \label{eqn:green-rect}
  \int_{a}^{b}\int_{c}^{d}\left(\frac{\partial f(x, y)}{\partial x}+\frac{\partial g(x, y)}{\partial y}\right)dydx=\\
  \int_{a}^{b}\left(g(x, d)-g(x, c)\right)dx+\int_{c}^{d}\left(f(b, y)-f(a, y)\right)dy,
\end{multline}
where \(f, g\colon \bbR^{2}\to E\) are functions from the plane to
some Banach space. This statement is also known as Green's theorem.
For continuously differentiable functions \(f\), \(g\), the equality
immediately follows from the Fundamental Theorem of Calculus and the
Fubini Theorem.

If \(F\colon \bbC\to E\) is a complex differentiable function, then, due
to Cauchy-Riemann relations, the left-hand side of Green's theorem
applied to \(f(x, y)=F(x+iy)\) and \(g(x, y)=iF(x+iy)\) is zero, and
we get
\href{https://en.wikipedia.org/wiki/Cauchy's_integral_theorem}{Cauchy's
  integral theorem} (a.k.a. the Cauchy-Goursat theorem) for a rectangle.

There is a gap in the proof outlined above: I explained how to prove
Green's formula for a \emph{continuously differentiable} function
but the Cauchy-Goursat theorem works for any \emph{complex
  differentiable} function. A common misbelief is that this makes
Green's formula (and divergence theorem) unusable for the Cauchy-Goursat
theorem, and one has to prove it using an explicit infinite descent.

The goal of this project is to formulate a version of the divergence
theorem that implies the Cauchy-Goursat theorem without any
assumptions on the derivative of a complex differentiable function. It
was originally inspired by a version of the divergence theorem by
F.~Acker~\cite{Acker1996} that works for a vector field with
\emph{continuous divergence}, though the actual proof I formalized is
very different.

Here is the list of most important definitions and theorems I
formalize in this project.
\begin{itemize}
\item Riemann, McShane, Henstock-Kurzweil, and GP-integrals of a
  function from a box in \(\bbR^{n}\) to a real Banach space, see
  \cref{sec:henst-kurzw-informal,sec:GP-impl};
\item the divergence theorem for the GP-integral, see
  \cref{thm:divergence,lst:divergence-GP};
\item the divergence theorem for the Bochner integral, see
  \cref{thm:divergence-Bochner,lst:divergence-bochner}; the Bochner
  integral is a generalization of the Lebesgue integral to functions
  that take values in Banach spaces, see \autoref{ssec:Bochner} for
  more details;
\item the Cauchy-Goursat theorem for rectangles, annuli, and disks,
  see \cref{lst:cauchy-rect,lst:cauchy-annulus,lst:cauchy-circle};
\item the Cauchy integral formula for a disk, see \cref{lst:cauchy-int};
\item analyticity of a complex differentiable function, see
  \cref{lst:diff-analytic};
\item the Riemann removable singularity theorem.
\end{itemize}

Most of these theorems were formalized earlier in other theorem
provers. However, this is the first project where the divergence
theorem was formalized in this generality. In particular, the
Cauchy-Goursat theorem becomes a simple corollary of the general
divergence theorem. Also, the assumptions in the Cauchy-Goursat
theorem are slightly weaker than in most textbooks.

The most similar other project is Abdulaziz and Paulson's
formalization of Green's theorem for a large class of domains in
\(\bbR^{2}\) in Isabelle~\cite{Abdulaziz_Paulson}. Neither Isabelle
nor my version of the divergence theorem implies the other. Here are
the key points where one of the formalizations is more general than
the other, see also \autoref{sec:gener-diverg-theor}.

\begin{description}
\item[shape of the domain] The Isabelle formalization works with any
  elementary region while my formalization only works for a
  rectangular box;
\item[differentiability] The Isabelle formalization only requires
  existence of the partial derivatives while I require Fréchet
  differentiability of the original function;
\item[regularity of the derivative] The Isabelle formalization
  requires integrability of each partial derivative while my
  formalization makes no regularity assumptions for the GP-integral
  and assumes only integrability of the divergence for the
  Henstock-Kurzweil and Bochner integrals; this makes it possible
  deduce the Cauchy-Goursat theorem from my version of the divergence
  theorem;
\item[domain dimension] The Isabelle formalization only deals with
  dimension two while I formalize the divergence theorem in any finite
  dimension; this generalization is needed throughout differential
  topology, PDE theory and mathematical physics;
\item[codomain dimension] The Isabelle formalization only works for
  finite dimensional codomain while my formalization works for any
  Banach space; this is needed, for example, in spectral theory for
  the resolvent.
\end{description}

The complex analysis part of the project does not try to compete with
the state of the art complex analysis libraries in
Mizar~\cite{harrison-mizar} and Isabelle/HOL~\cite{harrison-hol}, both
originally written by J.~Harrison, and is provided mostly as a proof
of concept (and the begining of a new project).

All these theorems are already in the \texttt{master} branch of the
Lean~\cite{10.1007/978-3-319-21401-6_26} mathematical library
\texttt{mathlib}~\cite{mathlib20}. For presentational purposes, I
changed some names (the \texttt{mathlib} naming convention sometimes
leads to very long names) and notation in the code listings below.

As in most parts of \texttt{mathlib} (and all of its analysis
library), I do not avoid the axiom of choice.

\subsection{Structure of the paper}%
\label{sec:structure-paper}

In \autoref{sec:gener-diverg-theor} I informally discuss different
ways to generalize the divergence theorem mentioned above, including
comparison with the formalization in Isabelle. Then in
\autoref{sec:henst-kurzw-informal} I give various definitions related
to the Henstock-Kurzweil, McShane, and GP-integrals and formulate the
divergence theorem for the GP-integral. In \autoref{sec:GP-impl} I
discuss some design choices I made in this project. Finally, in
\autoref{sec:appl-compl-analys} I explain how to apply this theorem to
prove the Cauchy-Goursat theorem and some other basic theorems from
complex analysis. \autoref{sec:future-plans} is devoted to my future
plans.

\section{Generalizations of the divergence theorem}%
\label{sec:gener-diverg-theor}

The divergence theorem for continuously differentiable vector fields
on rectangular boxes can be generalized in a few different directions,
leading to several theorems, none of which implies the others.

\subsection{Shape of the domain}
One natural direction of generalization is to deal with
non-rectangular domains. This generalization is done by Abdulaziz and
Paulson in Isabelle~\cite{Abdulaziz_Paulson} for regions that can be
divided both into type I regions by vertical lines only and into type
II regions by horizontal lines only. I only deal with rectangular
boxes, so I am not going to discuss this in any more details.

% https://www.cl.cam.ac.uk/~lp15/papers/Formath/Greens-theorem.pdf

\subsection{More general codomain}
Another possible direction of generalization is to deal with functions
\(f\colon \bbR^{n}\to E^{n}\), where \(E\) is a real Banach space,
instead of vector fields \(v\colon \bbR^{n}\to\bbR^{n}\) and \(E^{n}\)
is the direct sum of \(n\) copies of \(E\). Most proofs that work for
a vector field can be generalized to this case with no or little
modifications. I deal with functions \(\bbR^{n}\to E^{n}\) right away.

\subsection{Integrable partial derivatives}
It is easy to see that the standard proof based on Fubini's theorem
and FTC works for a function \(f\colon \bbR^{n}\to E^{n}\) such that
the partial derivatives \(\frac{\partial f^{i}(x)}{\partial x^{i}}\)
exist at all points of the box and are integrable on the whole
box.

\begin{remark}
  Here and below I use upper indices for coordinates of vectors to
  disambiguate \(i\)-th coordinate of a vector from \(i\)-th element
  in a sequence of vectors. I \textsw{do not assume} implicit
  summation over indices that appear both as an upper and as a lower
  index.
\end{remark}

Neither this generalization nor the next one imply each other. I
formalized the other one because it implies the Cauchy--Goursat theorem.

\subsection{Fréchet differentiability}
A function \(f\colon E_{1}\to E_{2}\) between normed vector spaces is
called \emph{Fréchet differentiable} at a point \(x\) with the
derivative given by a continuous linear map
\(f'\colon E_{1}\to E_{2}\) if \(f(x+y)=f(x)+f'(y)+o(y)\) as
\(y\to 0\). A Fréchet differentiable function \(f\) has all partial
derivatives and they are equal to the values of \(f'\) on the basis
vectors.

In 1981, Mawhin~\cite{Mawhin81} introduced a generalization of the
Henstock-Kurzweil integral he called the \emph{GP-integral} (probably
from \emph{generalized Perron}). This integral allows us to prove the
following theorem.

\begin{theorem}%
  [see~\cite{Mawhin81}]%
  \label{thm:divergence}
  Let \(E\) be a real Banach space. Let \(f\colon \bbR^{n}\to E\) be a
  function that is Fréchet differentiable at all points of a closed
  box \(\overline I=[a, b]\).

  Then for each \(i=1,\dots,n\), the partial derivative
  \(\frac{\partial f}{\partial x^{i}}\) is GP-integrable on \(I\) and
  its integral is equal to the difference of the integrals of \(f\) over
  the faces \(x^{i}=b^{i}\) and \(x^{i}=a^{i}\) of \(I\).

  In particular, for a function \(f\colon \bbR^{n}\to E^{n}\), the
  divergence
  \begin{equation}
    \label{eq:divg}
    \divg f=\sum_{i=1}^{n}\frac{\partial f^{i}}{\partial x^{i}}
  \end{equation}
  is GP-integrable on \(I\) and its integral is equal to the sum of
  integrals of \(f\) over the faces of \(I\) with appropriate signs.
\end{theorem}

Compared to the previous generalization, this one requires
differentiability in a stronger sense (Fréchet differentiability
instead of existence of one partial derivative) but it requires less
regularity from the derivatives (no requirements for the GP-integral
and integrability of the divergence instead of integrability of
partial derivatives for most other integrals).

\subsection{Weaker assumptions on a subset of the box}

One can push arguments in the proofs discussed above to weaken the
regularity assumptions on a “small” subset of the box.

I prove that \autoref{thm:divergence} works even if on some countable
subset of the box the function is continuous, not differentiable. It
is possible to push these arguments even further (especially if we use
another generalization of the Henstock-Kurzweil integral) but I did
not formalize these theorems (yet).

\section{Henstock-Kurzweil integral: informal description}\label{sec:henst-kurzw-informal}

While my main goal was to prove the divergence theorem for the Bochner
integral, I first proved the divergence theorem for the GP-integral,
see below. This integral is one of possible generalizations of the
Henstock-Kurzweil integral to higher dimension. In this section, I
state the relevant definitions and theorems.

\subsection{Henstock-Kurzweil integral in dimension one}\label{sec:HK-integral-dim1}
I start with the definition of the one-dimensional Henstock-Kurzweil
integral.

\begin{definition}%
  \label{def:Henstock}
  We say that a tagged partition \(a=x_{0}<x_{1}<\cdots<x_{k}=b\) with
  tags \(\xi_{i}\in[x_{i}, x_{i+1}]\), \(0\le i<k\), is
  \emph{subordinate} to a function \(\delta\colon[a, b]\to \bbR\) if
  \([x_{i}, x_{i+1}]\subset [\xi_{i}-\delta(\xi_{i}),
  \xi_{i}+\delta(\xi_{i})]\) for all \(0\le i<k\).

  We say that \(f\colon \bbR\to E\) has the Henstock-Kurzweil integral
  \(c\) over an interval \([a, b]\), \(\int_{a}^{b}f(x)\,dx=c\), if
  for any \(\eps>0\) there exists an everywhere positive function
  \(\delta\colon [a, b]\to \bbR\) such that for any tagged partition
  \((\set{x_{i}}, \set{\xi_{i}})\) subordinate to \(\delta\), the
  Riemann sum
  \(\displaystyle\sum_{i=0}^{k-1}f(\xi_{i})(x_{i+1}-x_{i}) \) is
  \(\eps\)-close to \(c\).
\end{definition}

Slight modifications of \autoref{def:Henstock} give the integrals of
Riemann (we require \(\delta\) to be a constant) and McShane (we no
longer require that tags belong to their intervals but still require
\(\xi_{i}\in[a, b]\)).

An equivalent (but more complicated) definition was given by A.~Denjoy
to integrate \(\frac{1}{x}\sin\left(\frac{1}{x^{3}}\right)\) over
\([-1, 1]\). This function is instegrable in the sense of the
Henstock-Kurzweil integral but it is not Lebesgue integrable.

A well-known property of the Henstock-Kurzweil integral is the
following form of the Fundamental Theorem of Calculus.
\begin{theorem}
  Let \(E\) be a real Banach space. Let \(f\colon \bbR\to E\) be a
  function differentiable on an interval \([a, b]\). Then its
  derivative is Henstock-Kurzweil integrable on \([a, b]\) and the
  integral is equal to \(f(b)-f(a)\).
\end{theorem}

The one-dimensional Henstock-Kurzweil integral is not a part of
\texttt{mathlib} and I decided not to formalize it. When we need it,
it will be easy to define it as a thin wrapper on top of the
Henstock-Kurzweil integral over a box in \lstinline+ℝ¹ = fin 1 → ℝ+.

\subsection{Henstock-Kurzweil integral in higher dimension}%
\label{sec:HK-integral-dim-n}

We will need a few definitions to generalize the Henstock-Kurzweil
integral to functions \(f\colon \bbR^{n}\to E\).

\begin{definition}%
  \label{def:box-partition}
  For \(a, b \in \bbR^{n}\), the \emph{open box} \((a, b)\) is the
  product of open intervals \((a^{i}, b^{i})\), that is
  \((a, b)=\set{x\in\bbR^{n}|\forall i, x^{i}\in(a^{i}, b^{i})}\). The
  \emph{open-closed box} \((a, b]\) and the \emph{closed box}
  \([a, b]\) are defined in a similar way.

  The \emph{distortion} (or \emph{irregularity}) \(\sigma(I)\) of an
  open-closed box \(I=(a, b]\) is the maximum of the ratios
  \(\frac{b^{i}-a^{i}}{b^{j}-a^{j}}\) over all \(i, j\).

  A \emph{partition} of an open-closed box \(I=(a, b]\) is a finite
  collection of pairwise disjoint boxes \(J_{k}=(a_{k}, b_{k}]\) that
  cover \(I\).

  A \emph{tagged partition} of an open-closed box \(I=(a, b]\) is a partition
  \(\set{J_{k}}\) together with a collection of points called
  \emph{tags} \(\xi_{k}\in [a, b]\), one per each box of the partition.

  A \emph{Henstock tagged partition} is a tagged partition such that
  each tag belongs to the corresponding closed box:
  \(\xi_{k}\in [c_{k}, d_{k}]\), where \(J_{k}=(c_{k}, d_{k}]\).

  A tagged partition \(\set{(J_{k}, \xi_{k})}\) of a box \(I\) is
  \emph{subordinate} to a \emph{gauge function}
  \(\delta\colon \bbR^{n}\to\bbR_{>0}\) if each box \(J_{k}\) is
  included by the closed box
  \(B_{\delta(\xi_{k})}(\xi_{k})=[\xi_{k}-\delta(\xi_{k}),
  \xi_{k}+\delta(\xi_{k})]\).
\end{definition}

Now we are ready to define the Henstock-Kurzweil integral of a
function \(f\colon \bbR^{n}\to E\) over a box \(I\).
\begin{definition}%
  \label{def:Henstock-dim-n}
  Let \(E\) be a real Banach space. We say that a function
  \(f\colon \bbR^{n}\to E\) is \emph{Henstock-Kurzweil integrable} on
  \(I\) with integral \(c\) if for any \(\eps>0\) there exists a gauge
  function \(\delta\colon \bbR^{n}\to \bbR_{>0}\) such that for any
  Henstock tagged partition \(\set{(J_{k}, \xi_{k})}\) of \(I\) that
  is subordinate to \(\delta\), the Riemann sum of \(f\) over this
  partition is \(\eps\)-close to \(c\).
\end{definition}

Similarly to the one-dimensional case, small modifications of
\autoref{def:Henstock-dim-n} provide definitions of Riemann and
McShane integrability, see the paragraph after \autoref{def:Henstock}.

Divergences of some vector fields are not integrable in the sense of
this definition (and any other generalization of the Henstock-Kurzweil
integral that satisfies Fubini's theorem, as shown by
W.~Pfeffer~\cite{Pfeffer93}), so we need another generalization to
prove the divergence theorem.

There are several generalizations of the Henstock-Kurzweil integral
such that the divergence of any Fréchet differentiable function is
integrable, see Bongiorno's survey~\cite{BONGIORNO2002587}.  I use the
one suggested by Mawhin~\cite{Mawhin81}.

\begin{definition}%
  \label{def:GP-integral}
  The \emph{distortion} (or \emph{irregularity}) \(\Sigma(\pi)\) of a
  partition \(\pi=\set{J_{k}}\) is the maximum of the distortions
  \(\sigma(J_{k})\) of the boxes \(J_{k}\).

  A function \(f\colon \bbR^{n}\to E\) is \emph{GP-integrable} on a
  box \(I\) with integral \(c\) if for any \(\eps>0\) and a real
  number \(d\) there exists a gauge function
  \(\delta\colon \bbR^{n}\to \bbR_{>0}\) such that for any Henstock
  tagged partition \(\set{(J_{k}, \xi_{k})}\) of \(I\) that is
  subordinate to \(\delta\) and has a distortion less than \(d\), the
  Riemann sum of \(f\) over this partition is \(\eps\)-close to \(c\).
\end{definition}

I formalized this definition (together with a few other definitions of
“box” integrals) and a proof of \autoref{thm:divergence}.

In dimension two, this theorem implies~\eqref{eqn:green-rect} for any
pair of functions \(f, g \colon \bbR^{2}\to E^{2}\) Fréchet
differentiable on a closed rectangle.

\subsection{Application to the Bochner integral}\label{ssec:Bochner}

The mathlib project uses the Bochner integral as its main
integral~\cite{vandoorn:LIPIcs.ITP.2021.18}. This integral is a
generalization of the Lebesgue integral. It was introduced by Bochner
in~\cite{Bochner1933IntegrationVF}, and it is also formalized in
Coq~\cite{boldo2022coq} and Isabelle~\cite{Avigad17}.

A~Bochner integrable function on a box in \(\bbR^{n}\) is McShane
integrable (hence Henstock-Kurzweil and GP-integrable), thus
\autoref{thm:divergence} holds for the Bochner integral if we assume
that the divergence is Bochner integrable on the box. Taking the limit
over an exhaustion of the box by smaller boxes, one can generalize the
theorem to functions that are differentiable in the interior of a box
and continuous on the whole box. Here is the precise statement of the
divergence theorem for Bochner integral.

\begin{theorem}%
  \label{thm:divergence-Bochner}
  Let \(E\) be a real Banach space. Let \(I=(a,b]\subset\bbR^{n}\) be
  an open-closed box. Let \(s \subset\bbR^{n}\) be a countable
  set. Let \(f\colon \bbR^{n}\to E^{n}\) be a function that is
  continuous on \(\overline I\) and is Fréchet differentiable at all
  points of \(\mathring I \setminus s\). Assume that the divergence
  \(\divg f\) defined by~\eqref{eq:divg} is Bochner integrable on
  \(I\). Then its integral is equal to the sum of integrals of \(f\)
  over the faces of \(\overline I\) taken with appropriate signs (plus
  for the integral over a front face \(x^{i}=b^{i}\) and minus for the
  integral over a back face \(x^{i}=a^{i}\)).
\end{theorem}

\section{Divergence theorem: design choices and implementation details}%
\label{sec:GP-impl}
The code below uses some notation that is specific either to
\texttt{mathlib} or this project.

\noindent
\begin{tabular}{rp{12cm}}
  \lstinline=Icc a b=& the closed interval \([a, b]\);\\
  \lstinline=Ioo a b=& the open interval \((a, b)\);\\
  \lstinline=Ioc a b=& the open-closed interval \((a, b]\);\\
  \lstinline=ICC a b=& the unordered closed interval \([\min(a, b), \max(a, b)]\);\\
  \lstinline=IOO a b=& the unordered open interval \((\min(a, b), \max(a, b))\);\\
  \lstinline=ℝⁿ=& the vector space \(\bbR^{n}\), implemented as \lstinline=fin n → ℝ=,
                  where \lstinline+fin n+ is the canonical type with \(n\) elements;\\
  \lstinline=Eⁿ=& the direct sum of \(n\) copies of a vector space \(E\), implemented as \lstinline=fin n → E=;
                  if \(E=\bbR\), then this notation agrees with the previous one;\\
  \lstinline=ℝ>0, ℝ≥0=& the types of positive and nonnegative real numbers, respectively;\\
  \lstinline=e i=& \(i\)-th basis vector in \(\bbR^{n}\);\\
  \lstinline=𝑖=& the imaginary unit;\\
  \lstinline=s ×ℂ t=& the product of sets on the real and imaginary axes in \(\bbC\).
\end{tabular}

\subsection{Boxes}\label{sec:boxes}

I use open-closed boxes in \(\bbR^{n}\), see \autoref{lst:box}, as
elements of partition because, this way, the boxes are disjoint as
sets and cover the whole ambient box, so one does not have to deal
with interiors or closures to define a partition.

\begin{lstlisting}[caption={Definition of a box}, label=lst:box]
structure box (n : ℕ) : Type :=
(lower upper : ℝⁿ)
(lower_lt_upper : ∀ i, lower i < upper i)
\end{lstlisting}

Each box can be interpreted as a set in \(\bbR^{n}\), see \autoref{lst:box-set}.
\begin{lstlisting}[caption={Box as a set}, label=lst:box-set]
instance : has_mem (ℝⁿ) (box n) :=
⟨λ x I, ∀ i, x i ∈ Ioc (I.lower i) (I.upper i)⟩

instance : has_coe_t (box n) (set ℝⁿ) := ⟨λ I, {x | x ∈ I}⟩
\end{lstlisting}
The order on the boxes is the inclusion order on the corresponding
sets.

I chose to explicitly deny empty boxes because this way the
\lstinline{lower} and \lstinline{upper} vertices are uniquely defined
by the set of points that belong to the box. The empty box is
represented as the bottom element \lstinline{⊥ : with_bot (box n)},
where \lstinline{with_bot α} is the type \lstinline={⊥} ∪ α=,
implemented as a type synonym for \lstinline{option α} with custom order.

From the order theory point of view, the type
\lstinline=with_bot (box n)= is a lattice, where the meet of two boxes
is their intersection and the join of two boxes is the minimal box
that includes both of them.

For an open-closed box \lstinline{I : box n}, \lstinline{I.Ioo} and
\lstinline{I.Icc} are the corresponding open and closed boxes,
respectively.

Given a box \lstinline=I : box (n + 1)= and an index
\lstinline=i : fin (n + 1)=, I define the \(i\)-th \emph{face} of
\(I\) to be the box in \(\bbR^{n}\) with lower and upper vertices given by
\lstinline=I.lower ∘ i.succ_above= and
\lstinline=I.upper ∘ i.succ_above=, where
\lstinline=i.succ_above : fin n → fin (n + 1)= is the unique monotone
embedding leaving a \enquote{hole} at \(i\): it sends \(j<i\) to \(j\)
and \(j\ge i\) to \(j+1\). I also define two embeddings
\lstinline=I.front_face i, I.back_face i : ℝⁿ → ℝⁿ⁺¹= that insert
\lstinline=I.upper i= and \lstinline=I.lower i=, respectively, as the
\(i\)-th coordinate. These embeddings map \lstinline=I.face i= to
the faces \lstinline+x i = I.upper i+ and \lstinline+x i = I.lower i+
of \(I\).

\subsection{Partitions}\label{sec:partitions}

A \emph{partition} of a box \(I\) is a finite collection of pairwise
disjoint boxes that cover \(I\). Sometimes, it is useful to deal with
a collection of pairwise disjoint boxes that cover only a part of
\(I\), so I define a \emph{prepartition} of a box and a predicate
saying that a prepartition is actually a partition, see
\autoref{lst:prepartition}.

I do not use two separate structures \lstinline=prepartition= and
\lstinline=partition= because with my approach I can define a function
of prepartitions (e.g., the Riemann integral sum), then prove
statements about its limits along various filters; some of these
filters require a prepartition to be a partition, some do not. Also, I
can define operations on prepartitions, then freely mix partitions and
prepartitions in the arguments instead of adding an explicit
\lstinline=to_prepartition= or an implicit coercion here and there.
On the other hand, I have to use
\lstinline=(π : prepartion I) (hπ : is_partition π)= instead of
\lstinline=(π : partition I)= whenever I want to argue about a
partition.

\begin{lstlisting}[caption={Definition of a (pre)partition}, label=lst:prepartition]
structure prepartition (I : box n) : Type :=
(boxes : finset (box n))
(le_of_mem' : ∀ J ∈ boxes, J ≤ I)
(pairwise_disjoint : pairwise boxes (disjoint on (coe : box n → set ℝⁿ)))

def is_partition (π : prepartition I) : Prop :=
∀ x ∈ I, ∃ J ∈ π, x ∈ J
\end{lstlisting}

Then I establish basic API about (pre)partitions, most notably the
following predicates, relations, and operations.

\noindent%
\begin{tabular}{rp{10cm}}
  \(\pi_{1}\le\pi_{2}\)&we say that one prepartition is less than or equal to another if each box of the former is included in some box of the latter; with this order, we get a bounded meet-semilattice structure on prepartitions of a box;\\
  \lstinline=Union=&the union of all boxes of a prepartition, as a set in \(\bbR^{n}\); for a partition, this union is equal to the original box;\\
  \lstinline=bUnion=&given a prepartition \(\pi\) of \(I\) and a function \(\pi'\) that sends each box in \(\bbR^{n}\) to a prepartition of that box, returns the prepartition of \(I\) formed by the boxes of \(\pi' J\), \(J \in \pi\);\\
  \lstinline=split_center=&the partition of a box into \(2^{n}\) subboxes by the coordinate hyperplanes passing through the center of the box;\\
  \lstinline=split=&the partition of a box into two subboxes by a coordinate hyperplane (or the trivial one-box partition if the hyperplane does not meet the box);\\
  \lstinline=split_many=&the partition of a box into subboxes by a finite set of coordinate hyperplanes;\\
  \lstinline=compl=&an unspecified prepartition such that \lstinline~π.compl.Union = I \ π.Union~; I prove that it exists, then use the axiom of choice to get a witness.
\end{tabular}

\subsection{Tagged partitions}%
\label{sec:tagged-partitions}

Recall that a \emph{tagged (pre)partition} is a (pre)partition~\(\pi\)
with a point (\enquote{tag}) chosen in each box of~\(\pi\). In the
formal definition, see \autoref{lst:tagged-partition}, I require that
the \lstinline=tag= function is defined on all boxes. This way I can
write \lstinline=π.tag J= without proving that \(J\) is one of the
boxes of \(\pi\).

\begin{lstlisting}[caption={Definition of a tagged (pre)partition}, label=lst:tagged-partition]
structure tagged_prepartition (I : box n) extends prepartition I :=
(tag : box n → ℝⁿ)
(tag_mem_Icc : ∀ J, tag J ∈ I.Icc)
\end{lstlisting}

Here the \lstinline=extends= keyword implicitly adds a field
\lstinline=to_prepartition= to the structure and introduces some
syntatic sugar for composed projections (e.g., given \lstinline=π= of
type \lstinline=tagged_prepartition I=, Lean unfolds
\lstinline=π.boxes= to \lstinline=π.to_prepartition.boxes=) and
constructors.

Unfortunately, similar syntax does not work for other definitions and
lemmas in the same namespace, so I have to repeat some definitions and
lemmas about prepartition once more (with one line proofs that
reference the corresponding lemma about prepartitions). I hope that
this tedious work will be automized in a future version of Lean or
mathlib.

There are a few new definitions about tagged prepartitions that
essentially use the tags, see \cref{def:box-partition,lst:Henstock}.

\begin{lstlisting}[caption={Henstock tagged (pre)partitions and (pre)partitions subordinate to a gauge function},label=lst:Henstock]
def is_Henstock (π : tagged_prepartition I) : Prop :=
∀ J ∈ π, π.tag J ∈ J.Icc

def is_subordinate (π : tagged_prepartition I) (r : ℝⁿ → ℝ>0) : Prop :=
∀ J ∈ π, J.Icc ⊆ closed_ball (π.tag J) (r (π.tag J))
\end{lstlisting}

\subsection{Cousin's lemma}\label{sec:cousins-lemma}

Cousin's lemma says that for any gauge function
\(\delta\colon\bbR^{n}\to\bbR_{>0}\) and a box, there exists a tagged
partition of this box that is subordinate to \(\delta\). This lemma is
needed to show that the Henstock-Kurzweil integral is well defined: if
it was false, any number would be the Henstock-Kurzweil integral of
any function.

I prove two versions of this lemma. First I prove the lemma as stated
in the previous paragraph with an additional assertion that all boxes
of the partition are homothetic to the original box, see \autoref{lst:cousin-box}.

\begin{lstlisting}[caption={Cousin's lemma for a box},label=lst:cousin-box]
lemma exists_subordinate_Henstock (I : box n) (r : ℝⁿ → ℝ>0) :
  ∃ π : tagged_prepartition I, π.is_partition ∧ π.is_Henstock ∧
    π.is_subordinate r ∧
    (∀ J ∈ π, ∃ m : ℕ, ∀ i, J.upper i - J.lower i =
      (I.upper i - I.lower i) / 2 ^ m) ∧
    π.distortion = I.distortion
\end{lstlisting}

Here is the sketch of the proof. If a box \(I\) does not admit a
tagged partition with these properties, then the same is true for one
of the \(2^{n}\) boxes of the partition
\lstinline=I.split_center=. Thus we obtain an infinite sequence of
boxes \(J_{k}\), each one is twice smaller than the previous one in
each direction, such that none of these boxes admit a partition with
these properties. Let \(a\) be the unique common point of these
boxes. For sufficiently large \(k\), \(J_{k}\) is included in the
closed ball with center~\(a\) and radius~\(r(a)\), hence the one-box
partition of \(J_{k}\) with tag at \(a\) satisfies all the required
properties. This contradiction proves the lemma.

Then I use it to prove that for any prepartition \(\pi\) there exists
a refinement of this prepartition with the same distortion, see
\autoref{def:GP-integral}, and a choice of tags such that the
resulting tagged prepartition is Henstock and is subordinate to a
given gauge function, see \autoref{lst:cousin-partition}. To prove
this, I apply the previous lemma to each box of \(\pi\), then merge
these partitions using \lstinline=prepartition.bUnion=. I use this
version of Cousin's lemma to prove that the GP-integral is well
defined.

\begin{lstlisting}[caption={Cousin's lemma for a prepartition},label=lst:cousin-partition]
lemma exists_le_Henstock_Union_eq (r : ℝⁿ → ℝ>0) (π : prepartition I) :
  ∃ π' : tagged_prepartition I, π'.to_prepartition ≤ π ∧
    π'.is_Henstock ∧ π'.is_subordinate r ∧ π'.distortion = π.distortion ∧
    π'.Union = π.Union :=
\end{lstlisting}

\subsection{The filters}\label{sec:filters}

Different “box” integrals (Riemann, McShane, Henstock-Kurzweil, GP)
are defined as the limits of the Riemann sums along some filters on
the space of partitions of a box.

I define the structure \lstinline=integration_params=, see
\autoref{lst:integration-params} that holds data needed to define
either of these four integrals and a few more.

\begin{lstlisting}[caption={Structure holding parameters needed to define a box integral},label=lst:integration-params]
structure integration_params : Type :=
(bRiemann bHenstock bDistortion : bool)
\end{lstlisting}

The parameters have the following meaning:

\noindent%
\begin{tabular}{rp{10cm}}
  \lstinline=bRiemann=&this is a Riemann integral, the gauge function must be a constant;\\
  \lstinline=bHenstock=&tags must belong to the closure of their boxes;\\
  \lstinline=bDistortion=&the gauge function may depend on the distortion of a partition.
\end{tabular}

The integration parameters used to define the Riemann,
Henstock-Kurzweil, McShane, and GP-integrals are listed in
\cref{lst:well-known-params}.

\begin{lstlisting}[caption={Parameters corresponding to well-known integrals},label=lst:well-known-params]
def Riemann : integration_params :=
{ bRiemann := tt,
  bHenstock := tt,
  bDistortion := ff }

def Henstock : integration_params :=
{ bRiemann := ff,
  bHenstock := tt,
  bDistortion := ff }

def McShane : integration_params :=
{ bRiemann := ff,
  bHenstock := ff,
  bDistortion := ff }

def GP : integration_params :=
{ bRiemann := ff,
  bHenstock := tt,
  bDistortion := tt }
\end{lstlisting}

On one hand, this design choice allows me to prove some lemmas (e.g.,
Henstock-Sacks inequality, see \autoref{sec:henst-sacks-ineq})
uniformly for all these integrals. On the other hand, it is hard to
add more integrals to the collection, see Bongiorno's
survey~\cite{BONGIORNO2002587} for other reasonable generalizations of
the Henstock-Kurzweil integral to higher dimension.

I require that the gauge function satisfies the following condition,
see \autoref{lst:r-cond}. If \lstinline=l.bRiemann= is false, then
this condition is trivial, otherwise it says that the gauge function
is actually a constant function.

\begin{lstlisting}[caption={Condition on the gauge function},label=lst:r-cond]
def r_cond {n : ℕ} (l : integration_params) (r : ℝⁿ → ℝ>0) : Prop :=
l.bRiemann → ∀ x, r x = r 0
\end{lstlisting}

For each set of parameters \lstinline=l : integration_params= and a
box~\(I\), we define several filters on the space of prepartitions of
\(I\). All these filters have basis sets of the same type, see
\autoref{lst:mem-base-set}.

\begin{lstlisting}[caption={Basis sets used to define filters related to integration parameters.},label=lst:mem-base-set]
structure mem_base_set (l : integration_params) (I : box n) (c : ℝ≥0)
  (r : ℝⁿ → ℝ>0) (π : tagged_prepartition I) : Prop :=
(is_subordinate : π.is_subordinate r)
(is_Henstock : l.bHenstock → π.is_Henstock)
(distortion_le : l.bDistortion → π.distortion ≤ c)
(exists_compl : l.bDistortion → ∃ π' : prepartition I,
  π'.Union = I \ π.Union ∧ π'.distortion ≤ c)
\end{lstlisting}

We already saw the first three assumptions in the informal definition
of the GP-integral. The last assumption is trivial if \(\pi\) is a
partition (then we can choose \(\pi'\) to be the empty
prepartition). One can show that it is also trivial whenever \(c>1\)
but I decided to cut a corner here and introduce this assumption
instead of adding an explicit assumption \(c>1\) here and there and
proving one more lemma.

The most important filter related to a set of integration parameters
is the filter \lstinline=to_filter_Union= below. Cousin's lemma from
\autoref{sec:cousins-lemma} implies that this filter is
nontrivial. The actual definition uses more intermediate filters but
the result is equal (though not definitionally equal) to the code in
\autoref{lst:filters}.

\begin{lstlisting}[caption=Filters defined by a set of integration parameters and a box,label=lst:filters]
def to_filter (l : integration_params) (I : box n) :
  filter (tagged_prepartition I) :=
⨆ c : ℝ≥0, ⨅ (r : ℝⁿ → ℝ>0) (hr : l.r_cond r),
  𝓟 {π | l.mem_base_set I c r π}

def to_filter_Union (l : integration_params) (I : box n)
  (π₀ : prepartition I) :=
l.to_filter I ⊓ 𝓟 {π | π.Union = π₀.Union}
\end{lstlisting}

The filter \lstinline=to_filter= is useful to prove facts about
integrals on subboxes.

\subsection{Box-additive function}%
\label{sec:box-addit-funct}

I introduce the following definition.

\begin{definition}
  A function on boxes in \(\bbR^{n}\) taking values in an additive
  group is said to be \emph{box-additive} if for any box \(I\) and its
  partition \(\pi\), the sum of its values on the boxes of \(\pi\) is
  equal to its value on \(I\).

  A function is said to be \emph{box-additive on subboxes of
    \(I_{0}\)} if the same property holds true whenever \(I\le I_{0}\).
\end{definition}

In order to deal with these two notions simultaneously, the actual
definition takes an argument of the type \lstinline=with_top (box n)=,
see \autoref{lst:box-additive}. Similarly to the type
\lstinline=with_bot (box n)=, this type is the disjoint union of
\lstinline=box n= and the top element \lstinline=⊤=.

\begin{lstlisting}[caption={Definition of a box-additive map},label=lst:box-additive]
structure box_additive_map (n : ℕ) (G : Type*) [add_comm_group G]
  (I : with_top (box n)) : Type* :=
(to_fun : box n → G)
(sum_partition_boxes' : ∀ J : box n, (J : with_top (box n)) ≤ I →
  ∀ π : prepartition J, π.is_partition →
    ∑ Ji in π.boxes, to_fun Ji = to_fun J)
\end{lstlisting}

I use notation \lstinline=n →ᵇᵃ G= for functions that are box-additive
on the whole space and \lstinline=n →ᵇᵃ[I] G= for functions that are
box-additive on subboxes of \(I\).

It suffices to verify additivity only on the two-box partitions
\lstinline=split= introduced above, see
\autoref{lst:of-map-split-add}. Indeed, let \(t\) be the set of all
hyperplanes that contain faces of a partition~\(\pi\) of \(I\). Then
the partition \lstinline=split_many I t= can be obtained by a series
of splits along a single hyperplane both from the trivial one-box
partition and from~\(\pi\). Therefore, if \(f\) is additive on the
two-box partitions, then the sum of values of \(f\) over all boxes of
\lstinline=split_many I t= is equal both to \(f(I)\) and to the sum of
its values over all boxes of~\(\pi\).

\begin{lstlisting}[caption={A map additive on splits by a hyperplane is a box-additive map},label=lst:of-map-split-add]
def of_map_split_add (f : box n → G) (I₀ : with_top (box n))
  (hf : ∀ I : box n, (I : with_top (box n)) ≤ I₀ →
    ∀ {i x}, x ∈ Ioo (I.lower i) (I.upper i) →
    f (I.split_lower i x) + f (I.split_upper i x) = f I) :
  n →ᵇᵃ[I₀] G
\end{lstlisting}

Here \lstinline=I.split_lower i x= and \lstinline=I.split_upper i x=
are the boxes of the partition \lstinline=split I=. Since one of them
can be empty, they have type \lstinline=with_bot (box n)=, so the
actual code looks like \lstinline=option.elim (I.split_lower i x) 0 f=
instead of \lstinline=f (I.split_lower i x)=.

Each locally finite measure \(\mu\) defines a box-additive function.
Next, if \(f\colon\bbR^{n}\to E\) is integrable (in any reasonable
sense) on a box~\(I\), then its integral over a box is a box-additive
function on subboxes of \(I\), see \autoref{sec:henst-sacks-ineq}.

One more construction of box-additive functions appears in the proof
of the divergence theorem. Given a box-additive function \(f_{y}\) on
each cross-section \(x^{i}=y\), \(y \in [a^{i}, b^{i}]\) of a closed
box \lstinline~I₀.Icc = [a, b]~, the function given by
\lstinline~g J = f (J.upper i) (J.face i) - f (J.lower i) (J.face i)~
is box additive on subboxes of~\(I_{0}\).

To ensure nice definitional equality properties of the result, the
actual definition involves two functions and a proof that they are
equal on all the boxes relevant to the definition, see
\autoref{lst:upper-sub-lower}.

\begin{lstlisting}[caption={Difference of values of a box-additive map on the front and back faces of a box is a box-additive map},label=lst:upper-sub-lower]
def upper_sub_lower {G : Type u} [add_comm_group G]
  (I₀ : box (n + 1)) (i : fin (n + 1)) (f : ℝ → box n → G)
  (fb : Icc (I₀.lower i) (I₀.upper i) → n →ᵇᵃ[I₀.face i] G)
  (hf : ∀ x (hx : x ∈ Icc (I₀.lower i) (I₀.upper i)) J,
    f x J = fb ⟨x, hx⟩ J) :
  (n + 1) →ᵇᵃ[I₀] G :=
\end{lstlisting}

\subsection{Box integral}%
\label{sec:box-integral}

The box integral of a function \(f\colon\bbR^{n}\to E\) on an
open-closed box \(I\) in the sense of integration parameters \(l\) is
defined as the limit of the Riemann sum over a partition \(\pi\) of
\(I\) along the filter \lstinline=l.to_filter_Union ⊤=, where
\lstinline=⊤= is the one-box partition of~\(I\). If the limit does not
exist, then the integral is defined to be zero, see
\autoref{lst:box-integral}.

I define the integral of a function \(f\colon \bbR^{n}\to E\) with
respect to a box-additive volume taking values in the space of
continuous linear functions \lstinline=E →L[ℝ] F=. This way one can
use the same definition, e.g., for Riemann-Stieltjes integrals.
However, I only used this definition in the case \(E=F\) and
\lstinline+vol J x = (μ J).to_real • x+ for some measure \(\mu\). So,
this generalization might be a case of overengineering.

\begin{lstlisting}[caption={Definition of a box integral},label=lst:box-integral]
def integral_sum (f : ℝⁿ → E) (vol : n →ᵇᵃ (E →L[ℝ] F))
  (π : tagged_prepartition I) : F :=
∑ J in π.boxes, vol J (f (π.tag J))

def has_integral (I : box n) (l : integration_params) (f : ℝⁿ → E)
  (vol : n →ᵇᵃ (E →L[ℝ] F)) (y : F) : Prop :=
tendsto (integral_sum f vol) (l.to_filter_Union I ⊤) (𝓝 y)

def integrable (I : box n) (l : integration_params) (f : ℝⁿ → E)
  (vol : n →ᵇᵃ (E →L[ℝ] F)) : Prop :=
∃ y, has_integral I l f vol y

def integral (I : box n) (l : integration_params) (f : ℝⁿ → E)
  (vol : n →ᵇᵃ (E →L[ℝ] F)) : F :=
if h : integrable I l f vol then h.some else 0
\end{lstlisting}

Usual theorems (uniqueness of the integral, Cauchy convergence test,
additivity) immediately follow from the definition and properties of
the limit.

\subsection{The Henstock-Sacks inequality}%
\label{sec:henst-sacks-ineq}

The Henstock-Sacks inequality for the Henstock-Kurzweil integral says
the following. Let \(f\) be a function integrable on a box \(I\); let
\(\delta\colon \bbR^{n} \to \bbR_{>0}\) be a gauge function such that
for any tagged partition of \(I\) subordinate to \(\delta\), the
integral sum over this partition is \(\eps\)-close to the
integral. Then for any tagged \emph{prepartition} \(\pi\), the
integral sum over \(\pi\) differs from the integral of \(f\) over the
part of \(I\) covered by \(\pi\) by at most \(\eps\).

This inequality is used, e.g., to prove that a function that is
Henstock-Kurzweil integrable on a box \(I\), is Henstock-Kurzweil
integrable on any subbox of \(I\) and defines a box-additive function
on subboxes of \(I\). I prove several versions of this inequality for
any of the \enquote{box} integrals.

Instead of using predicate assumptions on \(\delta\), I define
\lstinline=convergence_r= (see \autoref{lst:conv-r}) to be a function
\(\delta\colon\mathbb R^{n}\to\mathbb R_{>0}\) such that
\begin{itemize}
\item if \lstinline=l.bRiemann=, then \(\delta\) is a constant;
\item if \(\eps > 0\), then for any tagged partition \(\pi\) of \(I\)
  satisfying the predicate \lstinline=l.mem_base_set I c δ=, the
  integral sum of \(f\) over \(\pi\) differs from the integral of
  \(f\) over \(I\) by at most~\(\eps\).
\end{itemize}

\begin{lstlisting}[caption={Gauge function that provides a witness of integrability},label=lst:conv-r]
def convergence_r (h : integrable I l f vol) (ε : ℝ) (c : ℝ≥0) :
  ℝⁿ → ℝ>0
\end{lstlisting}

Let me quote two versions of the Henstock-Sacks inequality here. One
version compares the Riemann sums of a function over two prepartitions
that cover the same part of the box, see \autoref{lst:henstock-sacks}.
\begin{lstlisting}[caption={Henstock-Sacks inequality for two integral sums},label=lst:henstock-sacks]
lemma dist_integral_sum_le_of_mem_base_set (h : integrable I l f vol)
  (hpos₁ : 0 < ε₁) (hpos₂ : 0 < ε₂)
  (hπ₁ : l.mem_base_set I c₁ (h.convergence_r ε₁ c₁) π₁)
  (hπ₂ : l.mem_base_set I c₂ (h.convergence_r ε₂ c₂) π₂)
  (hU : π₁.Union = π₂.Union) :
  dist (integral_sum f vol π₁) (integral_sum f vol π₂) ≤ ε₁ + ε₂
\end{lstlisting}

The other replaces one of these Riemann sums with the sum of integrals
of the function over the boxes of the partition, see
\autoref{lst:henstock-sacks2}.

\begin{lstlisting}[caption={Henstock-Sacks inequality on the distance between an integral sum and a sum of integrals},label=lst:henstock-sacks2]
lemma dist_integral_sum_sum_integral_le_of_mem_base_set_of_Union_eq
  (h : integrable I l f vol) (hpos : 0 < ε)
  (hπ : l.mem_base_set I c (h.convergence_r ε c) π)
  (hU : π.Union = π₀.Union) :
  dist (integral_sum f vol π) (∑ J in π₀.boxes, integral J l f vol) ≤ ε
\end{lstlisting}

\subsection{Divergence theorem for the GP-integral}%
\label{sec:diverg-theor-gp}

To prove the divergence theorem for the GP-integral
\autoref{thm:divergence}, we prove that each partial derivative is
GP-integrable with the integral equal to the difference of the
integral of the original function over the front and back faces of the
box, see \autoref{lst:GP-pderiv}.

\begin{lstlisting}[caption={Key lemma for the divergence theorem for the GP-integral},label=lst:GP-pderiv]
lemma has_integral_GP_pderiv (f : ℝⁿ⁺¹ → E) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E)
  (s : set (ℝⁿ⁺¹)) (hs : countable s)
  (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
  (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x)
  (i : fin (n + 1)) :
  has_integral I GP (λ x, f' x (e i)) volume
    (integral (I.face i) GP (f ∘ I.front_face i) volume -
      integral (I.face i) GP (f ∘ I.back_face i) volume)
\end{lstlisting}

Here and in the next listing, \(volume\) is a notation for the
box-additive volume \lstinline=volume : (n + 1) →ᵇᵃ (E →L[ℝ] E)=
defined by \lstinline+dV J x = (∏ j, J.upper j - J.lower j) • x+.

The sum of these statements for all terms of the divergence gives us
the divergence theorem, see \autoref{lst:divergence-GP}.

\begin{lstlisting}[caption={The divergence theorem for the GP-integral},label=lst:divergence-GP]
lemma has_integral_GP_divergence (f : ℝⁿ⁺¹ → Eⁿ⁺¹)
  (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : countable s)
  (Hs : ∀ x ∈ s, continuous_within_at f I.Icc x)
  (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x) :
  has_integral I GP (λ x, ∑ i, f' x (e i) i) volume
    (∑ i, (integral (I.face i) GP (f ∘ I.front_face i) volume -
      integral (I.face i) GP (f ∘ I.back_face i) volume))
\end{lstlisting}

The proof of the main lemma follows the same scheme as the standard
proof of the Fundamental Theorem of Calculus for the Henstock-Kurzweil
integral: given a positive number \(\eps\) and an upper estimate \(c\)
on the distortion of the partition, for each point \(x\) of
differentiability, one can choose \(\delta(x)>0\) such that the
estimate \(f(y)=f(x)+f'(x)(y-x)+o(y-x)\) and \(\Sigma(\pi)\le c\)
imply that the difference between the integrals of
\(f\) over the \(i\)-th front and back faces of a \(\delta(x)\)-small
box \(J\ni x\) is \(\eps V(J)\)-close to the term
\(\frac{\partial f}{\partial x^{i}}V(J)\) of the Riemann sum for the
integral of the partial derivative.

I do one modification to this argument that allows me to use weaker
assumptions on a countable set of points. Namely, for \(x\in s\) I
choose \(\delta(x)\) so that for a \(\delta(x)\)-small box \(J\ni x\),
the term corresponding to this box has norm less than \(\kappa(x)>0\),
where \(\sum_{x\in s}\kappa(x)<\eps/2\). This is possible due to the
continuity of \(f\) at \(x\).

\subsection{McShane and Bochner integrability}%
\label{sec:mcsh-bochn-integr}

In order to transfer the result from the GP-integral to the Bochner
integral, I prove that any Bochner integrable function is integrable
in the sense of any box integral with \lstinline~bRiemann = ff~. In
other words, a Bochner integrable function is integrable in the sense
of the McShane, Henstock-Kurzweil, and GP-integrals, see
\autoref{lst:bochner-imp-McShane}.

\begin{lstlisting}[caption=Bochner integrability implies box integrability,label=lst:bochner-imp-McShane]
lemma integrable_on.has_box_integral {f : ℝⁿ → E} {μ : measure ℝⁿ}
  [is_locally_finite_measure μ] {I : box n} (hf : integrable_on f I μ)
  (l : integration_params) (hl : l.bRiemann = ff) :
  has_integral I l f μ.to_box_additive.to_smul (∫ x in I, f x ∂μ)
\end{lstlisting}

The proof follows R.~Gordon's book~\cite{Gordon55}, with some
modifications required to generalize it from a function
\(f\colon\bbR\to\bbR\) to a function \(f\colon\bbR^{n}\to E\).

First, I prove that the indicator function of a measurable set~\(s\)
is McShane integrable with respect to the volume defined by a locally
finite measure~\(\mu\). This immediately implies integrability of
simple functions. Then I show that changing the values of a function
on a set of measure zero does not affect its integral. Finally, I use
approximations of integrable functions by a sequence of simple
functions to prove McShane integrability of a Bochner integrable
function.

\subsection{Divergence theorem for the Bochner integral}%
\label{sec:diverg-theor-bochn}

Since any Bochner integrable function is GP-integrable, we immediately
obtain the divergence theorem for the Bochner integral under
assumptions that the function is continuous on a closed box, is
differentiable at all but countably many points of this box, and has
integrable divergence, see \autoref{lst:divergence-bochner-prelim}.

\begin{lstlisting}[caption={The divergence theorem for the Bochner integral, preliminary version},label=lst:divergence-bochner-prelim]
lemma integral_divergence_aux (I : box (n + 1)) (f : ℝⁿ⁺¹ → Eⁿ⁺¹)
  (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : countable s)
  (Hc : continuous_on f I.Icc)
  (Hd : ∀ x ∈ I.Icc \ s, has_fderiv_within_at f (f' x) I.Icc x)
  (Hi : integrable_on (λ x, ∑ i, f' x (e i) i) I.Icc) :
  ∫ x in I.Icc, ∑ i, f' x (e i) i =
    ∑ i : fin (n + 1),
      ((∫ x in (I.face i).Icc, f (I.front_face i x) i) -
        ∫ x in (I.face i).Icc, f (I.back_face i x) i)
\end{lstlisting}

I slightly generalize this result, see
\autoref{lst:divergence-bochner}. First, I drop the differentiability
assumption on the boundary of~\(I\). To do this, I apply the auxiliary
result to an increasing sequence of subboxes that cover the interior
of \(I\). Second, I allow \(a^{i}=b^{i}\); in this case both sides are
equal to zero.

\begin{lstlisting}[caption={The divergence theorem for the Bochner integral},label=lst:divergence-bochner]
lemma integral_divergence (a b : ℝⁿ⁺¹) (hle : a ≤ b) (f : ℝⁿ⁺¹ → Eⁿ⁺¹)
  (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : countable s)
  (Hc : continuous_on f (Icc a b))
  (Hd : ∀ x : ℝⁿ⁺¹, (∀ i, x i ∈ Ioo (a i) (b i)) → x ∉ s,
    has_fderiv_at f (f' x) x)
  (Hi : integrable_on (λ x, ∑ i, f' x (e i) i) (Icc a b)) :
  ∫ x in Icc a b, ∑ i, f' x (e i) i =
    ∑ i : fin (n + 1), ((∫ x in face i, f (front_face i x) i) -
      ∫ x in face i, f (back_face i x) i)
\end{lstlisting}

\section{Applications to complex analysis}%
\label{sec:appl-compl-analys}

The main goal of the project was to formalize a version of the
divergence theorem that implies the Cauchy integral formula under
standard assumptions. In this section, I will briefly explain how I
deduce the Cauchy integral formula from
\autoref{thm:divergence-Bochner}. While many textbooks on complex
analysis prove these formulas for functions \(f\colon \bbC\to \bbC\), I
prove them for functions that take values in a complex Banach space
\(E\). As before, I have to assume that \(E\) has a second countable
topology because of the way the Bochner integral is defined in
mathlib.

First, consider an open rectangle
\(R=\set{z|a\le \Re z\le b,c\le \Im z\le d}\) on the complex
plane~\(\bbC\). If \(f\colon \bbC\to E\) is continuous on \(R\) and is
complex differentiable at all but countably many points of the
interior of~\(R\), then one can apply the divergence theorem to the
function \(F\colon \bbC \to E^{2}\) given by \(F(z)=(-if(z),
f(z))\). Due to Cauchy-Riemann equations, the left-hand side
of~\eqref{eqn:green-rect} equals zero. It is easy to see that the
right-hand side is equal to the integral
\(\int_{\partial R}f(z)\,dz\). Thus we have the Cauchy-Goursat theorem
for a rectangular domain, see \autoref{lst:cauchy-rect}.

\begin{lstlisting}[caption={The Cauchy-Goursat theorem for a rectangle},label=lst:cauchy-rect]
lemma cauchy_theorem_rect (f : ℂ → E) (z w : ℂ)
  (s : set ℂ) (hs : countable s)
  (Hc : continuous_on f (ICC z.re w.re ×ℂ Icc z.im w.im))
  (Hd : ∀ x ∈ (IOO z.re w.re ×ℂ IOO z.im w.im) \ s,
    differentiable_at ℂ f x) :
  (∫ x in z.re..w.re, f (x + z.im * 𝑖)) -
    (∫ x in z.re..w.re, f (x + w.im * 𝑖)) +
    (𝑖 • ∫ y in z.im..w.im, f (re w + y * 𝑖)) -
    𝑖 • ∫ y in z.im..w.im, f (re z + y * 𝑖) = 0 :=
\end{lstlisting}

To formulate the Cauchy-Goursat theorem for an annulus and a circle, I
define the circle integral \(\oint_{|z-c|=R}f(z)\,dz\) as
\(\int_{0}^{2\pi}(c+Re^{\theta i})'f(c+Re^{\theta i})\,d\theta\), see
\autoref{lst:circle-integral}.

\begin{lstlisting}[caption=Definition of the circle integral \(\oint_{|z-c|=R}f(z)\,dz\),label=lst:circle-integral]
def circle_map (c : ℂ) (R : ℝ) : ℝ → ℂ := λ θ, c + R * exp (θ * 𝑖)

def circle_integral (f : ℂ → E) (c : ℂ) (R : ℝ) : E :=
∫ θ in 0..2 * π, deriv (circle_map c R) θ • f (circle_map c R θ)
\end{lstlisting}

Applying the Cauchy-Goursat theorem for a rectangle to the function
\(F(z)=e^{z}f(c+e^{z})\) on the rectangle \(\ln r\le \Re z\le \ln R\),
\(0\le \Im z\le 2\pi\), I prove the Cauchy-Goursat theorem for a
function differentiable on an annulus, see \autoref{lst:cauchy-annulus}.

\begin{lstlisting}[caption=The Cauchy-Goursat theorem for an annulus,label=lst:cauchy-annulus]
lemma cauchy_thm_annulus {c : ℂ} {r R : ℝ} (h0 : 0 < r)
  (hle : r ≤ R) {f : ℂ → E} {s : set ℂ} (hs : countable s)
  (hc : continuous_on f (closed_ball c R \ ball c r))
  (hd : ∀ z ∈ ball c R \ closed_ball c r \ s, differentiable_at ℂ f z) :
  ∮ z in C(c, R), f z = ∮ z in C(c, r), f z
\end{lstlisting}

Next, I apply this theorem to the function \(\frac{f(z)}{z-c}\)
(formally, \((z-c)^{-1}\cdot f(z)\) because \(f\) is a vector-valued
function) and take the limit as \(r\) tends to \(0\) from the
right. Thus, I prove the Cauchy integral formula for the value of a
complex differentiable function at the center of a disk, see
\autoref{lst:cauchy-int-center}. This theorem will be later
generalized to any point of the disk, but I will use this case to
prove the general version.

\begin{lstlisting}[caption=Cauchy integral formula for the center of a disk,label=lst:cauchy-int-center]
lemma cauchy_integral_disk_center {R : ℝ} (h0 : 0 < R)
  {f : ℂ → E} {c : ℂ} {s : set ℂ} (hs : countable s)
  (hc : continuous_on f (closed_ball c R))
  (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
  ∮ z in C(c, R), (z - c)⁻¹ • f z = (2 * π * 𝑖 : ℂ) • f c :=
\end{lstlisting}

Applying this lemma to the function \((z-c)\cdot f(z)\), we prove the
Cauchy-Goursat theorem for a disk, see \autoref{lst:cauchy-circle}.

\begin{lstlisting}[caption=The Cauchy-Goursat theorem for a disk,label=lst:cauchy-circle]
lemma cauchy_thm_disk {R : ℝ} (h0 : 0 ≤ R) {f : ℂ → E}
  {c : ℂ} {s : set ℂ} (hs : countable s)
  (hc : continuous_on f (closed_ball c R))
  (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) :
  ∮ z in C(c, R), f z = 0 :=
\end{lstlisting}

Next, I show the Cauchy integral formula
\[
  f(w)=\frac{1}{2\pi i}\oint_{|z-c|=R}\frac{f(z)}{z-w}\,dz
\]
for any point of the open disc, \(|w-c|<R\), see
\autoref{lst:cauchy-int}. To obtain this result, I apply the
Cauchy-Goursat theorem to the function
\[
  g(z)=
  \begin{cases}
    f'(w),&\text{if }z=w;\\
    \frac{f(z)-f(w)}{z-w},&\text{otherwise}.
  \end{cases}
\]
If \(f\) is differentiable at \(w\), then \(g\) satisfies the
assumptions of the previous theorem, hence the integrals of
\(\frac{f(z)}{z-w}\) and \(\frac{f(w)}{z-w}\) over the circle
\(|z-c|=R\) are equal. It is easy to see that the latter integral
equals \(2\pi i f(w)\).

If \(w\) belongs to the countable set where \(f\) is not guaranteed to
be differentiable, then the same formula follows from the previous case by
continuity.

\begin{lstlisting}[caption=Cauchy integral formula for a circle,label=lst:cauchy-int]
lemma cauchy_integral_disk {R : ℝ} {c w : ℂ} {f : ℂ → E} {s : set ℂ}
  (hs : countable s) (hw : w ∈ ball c R)
  (hc : continuous_on f (closed_ball c R))
  (hd : ∀ x ∈ ball c R \ s, differentiable_at ℂ f x) :
  (2 * π * 𝑖 : ℂ)⁻¹ • ∮ z in C(c, R), (z - w)⁻¹ • f z = f w :=
\end{lstlisting}

The Cauchy integral formula immediately implies that a function
\(f\colon\bbC\to E\) that is complex differentiable on an open disk
and is continuous on the corresponding closed disk must be analytic on
the interior of this disk. The coefficients of the Taylor series are
given by Cauchy integrals, see \cref{lst:cauchy-series,lst:diff-analytic}.

\begin{lstlisting}[caption=Power series for a function differentiable on a disk,label=lst:cauchy-series]
def cauchy_power_series (f : ℂ → E) (c : ℂ) (R : ℝ) :
  formal_multilinear_series ℂ ℂ E :=
λ n, continuous_multilinear_map.mk_pi_field ℂ _ $
  (2 * π * 𝑖 : ℂ)⁻¹ • ∮ z in C(c, R), (z - c) ^ (-n - 1 : ℤ) • f z
\end{lstlisting}

\begin{lstlisting}[caption=Analyticity of a complex differentiable function,label=lst:diff-analytic]
lemma analytic_of_differentiable {R : ℝ≥0} {c : ℂ} {f : ℂ → E}
  {s : set ℂ} (hs : countable s) (hc : continuous_on f (closed_ball c R))
  (hd : ∀ z ∈ ball c R \ s, differentiable_at ℂ f z) (hR : 0 < R) :
  has_fpower_series_on_ball f (cauchy_power_series f c R) c R :=
\end{lstlisting}

I started to use these theorems to build a complex analysis library in
Lean. For example, I proved the Riemann removable singularity theorem,
see \autoref{lst:removable-singularity}.

\begin{lstlisting}[caption={Riemann removable singularity theorem},label=lst:removable-singularity]
lemma removable_singularity
  (hd : ∀ᶠ z in 𝓝[≠] c, differentiable_at ℂ f z)
  (ho : is_o (λ z, f z - f c) (λ z, (z - c)⁻¹) (𝓝[≠] c)) :
  ∃ y : E, tendsto f (𝓝[≠] c) (𝓝 y)
\end{lstlisting}

Here \lstinline{𝓝[≠] c} is the filter of punctured neighborhoods of
\(c\).

\section{Future plans}\label{sec:future-plans}

\subsection{Other integrals}\label{sec:other-integrals}

One possible direction of improvement would be to formalize the
divergence theorem for (some of the) other integrals listed in the
Bongiorno's survey~\cite{BONGIORNO2002587}. Some of these theorems
allow the function to be continuous, not differentiable, on a
countable set of \emph{coordinate hyperplanes}. These theorems can be
transfered to more general versions of the Cauchy-Goursat theorems.

The main obstacle for this project is that I define \enquote{box}
integrals in a non-extensible way, see \autoref{sec:filters}. So, to
add more integrals (or to replace the GP-integral with a better one),
one has to seriously refactor the definition.

\subsection{Complex analysis in higher dimension}%
\label{sec:compl-analys-high}

Most of the proofs discussed in \autoref{sec:appl-compl-analys} can be
easily generalized to the case of a function
\(f\colon \bbC^{n}\to E\). I mentor a student who tries to generalize
the Cauchy integral formula as a part of a course.

\subsection{The Cauchy-Goursat theorem for any domain}\label{sec:cauchy-goursat-any}

My goal was to show that it is possible to deduce the Cauchy-Goursat
theorem from the divergence theorem, so I formalized the
Cauchy-Goursat theorem only for a few special cases (a rectangle, an
annulus, and a disk). One can deduce the general Cauchy-Goursat
theorem from the version for a rectangle but it requires quite a few
topological lemmas that are not in \texttt{mathlib} yet.

\subsection{One-dimensional complex analysis}%
\label{sec:one-dimens-compl}

Formalization of the Cauchy-Goursat theorem makes it possible to
formalize many theorems from the one-dimensional complex analysis. I
already formalized the removable singularity theorem, but, clearly,
this is just the beginning.

My main goal for the next year or two is to formalize Ilyashenko's
proof of the fact that a polynomial vector field on \(\bbR^{2}\) has
only finitely many limit cycles (i.e., isolated periodic solutions),
at least in the case of hyperbolic singular points. The proof of this
theorem heavily relies on the complex analysis.

\bibliography{divthm}
\end{document}