is obviously strictly convex. This can be shown by expanding and
rearranging the strict convexity condition
\begin{equation}
- \int_\Omega (\lambda x + (1-\lambda)y - f)^2 \, dx < \lambda
- \int_\Omega (x - f)^2 \, dx + (1 - \lambda) \int_\Omega (y - f)^2 \,
+ \int_\Omega (\lambda u_1 + (1-\lambda)u_2 - f)^2 \, dx < \lambda
+ \int_\Omega (u_1 - f)^2 \, dx + (1 - \lambda) \int_\Omega (u_2 - f)^2 \,
dx
\end{equation}
to obtain that it is equivalent to
\begin{equation}
- - \lambda(1 - \lambda) \int_\Omega (x - y)^2 \, dx < 0
+ - \lambda(1 - \lambda) \int_\Omega (u_1 - u_2)^2 \, dx < 0
\end{equation}
-which is true for $0 < \lambda < 1$ and $x \neq y$.
+which is true for $0 < \lambda < 1$ and $u_1 \neq u_2$.
The anisotropic total variation
\begin{equation}
\TVA(u) = \sup_{\norm{\xi}_A^* \leq 1} \int_\Omega u \diver \xi \,
dx
\end{equation}
-can be thought of as -- and has the properties of -- a norm, and is
+can be thought of as---and has the properties of---a semi-norm, and is
therefore convex. The sum of the two is thus strictly convex, which,
given the existence of a minimizer, implies uniqueness.
\subsection{Coercivity}
-We need coercivity to show that we cannot go further and further away to
-obtain a better and better solution. This means that $\lnorm{u}_{L^2} \to
-\infty$ should imply that $F(u) \to \infty$, which is obvious from the
-fidelity term for some fixed $f \in L^2(\Omega)$.
+\fixme{Sequential coercivity?}
-From the coercivity we can conclude that we should be able to find some
-near-minimal solutions somewhere in $L^2(\Omega)$ without ``going too far
-away.''
+It is obvious from the fidelity term that for some fixed $f \in
+L^2(\Omega)$ if $\lnorm{u}_{L^2} \to \infty$ then $F(u) \to \infty$.
+This tells us something about the locality of potential minimizers.
\begin{figure}
\input{fig/lower_semicont}
The lower semicontinuity is the most tricky part, and this is where we
will take some shortcuts. Lower semicontinuity for a functional $F$ at a
point $u$ means that at points $u_\epsilon$ close to $u$, the functional
-takes values either close to or above $F(u)$. More specifically, for a
-sequence $u_k$ converging to $u$, we have $F(u) \leq \liminf_k F(u_k)$.
-For a function $f : \mathbb{R} \to \mathbb{R}$ this can be visualized as
-in Figure~\ref{fig:lower_semicont}.
+takes values either close to or above $F(u)$. More specifically, for
+every sequence $u_k$ converging to $u$, we have $F(u) \leq \liminf_k
+F(u_k)$. For a function $f : \mathbb{R} \to \mathbb{R}$ this can be
+visualized as in Figure~\ref{fig:lower_semicont}.
Since our space $L^2(\Omega)$ is of infinite dimensions things become a
-little bit problematic here. The problem lies in the fact that a
+little problematic here. The problem lies in the fact that a
functional which is continuous with respect to sequences is not
necessarily continuous with respect to the underlying topology. In
-other words, in these spaces, there is a difference between sequential
+other words, in these spaces, there can be a difference between sequential
continuity and topological continuity. Topological continuity implies
-sequential continuity, but not the other way around. One way to get
+sequential continuity, but the converse does not hold. One way to get
around this would be to consider topological \emph{nets}, an extension
of sequences, but for simplicity, and because it might not add much to
the understanding of the restoration method, we will stick to proving
continuity see for example Megginson's book on Banach space theory
\cite{megginson}.
-\fixme{We consider the weak topology. Because it is convenient?}
+\fixme{We consider the weak topology. Because it is convenient? No,
+apparently to get the existence proof to work, but it does not say
+anything about weakness in the book? We do however have sequential
+coercivity in the assumptions of the Theorem, which might be a problem.}
We say that a sequence $f_n$ in $L^2(\Omega)$ converges weakly to $f$ if
\begin{equation}
- \lim_{n \to \infty} \int_\Omega f_n \, \xi \, dx = \int_\Omega f \, \xi \,
- dx
+ \lim_{n \to \infty} \int_\Omega f_n \, \xi \, dx = \int_\Omega f \,
+ \xi \, dx
\end{equation}
-for all $\xi \in L^2(\Omega)$ and we write $f_n \rightharpoonup f$. The
-weak topology is characterized by the fact that all weakly convergent
+for all $\xi \in L^2(\Omega)$ and we write $f_n \rightharpoonup f$. An
+important property is that all weakly convergent
sequences also converge in the weak topology. Also, the mapping $u
\mapsto \int_\Omega u \, \xi \, dx$ is weakly continuous for all $\xi
\in L^2(\Omega)$. Note that when we write weakly continuous it is not a
weaker version of continuity, but rather continuity in the weak
-topology, and the same goes for lower semi-continuity.
+topology, and the same goes for weak lower semi-continuity.
Before arguing that our own functional is sequentially weakly lower
-semi-continuous, we present a much needed result.
+semi-continuous, we present a needed result.
\begin{lemma}
Assume that the functional $F : L^2(\Omega) \to \mathbb{R}$ is
defined by
F(u) = \sup_i F_i(u) \leq \sup_i \liminf_{k \to \infty} F_i(u_k)
\end{equation}
from the sequential weak lower semi-continuity of $F_i$. Using that
- $\liminf_{k \to \infty} = \sup_k \inf_{k \leq l}$, we obtain
+ $\liminf_{k \to \infty} u_k = \sup_k \inf_{l \geq k} u_l$, we obtain
\begin{equation}
\begin{aligned}
- F(u) &\leq \sup_i \sup_k \inf_{k \leq l} F_i(u_k) \\
- &= \sup_k \sup_i \inf_{k \leq l} F_i(u_k) \\
- &\leq \sup_k \inf_{k \leq l} \sup_i F_i(u_k) \\
+ F(u) &\leq \sup_i \sup_k \inf_{l \geq k} F_i(u_l) \\
+ &= \sup_k \sup_i \inf_{l \geq k} F_i(u_l) \\
+ &\leq \sup_k \inf_{l \geq k} \sup_i F_i(u_l) \\
&= \liminf_{k \to \infty} F(u_k)
\end{aligned}
\end{equation}
which proves that $F$ is sequentially weakly lower semi-continuous.
\end{proof}
-From our functional in \eqref{eq:first_anisotropic_functional}, we first
+In our functional in \eqref{eq:first_anisotropic_functional}, we first
consider the fidelity term, and rewrite it as a supremum
\begin{equation}
- \int_\Omega (u - v)^2 \, dx
+ \int_\Omega (u - f)^2 \, dx
%= \sup_{\substack{\xi \in L^2(\Omega) \\ \norm{\xi}_{L^2} \leq
%\norm{u-v}_{L^2}}} \int_\Omega (u - v) \, \xi \, dx.
- = \sup \left\{\int_\Omega (u - v) \, \xi \, dx : \xi \in
- L^2(\Omega), \norm{\xi}_{L^2} \leq \norm{u-v}_{L^2} \right\}
+ = \sup \left\{\int_\Omega (u - f) \, \xi \, dx : \xi \in
+ L^2(\Omega), \abs{\xi(x)} \leq \abs{u(x)-f(x)} \right\}
\end{equation}
As the map $u \mapsto \int_\Omega (u - v) \xi\, dx$ is continuous in the
-weak topology, the fidelity term is then a supremum of weakly continuous
+weak topology, the fidelity term is thus a supremum of weakly continuous
functionals, and is thus by Lemma~\ref{lem:sup_semi_cont} sequentially
lower semi-continuous.
\TVA(u) = \sup \left\{\int_\Omega u \, \diver \xi \, dx : \xi \in
C_c^\infty(\Omega, \mathbb{R}^2), \norm{\xi}_A^* \leq 1 \right\}
\end{equation}
-This is again is a
+This is again a
supremum of weakly continuous functionals. Thus the regularization term
is by Lemma~\ref{lem:sup_semi_cont} also sequentially weakly lower
semi-continuous.
+The sum of the two terms is trivially sequentially weakly lower
+semi-continuous functional since
+\begin{equation}
+ \begin{aligned}
+ F_1(u) + F_2(u) &\leq \liminf_{k \to \infty} F_1(u_k) + \liminf_{k
+ \to \infty} F_2(u_k) \\
+ &= \lim_{k \to \infty} \left( \inf_{l \geq k}
+ F_1(u_l) + \inf_{l \geq k} F_2(u_l) \right) \\
+ &\leq \liminf_{k \to
+ \infty} \left( F_1(u_k) + F_2(u_k) \right),
+ \end{aligned}
+\end{equation}
+and thus our functional is sequentially weakly lower semi-continuous.
+
The usual ways of going from coercivity and lower semicontinuity to
existence do not work in infinite dimensions. But with our coercivity
and sequential lower semi-continuity we can apply \fixme{Theorem 5.1 in
The thresholded image definition also allows us to write a non-negative
image $u \geq 0$ as an integral over all the layers
\begin{equation}
- u = \int_0^\infty u^s \, ds.
+ u(x) = \int_0^\infty u^s(x) \, ds.
\label{eq:positive_int}
\end{equation}
-Note that \eqref{eq:positive_int} only holds for a non-negative image,
-something which has to be worked around in the proof of the anisotropic
-coarea formula. For the proof we will avoid measure theory and follow a
-proof given in \cite{olsson2009extending}.
+Note that \eqref{eq:positive_int} only holds for non-negative images,
+which complicates the following proof a little.
\begin{figure}
\input{fig/eta_r}
\end{equation}
\label{thm:anisotropic_coarea}
\end{theorem}
-\begin{proof}
+For the proof we will avoid measure theory and follow a proof given
+in \cite{olsson2009extending}, but first we will present a necessary
+result from measure theory.
+\begin{theorem}[Lebesgue's Dominated Convergence theorem]
+ Let $\{ f_n \}$ be a sequence of real-valued measurable functions on
+ a space $S$ with measure $d\mu$ which converges almost
+ everywhere to a real-valued measurable function $f$. If there exists
+ an integrable function $g$ such that $\abs{f_n} \leq g$ for all $n$,
+ then $f$ is integrable and
+ \begin{equation}
+ \lim_{n \to \infty} \int_S f_n \, d\mu = \int_S f \, d\mu.
+ \end{equation}
+\end{theorem}
+For a proof and further background on measure theory and Lebesgue
+integration theory see for example \cite{bartle1995elements}.
+\begin{proof}[Proof of anisotropic coarea formula.]
Assume that $u \in C^1(\Omega) \cap \BV(\Omega)$. The extension to
all functions $u \in \BV(\Omega)$ can be made by approximation
- arguments but will not be considered here. \fixme{ref maybe}
-
- \paragraph{First we prove that $\TVA(u) \leq \int_{-\infty}^\infty
- \TVA(u^s) \, ds$.}
- Assume that $u \geq 0$ such that the integral in
- \eqref{eq:positive_int} holds, then inserting into the extended
+ arguments but will not be considered here \fixme{theorem 5.3.3 in
+ ziemer}.
+
+ %\paragraph{First we prove that $\TVA(u) \leq \int_{-\infty}^\infty
+ %\TVA(u^s) \, ds$.}
+ \paragraph{Proof of upper bound.}
+ Assume that $u \geq 0$ such that the integral representation in
+ \eqref{eq:positive_int} holds, then inserting
+ \eqref{eq:positive_int} into the extended
total variation definition in \eqref{eq:extended_tv} gives
\begin{equation}
\begin{aligned}
For $u \leq 0$ we use that $\TVA(-v) = \TVA(v)$ and that $\TVA(c + v) =
\TVA(v)$ for any constant $c$. Note that $-u \geq 0$ and that its
thresholded image $(-u)^s$ will be exactly the opposite of $u^{-s}$,
- that is $(-u)^s = 1 - u^{-s}$. This allows us to show that
+ that is $(-u)^s = 1 - u^{-s}$. This allows us to show that
\begin{equation}
\begin{aligned}
\TVA(u) &= \TVA(-u) \leq \int_0^\infty \TVA \big( (-u)^r
- \big) \, dr \\
- &= \int_0^\infty \TVA(1 - u^{-r}) \, dr = \int_0^\infty
+ \big) \, dr
+ = \int_0^\infty \TVA(1 - u^{-r}) \, dr \\ &= \int_0^\infty
\TVA(u^{-r}) \, dr = \int_{-\infty}^0 \TVA(u^s) \, ds.
\end{aligned}
\label{eq:tv_u_neg}
\diver \xi \, dx\\
&= \TVA(u_1) + \TVA(u_2).
\end{aligned}
+ \label{eq:tv_sum}
\end{equation}
- Next, we write a general $u$ as a difference between two positive
- functions $u = u_+ - u_-$ where $u = u_+$ when $u \geq 0$ and $u =
- -u_-$ when $u \leq 0$. Inserting \eqref{eq:tv_u_pos} and
- \eqref{eq:tv_u_neg} we obtain
+ Next, we write a general $u$ as a difference of two positive
+ functions $u = u_+ - u_-$ where $u_+ = \max\{u,0\}$ and $u_- =
+ -\min\{u,0\}$.
+ Inserting \eqref{eq:tv_u_pos} and
+ \eqref{eq:tv_u_neg} into \eqref{eq:tv_sum} we obtain
\begin{equation}
\begin{aligned}
\TVA(u) &\leq \TVA(u_-) + \TVA(u_+) = \TVA(-u_-) + \TVA(u_+) \\
we did not use the differentiability of $u$ in this part of the
proof.
- \paragraph{Next we prove that $\TVA(u) \geq \int_{-\infty}^\infty
- \TVA(u^s) \, ds$.}
+ %\paragraph{Next we prove that $\TVA(u) \geq \int_{-\infty}^\infty
+ %\TVA(u^s) \, ds$.}
+ \paragraph{Proof of lower bound.}
Define the function
\begin{equation}
m(t) = \int_{\{ x \in \Omega : u(x) \leq t\}} \norm{\nabla u}_A
\, dx,
\end{equation}
- and note that $m(\infty) = \TVA(u)$. Since $m(t)$ is non-decreasing
- with $t$, we can apply the existence theorems of Lebesgue \cite[Thm.\
- 17.12, 18.14]{hewstrom} to conclude that $m\prime(t)$ exists almost
- everywhere and that the following inequality holds:
+ and note that $m(\infty) = \TVA(u)$ and $m(-\infty) = 0$. Since
+ $m(t)$ is non-decreasing with $t$, we can apply the existence
+ theorems of Lebesgue \cite[Thm.\ 17.12, 18.14]{hewstrom} to conclude
+ that $m\prime(t)$ exists almost everywhere and that the following
+ inequality holds:
\begin{equation}
\int_{-\infty}^\infty m\prime(t)\, dt \leq m(\infty) - m(-\infty) =
\TVA(u).
\label{eq:tva_geq_mder}
\end{equation}
- Next, fix an $s \in \mathbb{R}$ and define the function
+ Next, fix an $s \in \mathbb{R}$ and define the cut-off function
\begin{equation}
- \eta_r(t) = \begin{cases}
- 0 & \text{if } t < s \\
- (t - s)/r & \text{if } s \leq t < s + r \\
- 1 & \text{if } t > s + r
- \end{cases}
+ \begin{aligned}
+ \eta_r(t) = \begin{cases}
+ 0 & \text{if } t < s, \\
+ (t - s)/r & \text{if } s \leq t < s + r, \\
+ 1 & \text{if } t > s + r,
+ \end{cases}
+ & \qquad
+ \eta_r\prime(t) = \begin{cases}
+ 0 & \text{if } t < s, \\
+ 1 & \text{if } s < t < s + r, \\
+ 0 & \text{if } t > s + r,
+ \end{cases}
+ \end{aligned}
\end{equation}
- visualized in Figure~\ref{fig:eta_r} such that its derivative takes the
- form shown in Figure~\ref{fig:eta_r_diff}. By composing the function
- $\eta_r$ with our image $u$ and Green's identity we obtain
+ visualized in Figure~\ref{fig:eta_r} and \ref{fig:eta_r_diff}. By
+ composing the function $\eta_r$ with our image $u$ and using Green's
+ formula, for example from \cite[Corollary
+ 9.32]{grasmair2010anisotropic} we obtain
\begin{equation}
\int_\Omega - \eta_r(u) \diver \xi \, dx
= \int_\Omega \eta_r\prime(u) \nabla u\cdot \xi \, dx
- = \frac{1}{r} \int_{\{ s \leq u \leq s + r \}} \nabla u\cdot \xi
+ = \frac{1}{r} \int_{\{ s < u \leq s + r \}} \nabla u\cdot \xi
\, dx,
\end{equation}
for all vector fields $\xi \in C_c^\infty(\Omega, \mathbb{R}^2)$.
+ The measure of $\{ x : u(x) = s \text{ and } \nabla u(x) \neq
+ 0\}$ is zero for all $s$ following from \cite[Corollary \rom{1},
+ Section 3.1.2]{evans1991measure}, and thus no problems arise there.
Assuming that $\norm{\xi}_A^* \leq 1$ we have
\begin{equation}
\begin{aligned}
\frac{m(s+r) - m(s)}{r}
- &= \frac{1}{r} \int_{\{ s \leq u \leq s+r \}} \norm{\nabla u}_A
+ &= \frac{1}{r} \int_{\{ s < u \leq s+r \}} \norm{\nabla u}_A
\, dx \\
- &\geq \frac{1}{r} \int_{\{ s \leq u \leq s + r\}} \nabla u \cdot
+ &\geq \frac{1}{r} \int_{\{ s < u \leq s + r\}} \nabla u \cdot
\xi \, dx
= \int_\Omega -\eta_r(u) \diver \xi \, dx.
\end{aligned}
+ \label{eq:m_ineq_sr}
\end{equation}
- As the limit of the left-hand side when $r \to 0$ exists almost
- everywhere, suppose it exists at $s \in \mathbb{R}$, then
+ As the limit when $r \to 0$ of the left-hand side exists almost
+ everywhere, suppose it exists at $s \in \mathbb{R}$. We apply
+ Lebesgue's dominated convergence theorem on the right-hand side in
+ \eqref{eq:m_ineq_sr}, using that $\abs{\eta_r(u) \diver \xi} \leq
+ \abs{u^s \diver \xi}$. As $\xi \in C^\infty_c(\Omega,
+ \mathbb{R}^2)$, it is bounded by the extreme value theorem, and thus
+ $\abs{u^s \diver \xi}$ is integrable. From \eqref{eq:m_ineq_sr} we
+ then obtain
\begin{equation}
m\prime(s) \geq - \int_\Omega u^s \diver \xi \, dx
\end{equation}
\TVA(u) \geq \int_{-\infty}^\infty m'(t) \, dt \geq
\int_{-\infty}^\infty \TVA(u^s) \, ds.
\end{equation}
- Thus the inequality have been proved in both directions, and we have
- equality.
+ Combining the upper and lower bounds just proved, we have equality.
\end{proof}
This coarea formula is our first step in transforming the anisotropic
-total variation into an easily discretizisable expression.
+total variation into an easily discretizable expression.
The anisotropic total variation of the thresholded images occurring in
-the anisotropic coarea formula are very much related to the size of the
+the anisotropic coarea formula is very much related to the size of the
boundary of the level set, as the only variation in a characteristic
function occurs at the boundary of the set. This is why we introduce
the following definition of the anisotropic set perimeter.
\begin{equation}
\PerA(U;\Omega) = \TVA(\idfun_U).
\end{equation}
- A measurable set $U \subset \Omega$ is of finite anisotropic
- perimeter in $\Omega$ if $\idfun_U \in \BV(\Omega)$. \fixme{nope?}
\end{definition}
\nomenclature{$\PerA(u;\Omega)$}{Anisotropic perimeter of set $U$ using
anisotropy tensor $A$.}%
calculated in the following way
\begin{equation}
\begin{aligned}
- \PerA(\{ u > s \}; \Omega) = \TVA(u^s) &= \sup_{\norm{\xi}_A^* \leq 1}
+ \PerA(\{ u > s \}; \Omega) &= \TVA(u^s) \\ &= \sup_{\norm{\xi}_A^* \leq 1}
\int_\Omega u^s \diver \xi \, dx \\
&= \sup_{\norm{\xi}_A^* \leq 1} \int_{\{ u > s \}} \diver \xi \,
dx \\
&= \sup_{\norm{\xi}_A^* \leq 1} \int_{\partial \{ u > s\} } \nu_s
\cdot \xi \, dt \\
- &= \sup_{\norm{\eta} \leq 1} \int_{\partial \{ u > s\} } \nu_s
+ &= \sup_{\abs{\eta} \leq 1} \int_{\partial \{ u > s\} } \nu_s
\cdot \Ahalf \eta \, dt \\
+ &= \int_{\partial \{ u > s\} } \Ahalf \nu_s
+ \cdot \frac{\Ahalf \nu_s}{\abs{\Ahalf \nu_s}} \, dt \\
&= \int_{\partial \{ u > s\} } \sqrt{\nu_s A \nu_s} \, dt.
\end{aligned}
\label{eq:perimeter_calc}
\end{equation}
Here, $\nu_s$ is the unit normal of the level set $\{ u > s \}$ and by
applying the divergence theorem we have assumed that the boundary is
-piecewise smooth, which holds for almost all level sets if $u$ is
-differentiable. A consideration of the perimeter of level sets of any
-function $u \in \BV(\Omega)$ would be heavy on measure theory, and can
-be found in for example \fixme{ref, markus-note? one of the books?}
+\fixme{piecewise smooth}, which holds for almost all level sets if $u$ is
+differentiable. A consideration of exterior normals and perimeters of
+level sets of any function $u \in \BV(\Omega)$ will not be considered
+here, but can be found in for example \fixme{ziemer 5.4.1 and 5.5.1, in
+the non-anisotropic case.}
+
Further note that this is an integral of the anisotropic norm of the
unit normal vector. The length of the boundary would normally be
calculated by integrating the norm of the tangent vector. The connection
integration formula, and discretization, where an approximation of the
perimeter will be computed using a graph cut machinery.
-\fixme{well, if we assumed differentiability, we wouldn't need the sup
-definition of the TV.}
-
\section{Cauchy--Crofton formulas}
\fixme{Rating: 6/10, comment in the beginning that we are actually going
\input{fig/line_param}
\end{figure}
-In the fields of integral theory and geometric measure theory there are
+In the fields of integral geometry and geometric measure theory there are
a number of interesting integral formulas. Several of them fall in a
category often referred to as \emph{Cauchy--Crofton style formulas}, and
give ways to measure geometric objects using the set of all lines in the
plane. The formulas presented here will give a way to measure the length
of a curve by counting the times it intersects line in the set of all
-lines. Intuitively, a long curve will intersect more lines.
+lines.
-We write $\mathcal{L}$ for the set of all straight lines in the plane,
-and parametrize them as shown in Figure~\ref{fig:line_param}. Thus a
+We write $\mathcal{L}$ for the set of all lines in the plane,
+and parametrize them as shown in Figure~\ref{fig:line_param}. A
line is parametrized by the angle $\phi \in [0, 2\pi)$ of the normal going to the
origin, and the distance $\rho \in [0, \infty)$ from origin to the line. Sometimes it is
more convenient to consider a unit vector $\nu$ giving the direction of
-the line instead of the angle parameter $\phi$. We will write a line
+the line instead of the angle parameter $\phi$. We denote a line by
$\ell_{\phi, \rho} = \ell_{\nu, \rho}$ where $\nu$ is a unit vector
along the line, i.e.\ $\nu = (-\sin \phi, \cos \phi)^T$. By defining the
measure on this set $d\mathcal{L} = \dpdr$ we are ready to introduce the
Cauchy--Crofton formula. Note that the measure $d\mathcal{L}$ is
-invariant under rigid motions, meaning combinations of translations and
-rotations.
+invariant under rotations.
\nomenclature{$\mathcal{L}$}{The set of all straight lines in the
plane.}%
\nomenclature{$\ell_{\phi, \rho}$}{A line given by the angle of the
$\ell_{\phi, \rho}$ intersects the curve $C$.
\label{thm:euclidean_cauchy_crofton}
\end{theorem}
+\begin{proof}
+ See \cite[Theorem 3, Section 1-7.]{do1976differential}.
+\end{proof}
This elegant formula is very useful when we later will discretize our
perimeter calculation. The set of lines $\mathcal{L}$ is then discretized
in a reasonable way, and the length of the curve $C$ can be approximated
where our domain is equipped with a metric tensor in each point.
\begin{theorem}[The Riemannian Cauchy--Crofton formula]
Assume that our space $\Omega$ is equipped with a continuous metric
- tensor $M(x)$, whose eigenvalues are bounded $0 < k \leq
+ tensor $M(x)$, whose eigenvalues are bounded by $0 < k \leq
\lambda_2 \leq \lambda_1 \leq K < \infty$ for all $x \in \Omega$.
The Cauchy--Crofton formula for a differentiable curve $C$ of finite
length then becomes
\end{equation}
\label{thm:riemannian_cauchy_crofton}
\end{theorem}
-Before proving this we present an important result from measure theory
-that we will need.
-\begin{theorem}[Lebesgue's Dominated Convergence theorem]
- Let $\{ f_n \}$ be a sequence of real-valued measurable functions on
- a space $S$ with measure $d\mu$ which converges almost
- everywhere to a real-valued measurable function $f$. If there exists
- an integrable function $g$ such that $\abs{f_n} \leq g$ for all $n$,
- then $f$ is integrable and
- \begin{equation}
- \lim_{n \to \infty} \int_S f_n \, d\mu = \int_S f \, d\mu.
- \end{equation}
-\end{theorem}
-For a proof and further background on measure theory and Lebesgue
-integration theory see for example \cite{bartle1995elements}.
\begin{proof}[Proof of the Riemannian Cauchy--Crofton formula]
Assume first that our space is equipped with at constant metric
tensor $M$. The length of our curve using this tensor can be
projects / master / commitdiff