text:
\begin{document}
\date{}
\maketitle

\thispagestyle{empty}

\begin{abstract}
We study nonnegative classical solutions $u$ of the polyharmonic inequality
\[
 -\Delta^mu \ge 0 \quad \text{in}\quad B_1(0) - \{0\} \subset{\bb R}^n.
\]
We give necessary and sufficient conditions on integers $n\ge 2$ and
$m\ge 1$ such that these solutions $u$ satisfy a pointwise a priori
bound as $x\to 0$. In this case we show that the optimal bound for $u$
is
\[
 u(x) = O(\Gamma(x))\quad \text{as}\quad x\to 0
\]
where $\Gamma$ is the fundamental solution of $-\Delta$ in ${\bb R}^n$.
\medskip

\n {\it Keywords:} Polyharmonic inequality, isolated singularity.

\n 2010 Mathematics Subject Classification Codes: 35B09, 35B40,
35B45, 35C15, 35G05, 35R45.
\end{abstract}

\section{Introduction}\label{sec1}

\indent

It is easy to show that there does not exist a pointwise a priori
bound as $x\to 0$ for $C^2$ nonnegative solutions $u(x)$ of
\begin{equation}\label{eq1.1}
 -\Delta u\ge 0 \quad \text{in}\quad B_1(0)-\{0\} \subset {\bb R}^n,
\quad n\ge 2.
\end{equation}
That is, given any continuous function $\psi\colon (0,1)\to
(0,\infty)$ there exists a $C^2$ nonnegative solution $u(x)$ of
\eqref{eq1.1} such that
\[
 u(x)\ne O(\psi(|x|)) \quad \text{as}\quad x\to 0.
\]
The same is true if the inequality in \eqref{eq1.1} is reversed.

In this paper we study $C^{2m}$ nonnegative solutions of the polyharmonic
inequality
\begin{equation}\label{eq1.2}
 -\Delta^m u\ge 0\quad \text{in}\quad B_1(0) - \{0\}\subset {\bb R}^n
\end{equation}
where $n\ge 2$ and $m\ge 1$ are integers. We obtain the following result.

\begin{thm}\label{thm1.1}
  A necessary and sufficient condition on integers $n\ge 2$ and $m\ge
  1$ such that $C^{2m}$ nonnegative solutions $u(x)$ of \eqref{eq1.2}
  satisfy a pointwise a priori bound as $x\to 0$ is that
\begin{equation}\label{eq1.3}
\text{either $m$ is even or $n<2m$.}
\end{equation}
In this case, the optimal bound for $u$ is
\begin{equation}\label{eq1.5}
 u(x) = O(\Gamma_0(x))\quad \text{as}\quad x\to 0,
\end{equation}
where
\begin{equation}\label{eq1.6}
 \Gamma_0(x)= \begin{cases}
              |x|^{2-n}&\text{if $n\ge 3$}\\
\noalign{\medskip}
\log \dfrac5{|x|}&\text{if $n=2$.}
             \end{cases}
\end{equation}
\end{thm}

The $m$-Kelvin transform of a function $u(x)$, $x\in\Omega\subset
{\bb R}^n-\{0\}$, is defined by
\begin{equation}\label{eq1.5.1}
v(y)=|x|^{n-2m}u(x) \qquad \text{where} \quad x=y/|y|^2.
\end{equation}
By direct computation, $v(y)$ satisfies
\begin{equation}\label{eq1.5.2}
\Delta^mv(y)=|x|^{n+2m}\Delta^mu(x).
\end{equation}
See \cite[p.~221]{WX} or \cite[p.~660]{X}. This fact and
Theorem \ref{thm1.1} immediately imply the following result.

\begin{thm}\label{thm1.2}
  A necessary and sufficient condition on integers $n\ge 2$ and $m\ge
  1$ such that $C^{2m}$ nonnegative solutions $v(y)$ of
\[
 -\Delta^m v\ge 0\quad \text{in}\quad {\bb R}^n-B_1(0)
\]
satisfy a pointwise a priori bound as $|y|\to \infty$ is that
\eqref{eq1.3} holds. In this case, the optimal bound
for $v$ is
\begin{equation}\label{eq1.7}
 v(y) = O(\Gamma_\infty(y))\quad \text{as}\quad |y|\to\infty
\end{equation}
where
\begin{equation}\label{eq1.71}
 \Gamma_\infty(y) = \begin{cases}
                     |y|^{2m-2}&\text{if $n\ge 3$}\\
|y|^{2m-2}\log(5|y|)&\text{if $n=2$.}
                    \end{cases}
\end{equation}
\end{thm}

The estimates \eqref{eq1.5} and \eqref{eq1.7} are optimal because
$\Delta^m\Gamma_0=0=\Delta^m\Gamma_\infty$ in ${\bb R}^n-\{0\}$.

The sufficiency of condition \eqref{eq1.3} in Theorem \ref{thm1.1} and
the estimate \eqref{eq1.5} are an immediate consequence of the
following theorem, which gives for $C^{2m}$ nonnegative solutions $u$
of \eqref{eq1.2} one sided estimates for $\Delta^\sigma u$,
$\sigma=0,1,2,\dots, m$, and estimates for $|D^\beta u|$ for certain
multi-indices $\beta$.

\begin{thm}\label{thm1.3}
Let $u(x)$ be a $C^{2m}$ nonnegative solution of
\begin{equation}\label{eq4.1}
 -\Delta^mu\ge 0\quad \text{in}\quad B_2(0) -\{0\}\subset {\bb R}^n,
\end{equation}
where $n\ge 2$ and $m\ge 1$ are integers. Then for each nonnegative
integer $\sigma\le m$ we have
\begin{equation}\label{eq4.2}
(-1)^{m+\sigma} \Delta^\sigma u(x)
\le C\left|\frac{d^{2\sigma}}{d|x|^{2\sigma}} \Gamma_0(|x|)\right|
\quad \text{for}\quad 0<|x|<1
\end{equation}
where $\Gamma_0$ is given by \eqref{eq1.6} and $C$ is a positive
constant independent of $x$.

Moreover, if $n<2m$ and $\beta$ is a multi-index then
\begin{equation}\label{eq4.3}
 |D^\beta u(x)| = O\left(\left|\frac{d^{|\beta|}}{d|x|^{|\beta|}}
\Gamma_0(|x|)\right|\right) \quad \text{as}\quad x\to 0
\end{equation}
for
\begin{equation}\label{neq4.4}
 |\beta|\le \begin{cases}
             2m-n&\text{if $n$ is odd}\\
2m-n-1&\text{if $n$ is even.}
            \end{cases}
\end{equation}
\end{thm}

There is a similar result when the singularity is at infinity.

\begin{thm}\label{thm1.4}
Let $v(y)$ be a $C^{2m}$ nonnegative solution of
\begin{equation}\label{neq4.1}
 -\Delta^mv\ge 0\quad \text{in}\quad {\bb R}^n - B_{1/2}(0),
\end{equation}
where $n\ge 2$ and $m\ge 1$ are integers. Then for each nonnegative
integer $\sigma\le m$ we have
\begin{equation}\label{neq4.2}
(-1)^{m+\sigma} \Delta^\sigma(|y|^{2\sigma-2m}v(y))
\le C \begin{cases}
|y|^{-2}\log 5|y| &\text{if $\sigma=0$ and $n=2$}\\
|y|^{-2}  &\text{if $\sigma\ge 1$ or $n\ge 3$}
\end{cases}
\quad \text{for} \quad |y|>1
\end{equation}
where $C$ is a positive
constant independent of $y$.

Moreover, if $n<2m$ and $\beta$ is a multi-index satisfying
\eqref{neq4.4} then
\begin{equation}\label{neq4.3}
 |D^\beta v(y)| = O\left(\left|\frac{d^{|\beta|}}{d|y|^{|\beta|}}
\Gamma_\infty(|y|)\right|\right) \quad \text{as}\quad |y|\to \infty
\end{equation}
where $\Gamma_\infty$ is given by \eqref{eq1.71}.
\end{thm}

Note that in Theorems \ref{thm1.3} and \ref{thm1.4} we do not require that
$m$ and $n$ satisfy \eqref{eq1.3}.

Inequality \eqref{neq4.2} gives one sided estimates for
$\Delta^\sigma(|y|^{2\sigma-2m}v(y))$. Sometimes one sided estimates
for $\Delta^\sigma v$ also hold. For example, in the important
case $m=2$, $n=2$ or 3, and the singularity is at the infinity, we
have the following corollary of Theorem \ref{thm1.4}.

\begin{cor}\label{cor1.1}
Let $v(y)$ be a $C^4$ nonnegative solution of
\[
-\Delta^2 v \ge 0 \quad \text{in} \quad {\bb R}^n - B_{1/2}(0)
\]
where $n=2$ or $3$. Then
\begin{equation}\label{eq1.14.1}
v(y)=O\left(\Gamma_\infty(|y|)\right) \quad\text{and} \quad
|\nabla v(y)|=O\left(\left|\frac{d}{d|y|}
\Gamma_\infty(|y|)\right|\right) \quad \text{as} \quad |y|\to\infty
\end{equation}
and
\begin{equation}\label{eq1.14.2}
-\Delta v(y)<C\left|\frac{d^2}{d|y|^2}
\Gamma_\infty(|y|)\right|\quad \text{for} \quad |y|>1
\end{equation}
where $\Gamma_\infty$ is given by \eqref{eq1.71} and $C$ is  a
positive constant independent of $y$.
\end{cor}

The proof of Theorem~\ref{thm1.3} relies heavily on a representation
formula for $C^{2m}$ nonnegative solutions $u$ of \eqref{eq1.2}, which
we state and prove in Section~\ref{sec3}. This formula, which is valid
for all integers $n\ge 2$ and $m\ge 1$ and which when $m=1$ is
essentially a result of Brezis and Lions \cite{BL}, may also be useful
for studying nonnegative solutions in a punctured neighborhood of the
origin---or near $x=\infty$ via the $m$-Kelvin transform---of problems of
the form
\begin{equation}\label{eq1.8}
 -\Delta^m u = f(x,u)\quad\text{or}\quad 0\le - \Delta^mu \le f(x,u)
\end{equation}
when $f$ is a nonnegative function and $m$ and $n$ may or may not
satisfy \eqref{eq1.3}. Examples of such problems can
be found in \cite{CMS,CX,GL,H,MR,WX,X} and elsewhere.

Pointwise estimates at $x=\infty$ of solutions $u$ of problems
\eqref{eq1.8} can be crucial for proving existence results for entire
solutions of \eqref{eq1.8} which in turn can be used to obtain, via
scaling methods, existence and estimates of solutions of boundary
value problems associated with \eqref{eq1.8}, see
e.g. \cite{RW1,RW2}. An excellent reference for polyharmonic boundary
value problems is \cite{GGS}.

Lastly, weak solutions of $\Delta^mu = \mu$, where
$\mu$ is a measure on a subset of ${\bb R}^n$, have been studied in
\cite{CDM} and \cite{FKM}, and removable isolated singularities of
$\Delta^mu=0$ have been studied in \cite{H}.

\section{Preliminary results}\label{sec2}

\indent

In this section we state and prove four lemmas. Lemmas~\ref{lem2.1},
\ref{lem2.2}, and \ref{lem2.3} will only be used to prove
Lemma~\ref{lem2.4}, which in turn will be used in Section~\ref{sec3}
to prove Theorem~\ref{thm3.1}.

Lemmas \ref{lem2.1} and \ref{lem2.2} are well-known. We include their
very short proofs for the convenience of the reader.

\begin{lem}\label{lem2.1}
  Let $f\colon (0,r_2]\to [0,\infty)$ be a continuous function where
  $r_2$ is a finite positive constant. Suppose $n\ge 2$ is an integer
  and the equation
\begin{equation}\label{eq2.1}
v'' + \frac{n-1}r v' = -f(r)\qquad 0<r<r_2
\end{equation}
has a nonnegative solution $v(r)$. Then
\begin{equation}\label{eq2.2}
 \int^{r_2}_0 r^{n-1} f(r)\,dr < \infty.
\end{equation}
\end{lem}

\begin{proof}
Let $r_1=r_2/2$. Integrating \eqref{eq2.1} we obtain
\begin{equation}\label{eq2.3}
r^{n-1}v'(r) = r^{n-1}_1 v'(r_1) + \int^{r_1}_r \rho^{n-1}f(\rho)\,d\rho
\quad \text{for}\quad 0<r<r_1.
\end{equation}
Suppose for contradiction that
\[
 r^{n-1}_1v'(r_1) + \int^{r_1}_{r_0} \rho^{n-1}f(\rho)\,d\rho \ge 1
\quad \text{for some} \quad r_0\in (0,r_1).
\]
Then for $0<r<r_0$ we have by \eqref{eq2.3} that
\[
 v(r_0) - v(r) \ge \int^{r_0}_r \rho^{1-n}\,d\rho \to \infty
\quad \text{as}\quad r\to 0^+
\]
which contradicts the nonnegativity of $v(r)$.
\end{proof}

\begin{lem}\label{lem2.2}
  Suppose $f\colon (0,R]\to {\bb R}$ is a continuous function, $n\ge
  2$ is an integer, and
\begin{equation}\label{eq2.4}
\int^R_0 \rho^{n-1}|f(\rho)|\,d\rho < \infty.
\end{equation}
Define $u_0\colon (0,R]\to {\bb R}$ by
\[
 u_0(r)= \begin{cases}
          \dfrac1{n-2} \left[\dfrac1{r^{n-2}}
{\ds\int^r_0} \rho^{n-1}f(\rho)\,d\rho
+ {\ds\int^R_r} \rho f(\rho)\,d\rho\right]&\text{if $n\ge 3$}\\
\noalign{\medskip}
\left(\log \dfrac{2R}r\right) {\ds\int^r_0} \rho f(\rho)\,d\rho
+ {\ds\int^R_r} \rho\left(\log \dfrac{2R}\rho\right) f(\rho)\,d\rho
&\text{if $n=2$}.
         \end{cases}
\]
Then $u = u_0(r)$ is a $C^2$ solution of
\begin{equation}\label{eq2.5}
 -(\Delta u)(r) := -\left(u''(r) + \frac{n-1}r u'(r)\right)
= f(r)\quad \text{for}\quad 0<r\le R.
\end{equation}
Moreover, all solutions $u(r)$ of \eqref{eq2.5} are such that
\begin{equation}\label{eq2.6}
 \int^r_0 \rho^{n-1}|u(\rho)|\,d\rho =
\begin{cases}
O(r^2)&\text{as $r\to 0^+$ if $n\ge 3$}\\
\noalign{\medskip}
O\left(r^2 \log \dfrac1r\right)&\text{as $r\to 0^+$ if $n=2$.}
\end{cases}
\end{equation}
\end{lem}

\begin{proof}
  By \eqref{eq2.4} the formula for $u_0(r)$ makes sense and it is easy
  to check that $u=u_0(r)$ is a solution of \eqref{eq2.5} and, as
  $r\to 0^+$,
\[
 u_0(r) = \begin{cases}
           O(r^{2-n})&\text{if $n\ge 3$}\\
\noalign{\medskip}
O\left(\log \dfrac1r\right)&\text{if $n=2$.}
          \end{cases}
\]
Thus, since all solutions of \eqref{eq2.5} are given by
\[
 u= u_0(r) + C_1+C_2
\begin{cases}
 r^{2-n}&\text{if $n\ge 3$}\\
\noalign{\medskip}
\log \dfrac1r&\text{if $n=2$}
\end{cases}
\]
where $C_1$ and $C_2$ are arbitrary constants, we see that all
solutions of \eqref{eq2.5} satisfy \eqref{eq2.6}.
\end{proof}

\begin{lem}\label{lem2.3}
  Suppose $f\colon (0,R]\to {\bb R}$ is a continuous function, $n\ge
  2$ is an integer, and
\begin{equation}\label{eq2.7}
\intl_{x\in B_R(0)\subset{\bb R}^n} |f(|x|)| \,dx < \infty.
\end{equation}
If $u = u(|x|)$ is a radial solution of
\begin{equation}\label{eq2.8}
 -\Delta^m u = f\quad \text{for}\quad 0<|x|\le R,\quad  m\ge 1
\end{equation}
then
\begin{equation}\label{eq2.9}
\intl_{|x|<r}  |u(x)|\,dx =
\begin{cases}
 O(r^2)&\text{as $r\to 0^+$ if $n\ge 3$}\\
\noalign{\medskip}
O\left(r^2 \log \dfrac1r\right)&\text{as $r\to 0^+$ if $n=2$.}
\end{cases}
\end{equation}
\end{lem}

\begin{proof}
  The lemma is true for $m=1$ by Lemma~\ref{lem2.2}. Assume,
  inductively, that the lemma is true for $m-1$ where $m\ge 2$. Let
  $u$ be a radial solution of \eqref{eq2.8}. Then
\[
 -\Delta(\Delta^{m-1}u) = -\Delta^mu = f\quad \text{for}\quad 0<|x|\le R.
\]
Hence by \eqref{eq2.7} and Lemma \ref{lem2.2},
\[
 g := -\Delta^{m-1}u \in L^1(B_R(0)).
\]
So by the inductive assumption, \eqref{eq2.9} holds.
\end{proof}

\begin{lem}\label{lem2.4}
  Suppose $f\colon \ovl{B_R(0)} - \{0\}\to {\bb R}$ is a nonnegative
  continuous function and $u$ is a $C^{2m}$ solution of
\begin{equation}\label{eq2.10}
 \left.\begin{array}{r} -\Delta^mu=f\\ u\ge 0\end{array}\right\}
\quad \text{in} \quad \ovl{B_R(0)} - \{0\} \subset {\bb R}^n,
\quad n\ge 2,\quad m\ge 1.
\end{equation}
Then
\begin{align}\label{eq2.11}
 &\intl_{|x|<r} u(x)\,dx = \begin{cases}
                          O(r^2)&\text{as $r\to 0^+$ if $n\ge 3$}\\
\noalign{\medskip}
O\left(r^2\log \dfrac1r\right)&\text{as $r\to 0^+$ if $n=2$}\end{cases}\\
\intertext{and}
\label{eq2.12}
&\intl_{|x|<R} |x|^{2m-2} f(x)\,dx < \infty.
\end{align}
\end{lem}

\begin{proof}
  By averaging \eqref{eq2.10} we can assume $f=f(|x|)$ and $u=u(|x|)$
  are radial functions. The lemma is true for $m=1$ by
  Lemmas~\ref{lem2.1} and \ref{lem2.2}. Assume inductively that the
  lemma is true for $m-1$, where $m\ge 2$. Let $u = u(|x|)$ be a
  radial solution of \eqref{eq2.10}. Let $v=\Delta^{m-1}u$. Then
  $-\Delta v = -\Delta^mu=f$ and integrating this equation we obtain
  as in the proof of Lemma~\ref{lem2.1} that
\begin{equation}\label{eq2.13}
 r^{n-1}v'(r) = r^{n-1}_2v'(r_2) + \int^{r_2}_r \rho^{n-1}f(\rho)\,d\rho
\quad \text{for all}\quad 0<r<r_2\le R.
\end{equation}

We can assume
\begin{equation}\label{eq2.14}
 \int^R_0 \rho^{n-1}f(\rho)\,d\rho = \infty
\end{equation}
for otherwise $\intl_{|x|<R} f(x)\,dx < \infty$ and hence
\eqref{eq2.12} obviously holds and \eqref{eq2.11} holds by Lemma
\ref{lem2.3}. By \eqref{eq2.13} and \eqref{eq2.14} we have for some
$r_1\in (0,R)$ that
\begin{equation}\label{eq2.15}
 v'(r_1)\ge 1.
\end{equation}
Replacing $r_2$ with $r_1$ in \eqref{eq2.13} we get
\[
 v'(\rho) = \frac{r^{n-1}_1 v'(r_1)}{\rho^{n-1}}
+ \frac1{\rho^{n-1}} \int^{r_1}_\rho s^{n-1}f(s)\,ds
\quad \text{for}\quad 0<\rho\le r_1
\]
and integrating this equation from $r$ to $r_1$ we obtain for $0<r\le
r_1$ that
\[
 -v(r) = -v(r_1) + r^{n-1}_1v'(r_1) \int^{r_1}_r \frac1{\rho^{n-1}}
 \,d\rho
+ \int^{r_1}_r \frac1{\rho^{n-1}} \int^{r_1}_\rho s^{n-1} f(s)\,ds\,d\rho
\]
and hence by \eqref{eq2.15} for some $r_0\in (0,r_1)$ we have
\[
 -\Delta^{m-1}u(r) = -v(r)
> \int^{r_0}_r \frac1{\rho^{n-1}} \int^{r_0}_\rho s^{n-1}f(s)\,ds \,d\rho
\ge 0\quad \text{for}\quad 0<r\le r_0.
\]
So by the inductive assumption, $u$ satisfies \eqref{eq2.11} and
\begin{align*}
\infty &> \frac1{n\omega_n} \intl_{|x|<r_0} |x|^{2m-4}(-v(|x|))\,dx\\
&= \int^{r_0}_0 r^{2m+n-5} (-v(r))\,dr\\
&\ge \int^{r_0}_0 r^{2m+n-5} \left(\int^{r_0}_r
\frac1{\rho^{n-1}} \int^{r_0}_\rho s^{n-1} f(s)\,ds\,d\rho\right)dr\\
&= C\int^{r_0}_0 s^{2m-2} f(s)s^{n-1}ds\\
&= C\intl_{|x|<r_0} |x|^{2m-2} f(x)\,dx
\end{align*}
where in the above calculation we have interchanged the order of
integration and $C$ is a positive constant which depends only on $m$
and $n$. This completes the inductive proof.
\end{proof}

\section{Representation formula}\label{sec3}

\indent

A fundamental solution of $\Delta^m$ in ${\bb R}^n$, where $n\ge 2$
and $m\ge 1$ are integers, is given by
\begin{numcases}{\Phi(x):=a}
(-1)^m |x|^{2m-n}, & if $2 \le 2m < n$ \label{eq3.1}\\
(-1)^{\frac{n-1}2}|x|^{2m-n}, & if $3\le n < 2m$ and  $n$ is odd \label{eq3.2}\\
(-1)^{\frac{n}2} |x|^{2m-n} \log \frac5{|x|}, & if $2\le n \le 2m$
 and $n$ is even \label{eq3.3}
\end{numcases}
where $a = a(m,n)$ is a \emph{positive} constant. In the sense of
distributions, $\Delta^m\Phi=\delta$, where $\delta$ is the Dirac mass
at the origin in ${\bb R}^n$. For $x\ne 0$ and
$y\ne x$, let
\begin{equation}\label{eq3.4}
 \Psi(x,y) = \Phi(x-y) - \sum_{|\alpha|\le 2m-3}
\frac{(-y)^\alpha}{\alpha!} D^\alpha\Phi(x)
\end{equation}
be the error in approximating $\Phi(x-y)$ with the partial sum of
degree $2m-3$ of the Taylor series of $\Phi$ at $x$.

The following theorem gives representation formula \eqref{eq3.6} for
nonnegative solutions of inequality \eqref{eq3.5}.

\begin{thm}\label{thm3.1}
Let $u(x)$ be a $C^{2m}$ nonnegative solution of
\begin{equation}\label{eq3.5}
 -\Delta^mu \ge 0\quad \text{in}\quad B_2(0)-\{0\}\subset {\bb R}^n,
\end{equation}
where $n\ge 2$ and $m\ge 1$ are integers. Then
\begin{equation}\label{eq3.6}
 u = N+h+ \sum_{|\alpha|\le 2m-2} a_\alpha D^\alpha\Phi\quad
\text{ in}\quad B_1(0)-\{0\}
\end{equation}
where $a_\alpha, |\alpha|\le 2m-2$, are constants, $h\in
C^\infty(B_1(0))$ is a solution of
\[
 \Delta^mh = 0\quad \text{in}\quad B_1(0),
\]
and
\begin{equation}\label{eq3.7}
 N(x) = \intl_{|y|\le 1} \Psi(x,y) \Delta^mu(y)\,dy\quad \text{for}\quad x\ne 0.
\end{equation}
\end{thm}

When $m=1$, equation \eqref{eq3.6} becomes
\[
u = N+h+a_0\Phi_1 \quad \text{in} \quad B_1(0)-\{0\},
\]
where
\[
 N(x)= \intl_{|y|<1} \Phi_1(x-y) \Delta u(y)\,dy
\]
and $\Phi_1$ is the fundamental solution of the Laplacian in ${\bb
  R}^n$. Thus, when $m=1$, Theorem~\ref{thm3.1} is essentially a
result of Brezis and Lions \cite{BL}.

Futamura, Kishi, and Mizuta \cite[Theorem 1]{FKM} and \cite[Corollary
5.1]{FM} obtained a result very similar to our Theorem~\ref{thm3.1},
but using their result we would have to let the index of summation
$\alpha$ in \eqref{eq3.4} range over the larger set $|\alpha|\le
2m-2$. This would not suffice for our proof of
Theorem~\ref{thm1.1}. We have however used their idea of using the
remainder term $\Psi(x,y)$ instead of $\Phi(x-y)$ in
\eqref{eq3.7}. This is done so that the integral in \eqref{eq3.7} is
finite. See also the book \cite[p. 137]{HK}.

\begin{proof}[Proof of Theorem \ref{thm3.1}]
By \eqref{eq3.5},
\begin{equation}\label{eq3.8}
f := -\Delta^mu \ge 0\quad \text{in}\quad B_2(0)-\{0\}.
\end{equation}
Thus by Lemma \ref{lem2.4},
\begin{equation}\label{eq3.9}
 \intl_{|x|<1} |x|^{2m-2} f(x)\,dx < \infty
\end{equation}
and
\begin{equation}\label{eq3.10}
 \intl_{|x|<r} u(x)\,dx = O\left(r^2\log \frac1r\right)
\quad \text{as}\quad r\to 0^+.
\end{equation}

If $|\alpha| = 2m-2$ we claim
\begin{equation}\label{eq3.11}
D^\alpha \Phi(x) = O(\Gamma_0(x))\quad \text{as}\quad x\to 0
\end{equation}
where $\Gamma_0(x)$ is given by \eqref{eq1.6}. This is clearly true if
$\Phi$ is given by \eqref{eq3.1} or \eqref{eq3.2} because then $n\ge
3$ and $\Gamma_0(x)=|x|^{2-n}$. The estimate \eqref{eq3.11} is also
true when $\Phi$ is given by \eqref{eq3.3} because then $|x|^{2m-n}$
is a \emph{polynomial} of degree $2m-n\le 2m-2=|\alpha|$ with equality
if and only if $n=2$, and hence $D^\alpha\Phi$ has a term with $\log
\frac5{|x|}$ as a factor if and only if $n=2$. This proves
\eqref{eq3.11}.

By Taylor's theorem and \eqref{eq3.11} we have
\begin{align}\label{eq3.12}
 |\Psi(x,y)| &\le C|y|^{2m-2} \Gamma_0(x)\\
&\le C|y|^{2m-2} |x|^{2-n} \log \frac5{|x|} \quad
\text{for}\quad |y| < \frac{|x|}2<1.\notag
\end{align}

Differentiating \eqref{eq3.4} with respect to $x$ we get
\begin{equation}\label{eq3.13}
 D^\beta_x(\Psi(x,y)) = (D^\beta\Phi)(x-y)
-  \sum_{|\alpha|\le 2m-3} \frac{(-y)^\alpha}{\alpha!}
(D^{\alpha+\beta}\Phi)(x)\quad \text{for}\quad x\ne 0
\quad \text{and}\quad y\ne x
\end{equation}
and so by Taylor's theorem applied to $D^\beta\Phi$ we have
\begin{equation}\label{eq3.14}
 |D^\beta_x\Psi(x,y)| \le C|y|^{2m-2} |x|^{2-n-|\beta|}
\log \frac5{|x|}\quad \text{for}\quad |y| < \frac{|x|}2 <1.
\end{equation}
Also,
\begin{equation}\label{eq3.15}
 \Delta^m_x\Psi(x,y) = 0 = \Delta^m_y\Psi(x,y)\quad \text{for}
\quad x\ne 0\quad \text{and}\quad y\ne x
\end{equation}
(see also \cite[Lemma 4.1, p. 137]{HK}) and
\begin{align}
 \intl_{|x|<r} |\Phi(x-y)|\,dx &\le Cr^{2m}\log\frac{5}{r}\notag\\
&\le C|y|^{2m-2} r^2\log \frac5r
\quad \text{for} \quad 0 < r \le 2|y| < 2.
\label{eq3.16}
\end{align}
Before continuing with the proof of Theorem \ref{thm3.1}, we state and
prove the following lemma.

\begin{lem}\label{lem3.1}
For $|y|<1$ and $0<r<1$ we have
\begin{equation}\label{eq3.17}
 \intl_{|x|<r} |\Psi(x,y)| \,dx \le C|y|^{2m-2} r^2\log \frac5r.
\end{equation}
\end{lem}

\begin{proof}
Since $\Psi(x,0)\equiv 0$ for $x\ne 0$, we can assume $y\ne 0$.\medskip

\n {\bf Case I.} Suppose $0<r\le |y| <1$. Then by \eqref{eq3.16}
\begin{align*}
\intl_{0<|x|<r} |\Psi(x,y)|\,dx &\le \intl_{0<|x|<r} |\Phi(x-y)|\,dx
+ \sum_{|\alpha|\le 2m-3} |y|^{|\alpha|} \intl_{0<|x|<r} |D^\alpha\Phi(x)|\,dx\\
&\le C\left[|y|^{2m-2} r^2 \log \frac5r
+ \sum_{|\alpha|<2m-3} |y|^{|\alpha|} r^{2m-|\alpha|} \log \frac5r\right]\\
&\le C |y|^{2m-2} r^2 \log \frac5r.
\end{align*}

\n {\bf Case II.} Suppose $0<|y|<r<1$. Then by \eqref{eq3.16}, with
$r=2|y|$, and \eqref{eq3.12} we have
\begin{align*}
\intl_{|x|<2r} |\Psi(x,y)|\,dx &= \intl_{2|y|<|x|<2r} |\Psi(x,y)|\,dx
+ \intl_{|x|<2|y|} |\Psi(x,y)|\,dx\\
&\le C\left[\, \intl_{2|y|<|x|<2r} |y|^{2m-2} |x|^{2-n}
\log \frac5{|x|} \,dx + |y|^{2m} \log \frac5{|y|}\right.\\
&\quad \left. + \sum_{|\alpha|\le 2m-3} |y|^{|\alpha|} \intl_{|x|<2|y|}
|D^\alpha\Phi(x)|\,dx\right]\\
&\le C\left[|y|^{2m-2} r^2 \log \frac5r
+ |y|^{2m-2} |y|^2 \log \frac5{|y|}\right]\\
&\le C |y|^{2m-2} r^2 \log \frac5r
\end{align*}
which proves the lemma.
\end{proof}

Continuing with the proof of Theorem \ref{thm3.1},
let $N$ be defined by \eqref{eq3.7} and let $2r\in (0,1)$ be
fixed. Then for $2r<|x|<1$ we have
\begin{align*}
 N(x) &= \intl_{r<|y|<1} \left[\Phi (y-x) - \sum_{|\alpha|\le 2m-3}
\frac{(-y)^\alpha}{\alpha!} D^\alpha\Phi(x)\right] \Delta^m u(y)\,dy\\
&\quad -\intl_{0<|y|<r} \Psi(x,y) f(y)\,dy.
\end{align*}
By \eqref{eq3.9} and \eqref{eq3.14}, we can move
differentiation of the second integral with respect to $x$ under the
integral. Hence by \eqref{eq3.15},
\begin{equation}\label{eq3.18}
 \Delta^m N = \Delta^m u
\end{equation}
for $2r< |x|<1$ and since $2r\in (0,1)$ was arbitrary, \eqref{eq3.18}
holds for $0<|x|<1$.

By \eqref{eq3.7}, \eqref{eq3.8}, and Lemma \ref{lem3.1}, for $0<r<1$ we have
\begin{align*}
 \intl_{|x|<r} |N(x)|\,dx &\le \intl_{|y|<1}
\left(\, \intl_{|x|<r} |\Psi(x,y)|\,dx\right) f(y)\,dy\\
&\le Cr^2 \log \frac5r \intl_{|y|<1} |y|^{2m-2} f(y)\,dy\\
&= O\left(r^2 \log \frac1r\right) \quad \text{as}\quad r\to 0^+
\end{align*}
by \eqref{eq3.9}. Thus by \eqref{eq3.10}
\begin{equation}\label{eq3.19}
 v := u-N \in L^1_{\text{loc}}(B_1(0)) \subset {\cl D}'(B_1(0))
\end{equation}
and
\begin{equation}\label{eq3.20}
 \intl_{|x|<r} |v(x)|\,dx = O\left(r^2\log \frac1r\right) \quad
\text{as}\quad r\to 0^+.
\end{equation}
By \eqref{eq3.18},
\[
 \Delta^mv(x) = 0\quad \text{for}\quad 0<|x|<1.
\]
Thus $\Delta^mv$ is a distribution in ${\cl D}'(B_1(0))$ whose support
is a subset of $\{0\}$. Hence
\[
 \Delta^mv = \sum_{|\alpha|\le k} a_\alpha D^\alpha\delta
\]
is a finite linear combination of the delta function and its derivatives.

We now use a method of Brezis and Lions \cite{BL} to show $a_\alpha=0$ for
$|\alpha|\ge 2m-1$. Choose $\varphi\in C^\infty_0(B_1(0))$ such that
\[
(-1)^{|\alpha|}(D^\alpha\varphi)(0)=a_\alpha\quad \text{for}\quad  |\alpha|\le k.
\]
Let $\varphi_\vp(x) = \varphi\big(\frac{x}\vp\big)$. Then, for
$0<\vp<1$, $\varphi_\vp\in C^\infty_0(B_1(0))$ and
\begin{align*}
 \int v\Delta^m\varphi_\vp &= (\Delta^mv)(\varphi_\vp)
= \sum_{|\alpha|\le k} a_\alpha(D^\alpha\delta)\varphi_\vp\\
&= \sum_{|\alpha|\le k} a_\alpha(-1)^{|\alpha|}
\delta(D^\alpha\varphi_\vp)
= \sum_{|\alpha|\le k} a_\alpha(-1)^{|\alpha|} (D^\alpha\varphi_\vp)(0)\\
&= \sum_{|\alpha|\le k} a_\alpha(-1)^{|\alpha|} \frac1{\vp^{|\alpha|}}
(D^\alpha\varphi)(0) = \sum_{|\alpha|\le k} a^2_\alpha \frac1{\vp^{|\alpha|}}.
\end{align*}

On the other hand,
\begin{align*}
 \int v\Delta^m \varphi_\vp &= \int v(x) \frac1{\vp^{2m}}
(\Delta^m\varphi) \left(\frac{x}\vp\right) \,dx\\
&\le \frac{C}{\vp^{2m}} \intl_{|x|<\vp} |v(x)|\,dx
= O\left(\frac1{\vp^{2m-2}} \log \frac1\vp\right) \quad
\text{as}\quad \vp\to 0^+
\end{align*}
by \eqref{eq3.20}. Hence $a_\alpha = 0$ for $|\alpha|\ge 2m-1$ and consequently
\[
 \Delta^mv = \sum_{|\alpha|\le 2m-2} a_\alpha D^\alpha\delta
= \sum_{|\alpha|\le 2m-2} a_\alpha D^\alpha \Delta^m\Phi.
\]
That is
\[
 \Delta^m \left(v-\sum_{|\alpha|\le 2m-2} a_\alpha D^\alpha\Phi\right)
= 0 \quad \text{in}\quad {\cl D}'(B_1(0)).
\]
Thus for some $C^\infty$ solution of $\Delta^mh = 0$ in $B_1(0)$ we have
\[
 v = \sum_{|\alpha|\le 2m-2} a_\alpha D^\alpha \Phi
+ h\quad \text{in}\quad B_1(0) - \{0\}.
\]
Hence Theorem \ref{thm3.1} follows from \eqref{eq3.19}.
\end{proof}

\section{Proofs of Theorems \ref{thm1.3} and \ref{thm1.4} and
Corollary \ref{cor1.1}}
\label{sec4}

\indent

In this section we prove Theorems \ref{thm1.3} and \ref{thm1.4} and
Corollary \ref{cor1.1}.

\begin{proof}[Proof of Theorem \ref{thm1.3}]
This proof is a continuation of the proof of Theorem~\ref{thm3.1}.
If $m=1$ then Theorem~\ref{thm1.3} is trivially true. Hence we can
assume $m\ge 2$. Also, if $\sigma=m$ then \eqref{eq4.2} follows
trivially from \eqref{eq4.1}. Hence we can assume $\sigma\le m-1$ in
\eqref{eq4.2}.

If $\alpha$ and $\beta$ are multi-indices and $|\alpha|= 2m-2$ then it
follows from \eqref{eq3.1}--\eqref{eq3.3} that
\begin{equation}\label{eq4.4}
 D^{\alpha+\beta}\Phi(x) =
 O\left(\left|\frac{d^{|\beta|}}{d|x|^{|\beta|}}
\Gamma_0(|x|)\right|\right) \quad \text{as}\quad x\to 0.
\end{equation}
(This is clearly true if $n=2$. If $n\ge 3$ then $|\alpha+\beta| =
2m-2+|\beta| > 2m-n$ and thus
\[
D^{\alpha+\beta} \Phi(x) = O(|x|^{2m-n-(2m-2+|\beta|)})
= O\left(\left|\frac{d^{|\beta|}}{d|x|^{|\beta|}}
\Gamma_0(|x|)\right|\right).)
\]
Let $L^b$ be any linear partial differential operator of the form
$\sum\limits_{|\beta|=b} c_\beta D^\beta$, where $b$ is a nonnegative
integer and $c_\beta\in {\bb R}$. Then applying Taylor's theorem to
\eqref{eq3.13} and using \eqref{eq4.4} we obtain
\begin{equation}\label{eq4.5}
 |L^b_x\Psi(x,y)|\le C|y|^{2m-2} \left|\frac{d^b}{d|x|^b}
\Gamma_0(|x|)\right| \quad \text{for}\quad |y|< \frac{|x|}2<1.
\end{equation}
Here and later $C$ is a positive constant, independent of $x$ and $y$,
whose value may change from line to line. For $0\le b\le 2m-1$ we have
\[
 L^bN(x)=\int\limits_{|y|<1} -L^b_x \Psi(x,y) f(y)\,dy\quad
\text{for}\quad 0<|x|<1.
\]
Hence by \eqref{eq4.4}, \eqref{eq4.5}, \eqref{eq3.6} and \eqref{eq3.9} we have
\begin{equation}\label{eq4.6}
 L^bu(x) \le C\left|\frac{d^b}{d|x|^b}
\Gamma_0(|x|)\right|\quad \text{for}\quad 0<|x|<1
\end{equation}
provided $0\le b\le 2m-1$ and
\begin{equation}\label{eq4.7}
 -L^b_x\Psi(x,y) \le C|y|^{2m-2} \left|\frac{d^b}{d|x|^b}
\Gamma_0(|x|)\right|\quad \text{for}\quad 0<\frac{|x|}2 < |y|<1.
\end{equation}
We will complete the proof of Theorem~\ref{thm1.3} by proving
\eqref{eq4.7} for various choices for $L^b$. For the rest of the proof
of Theorem~\ref{thm1.3} we will always assume
\begin{equation}\label{eq4.8}
 0 < \frac{|x|}2 < |y|<1
\end{equation}
which implies
\begin{equation}\label{eq4.9}
 |x-y| \le |x|+|y| \le 3|y|.
\end{equation}

\n {\bf Case I.} Suppose $\Phi$ is given by \eqref{eq3.1} or
\eqref{eq3.2}. It follows from \eqref{eq3.13} and \eqref{eq4.8} that
\begin{align*}
 |D^\beta_x\Psi(x,y) - D^\beta_x\Phi(x-y)| &\le
C\sum_{|\alpha|\le 2m-3}
|y|^{|\alpha|} |x|^{2m-n-|\alpha|-|\beta|}\\
&\le C|y|^{2m-2} |x|^{2-n-|\beta|}.
\end{align*}
Thus \eqref{eq4.7}, and hence \eqref{eq4.6}, holds provided $0\le b\le
2m-1$ and
\begin{equation}\label{eq4.10}
-(L^b\Phi)(x-y) \le C|y|^{2m-2} |x|^{2-n-b}.
\end{equation}

\n {\bf Case I(a).} Suppose $\Phi$ is given by \eqref{eq3.1}. Let
$\sigma\in [0,m-1]$ be an integer, $b=2\sigma$, and
$L^b=(-1)^{m+\sigma}\Delta^\sigma$. Then $0 \le b\le 2m-2$ and
\[
\text{sgn}(-L^b\Phi) = (-1)^{1+m+\sigma} \text{ sgn }
\Delta^\sigma\Phi = (-1)^{1+2m+\sigma} \text{ sgn }
\Delta^\sigma|x|^{2m-n} = (-1)^{1+2m+2\sigma}=-1.
\]
Thus \eqref{eq4.10}, and hence \eqref{eq4.6} holds with
$L^b=(-1)^{m+\sigma}\Delta^\sigma$ and $0\le \sigma \le m-1$. This
completes the proof of Theorem~\ref{thm1.3} when $\Phi$ is given
by \eqref{eq3.1}.\medskip

\n {\bf Case I(b).} Suppose $\Phi$ is given by \eqref{eq3.2}. Then $n$
is odd. It follows from \eqref{eq4.8} and \eqref{eq4.9} that for $0\le
|\beta|\le 2m-n$ we have
\[
 |(D^\beta\Phi)(x-y)| \le C|x-y|^{2m-n-|\beta|} \le
 C|y|^{2m-n-|\beta|}
\le C|y|^{2m-2} |x|^{2-n-|\beta|}.
\]
So \eqref{eq4.10} holds with $L^b = \pm D^\beta$ and $|\beta|=b$. Hence
\[
 |D^\beta u(x)| \le C|x|^{2-n-|\beta|} \quad \text{for}\quad 0
\le |\beta|\le 2m-n\quad \text{and} \quad 0<|x|<1.
\]
In particular
\[
 |\Delta^\sigma u(x)|\le C|x|^{2-n-2\sigma} \quad \text{for}
\quad 2\sigma \le 2m-n\quad \text{and}\quad 0<|x|<1.
\]
Also, if $2m-n+1 \le 2\sigma \le 2m-2$, $b=2\sigma$, and $L^b =
(-1)^{m+\sigma}\Delta^\sigma$, then $0 \le \sigma\le m-1$ and
\begin{align*}
 \text{sgn} (-L^b\Phi) &= (-1)^{m+\sigma+1} \text{ sgn }
\Delta^\sigma\Phi = (-1)^{m+\sigma+1+\frac{n-1}2} \text{ sgn }
\Delta^\sigma |x|^{2m-n}\\
&= (-1)^{m+\sigma+1+\frac{n-1}2} \text{ sgn}
(\Delta^{\frac{b-(2m-n+1)}2}
\Delta^{\frac{2m-n+1}2} |x|^{2m-n})\\
&= (-1)^{m+\sigma+1+\frac{n-1}2 +\sigma-m+\frac{n-1}2} = -1
\end{align*}
because $\Delta^{\frac{2m-n+1}2} |x|^{2m-n} = C|x|^{-1}$ where $C>0$.

So \eqref{eq4.10} holds with $L^b =
(-1)^{m+\sigma}\Delta^\sigma$. Hence $(-1)^{m+\sigma} \Delta^\sigma
u(x) \le C|x|^{2-n-2\sigma}$ for $0 \le \sigma\le m-1$ and
$0<|x|<1$. This completes the proof Theorem~\ref{thm1.3} when $\Phi$
is given by \eqref{eq3.2}.\medskip

\n {\bf Case II.} Suppose $\Phi$ is given by \eqref{eq3.3}. Then $2\le
n \le 2m$ and $n$ is even. To prove Theorem~\ref{thm1.3} in Case~II,
it suffices to prove the following three statements.
\begin{itemize}
 \item[(i)] Estimate \eqref{eq4.3} holds when $n=2$, $\beta=0$, and $m\ge 2$.
\item[(ii)] Estimate \eqref{eq4.3} holds when $|\beta|\le 2m-n-1$
            and either $n\ge 3$ or $|\beta|\ge 1$.
\item[(iii)] Estimate \eqref{eq4.2} holds for $2m-n\le 2\sigma\le 2m-2$.
\end{itemize}
\medskip

\noindent {\it Proof of (i).}
Suppose $n=2$, $\beta=0$, and $m \ge 2$. Then, since $u$ is
nonnegative, to prove (i) it suffices to prove
\[
 u(x) \le C \log \frac5{|x|}\quad \text{for}\quad 0<|x|<1
\]
which holds if \eqref{eq4.7} holds with $b=0$ and $L^b=D^0 =$ id. That
is if
\begin{equation}\label{eq4.11}
-\Psi(x,y) \le C|y|^{2m-2} \log \frac5{|x|}
\end{equation}
By \eqref{eq3.4}, \eqref{eq4.8}, and \eqref{eq4.9} we have
\begin{align*}
 |\Psi(x,y) - \Phi(x-y)| &\le \sum_{|\alpha|\le 2m-3} |y|^{|\alpha|}
|D^\alpha\Phi(x)|\\
&\le C \sum_{|\alpha|\le 2m-3} |y|^{|\alpha|} |x|^{2m-2-|\alpha|}
\log \frac5{|x|} \le C |y|^{2m-2} \log \frac5{|x|}
\end{align*}
and
\begin{align*}
 |\Phi(x-y)| &= a|x-y|^{2m-2} \log \frac5{|x-y|}\\
&\le C|y|^{2m-2} \log \frac5{|y|} \le C|y|^{2m-2} \log \frac5{|x|}
\end{align*}
which imply \eqref{eq4.11}. This completes the proof of (i).
\medskip

\noindent {\it Proof of (ii).}
Suppose $|\beta|\le 2m-n-1$ and either $n\ge 3$ or $|\beta|\ge
  1$. Then $n+|\beta|\ge 3$ and in
order to prove (ii) it suffices to prove
\begin{equation}\label{eq4.12}
 |D^\beta_x\Psi(x,y)|\le C|y|^{2m-2}
\left|\frac{d^{|\beta|}}{d|x|^{|\beta|}} \Gamma_0(|x|)\right|
\end{equation}
because then \eqref{eq4.7}, and hence \eqref{eq4.6}, holds with
$L^b=\pm D^\beta$.

Since $\Phi$ is given by \eqref{eq3.3} we have $n\ge 2$ is even and
\[
 \Phi(x) = P(x) \log \frac5{|x|}
\]
where $P(x) = a(-1)^{\frac{n}2} |x|^{2m-n}$ is a \emph{polynomial} of
degree $2m-n$. Since $D^\beta P$ is a polynomial of degree
$2m-n-|\beta|\le 2m-3$ we have
\begin{equation}\label{eq4.13}
 D^\beta_xP(x-y) = \sum_{|\alpha|\le 2m-3}
\frac{(-y)^\alpha}{\alpha!} D^{\alpha+\beta}P(x).
\end{equation}

Since $D^\beta_x\Psi(x,y) = A_1+A_2+A_3$, where
\begin{align*}
 A_1 &= D^\beta_x\Psi(x,y) - D^\beta_x\Phi(x-y) + (D^\beta_xP(x-y))
\log \frac5{|x|}\\
A_2 &= D^\beta_x\Phi(x-y) - (D^\beta_xP(x-y)) \log \frac5{|x-y|}\\
A_3 &= (D^\beta_xP(x-y)) \log \frac{|x|}{|x-y|},
\end{align*}
to prove \eqref{eq4.12} it suffices to prove for $j=1,2,3$ that
\begin{equation}\label{eq4.14}
 |A_j| \le C|y|^{2m-2} \left|\frac{d^{|\beta|}}{d|x|^{|\beta|}}
\Gamma_0(|x|)\right|.
\end{equation}

Since
\begin{align*}
 \left|D^{\alpha+\beta}\Phi(x) - (D^{\alpha+\beta}P(x))
\log \frac5{|x|}\right| &= \left|
\sum_{\underset{\scriptstyle |\alpha+\beta-\gamma|\ge 1}{\gamma\le
    \alpha+\beta}}
\binom{\alpha+\beta}\gamma (D^\gamma P(x))
\left(D^{\alpha+\beta-\gamma} \log \frac5{|x|}\right)\right|\\
&\le C |x|^{2m-n-|\alpha|-|\beta|}
\end{align*}
it follows from \eqref{eq3.13}, \eqref{eq4.13}, and \eqref{eq4.8} that
\begin{align*}
 |A_1| = |-A_1| &= \left|\sum_{|\alpha|\le 2m-3}
\frac{(-y)^\alpha}{\alpha!} D^{\alpha+\beta} \Phi(x)
- \sum_{|\alpha|\le 2m-3} \frac{(-y)^\alpha}{\alpha!}
(D^{\alpha+\beta} P(x)) \log \frac5{|x|}\right|\\
&\le C \sum_{|\alpha|\le 2m-3} |y|^{|\alpha|}
|x|^{2m-n-|\alpha|-|\beta|}
\le C |y|^{2m-2} |x|^{2-n-|\beta|}\\
&= C|y|^{2m-2} \left|\frac{d^{|\beta|}}{d|x|^{|\beta|}} \Gamma_0(|x|)\right|.
\end{align*}
Thus \eqref{eq4.14} hold when $j=1$.

Since $A_2=0$ when $\beta=0$, we can assume for the proof of
\eqref{eq4.14} when $j=2$ that $|\beta|\ge 1$. Then by \eqref{eq4.9}
and \eqref{eq4.8},
\begin{align*}
 |A_2| &= \left|\sum_{\underset{\scriptstyle |\beta-\alpha|\ge 1}{\alpha\le \beta}}
\binom\beta\alpha (D^\alpha_xP(x-y)) \left(D^{\beta-\alpha}_x
\log \frac5{|x-y|}\right)\right|\\
&\le C|x-y|^{2m-n-|\beta|} \le C|y|^{2m-n-|\beta|}\\
&\le C |y|^{2m-2} |x|^{2-n-|\beta|}\\
&= C|y|^{2m-2} \left|\frac{d^{|\beta|}}{d|x|^{|\beta|}} \Gamma_0(|x|)\right|.
\end{align*}
Thus \eqref{eq4.14} holds when $j=2$.

Finally we prove \eqref{eq4.14} when $j=3$. Let $d=2m-n-|\beta|$. Then
$1\le d\le 2m-3$,
\[
 |A_3| \le C|x-y|^d \left|\log \frac{|x|}{|x-y|}\right|
\]
and by \eqref{eq4.8} and \eqref{eq4.9} we have
\begin{align*}
 |x-y|^d \left|\log \frac{|x|}{|x-y|}\right| &\le
\begin{cases}
 |x-y|^d \left(\dfrac{|x|}{|x-y|}\right)^d
= |x|^d \le C|y|^{2m-2} |x|^{2-n-|\beta|} &\text{if $|x-y|\le |x|$}\\
|x-y|^d \left(\dfrac{|x-y|}{|x|}\right)^{2m-2-d}
= |x-y|^{2m-2} |x|^{2-n-|\beta|} &\text{if $|x|\le |x-y|$}
\end{cases}\\
&\le C|y|^{2m-2} |x|^{2-n-|\beta|}
= C|y|^{2m-2} \left|\frac{d^{|\beta|}}{d|x|^{|\beta|}} \Gamma_0(|x|)\right|.
\end{align*}
Thus \eqref{eq4.14} holds when $j=3$. This completes the proof of
\eqref{eq4.12} and hence of (ii).
\medskip

\noindent {\it Proof of (iii).}
Suppose $2m-n\le 2\sigma \le 2m-2$. In order to prove (iii) it suffices to prove
\begin{equation}\label{eq4.15}
 (-1)^{m+\sigma+1} \Delta^\sigma_x\Psi(x,y) \le C|y|^{2m-2}
\left|\frac{d^{2\sigma}}{d|x|^{2\sigma}} \Gamma_0(|x|)\right|
\end{equation}
because then \eqref{eq4.7}, and hence \eqref{eq4.6}, holds with
$L^b=(-1)^{m+\sigma}\Delta^\sigma$ and $b=2\sigma$.

If $|\beta|=2\sigma$ then \eqref{eq4.8} implies
\begin{align*}
\left|\sum_{1\le |\alpha| \le 2m-3} \frac{(-y)^\alpha}{\alpha!}
D^{\alpha+\beta} \Phi(x)\right| &\le C \sum_{1\le |\alpha|\le 2m-3}
|y|^{|\alpha|} |x|^{2m-n-|\alpha|-|\beta|}\\
&\le C|y|^{2m-2} |x|^{2-n-|\beta|}.
\end{align*}
Thus it follows from \eqref{eq3.13} that
\[
 |\Delta^\sigma_x\Psi(x,y) - \Delta^\sigma_x\Phi(x-y)
+ \Delta^\sigma\Phi(x)|\le C|y|^{2m-2} |x|^{2-n-2\sigma}.
\]
Hence to prove \eqref{eq4.15} it suffices to prove
\begin{equation}\label{eq4.16}
 (-1)^{m+\sigma+1} (\Delta^\sigma_x \Phi(x-y) - \Delta^\sigma\Phi(x))
\le C|y|^{2m-2} |x|^{2-n-2\sigma}.
\end{equation}
We divide the proof of \eqref{eq4.16} into cases.\medskip

\n {\bf Case 1.} Suppose $2\le 2m-n+2\le 2\sigma\le 2m-2$. Then by \eqref{eq4.8}
\[
 |\Delta^\sigma\Phi(x)| \le C|x|^{2m-n-2\sigma} \le C|y|^{2m-2} |x|^{2-n-2\sigma}
\]
and since
\begin{equation}\label{eq4.17}
 \Delta^{\frac{2m-n}2} \left(|x|^{2m-n} \log \frac5{|x|}\right)
= A \log \frac5{|x|}-B
\end{equation}
where $A>0$ and $B\ge 0$ are constants, we have
\[
 \text{sgn}((-1)^{m+\sigma+1} \Delta^\sigma\Phi(z))
= (-1)^{m+\sigma+\frac{n}2+1} (-1)^{\sigma - \frac{2m-n}2}
= -1 \quad \text{for}\quad |z|>0.
\]
This proves \eqref{eq4.16} and hence (iii) in Case 1.
\medskip

\n {\bf Case 2.} Suppose $2\sigma =2m-n$. Then by \eqref{eq4.17} and
\eqref{eq4.9} we have
\begin{align*}
 (-1)^{m+\sigma+1} (\Delta^\sigma_x\Phi(x-y) - \Delta^\sigma\Phi(x))
&= (-1)^{\frac{n}2 +m+\sigma+1} A \log \frac{|x|}{|x-y|}\\
&= A\log \frac{|x-y|}{|x|} \le A \log \frac{3|y|}{|x|}
\le A \left(\frac{3|y|}{|x|}\right)^{2m-2}\\
&= A 3^{2m-2} |y|^{2m-2} |x|^{2-n-2\sigma}.
\end{align*}
This proves \eqref{eq4.16} and hence (iii) in Case 2, and thereby
completes the proof of Theorem~\ref{thm1.3}.
\end{proof}

\begin{proof}[Proof of Theorem \ref{thm1.4}]
Let $u(x)$ be defined in terms of $v(y)$ by \eqref{eq1.5.1}. Then by
\eqref{eq1.5.2} and \eqref{neq4.1}, $u(x)$ is a $C^{2m}$ nonnegative
solution of \eqref{eq4.1}, and hence $u(x)$ satisfies the conclusion
of Theorem \ref{thm1.3}. It is a straight-forward exercise to show
that \eqref{neq4.3} follows from \eqref{eq4.3} when $n<2m$ and $\beta$
satisfies \eqref{neq4.4}. So to complete the proof of Theorem
\ref{thm1.4} we will now prove \eqref{neq4.2}.

Suppose $\sigma\le m$ is a nonnegative integer. Let $v_\sigma(y)$ be
the $\sigma$-Kelvin transform of $u(x)$. Then
$v_\sigma(y)=|y|^{2\sigma-2m}v(y)$ and thus by \eqref{eq4.2}, we have
for $|y|>1$ that
\begin{align*}
(-1)^{m+\sigma}\Delta^\sigma(|y|^{2\sigma-2m}v(y))
&=(-1)^{m+\sigma}\Delta^\sigma v_\sigma(y)\\
&=(-1)^{m+\sigma}|x|^{n+2\sigma}\Delta^\sigma u(x)\\
&\le C|x|^{n+2\sigma} \left|\frac{d^{2\sigma}}{d|x|^{2\sigma}}
\Gamma_0(|x|)\right|\\
&\le C\begin{cases}
|x|^2\log\frac{5}{|x|}
&\text{if $\sigma=0$ and $n=2$}\\
|x|^2
&\text{if $\sigma\ge 1$ or $n\ge 3$}
\end{cases}
\end{align*}
which implies \eqref{neq4.2} after replacing $|x|$ with $1/|y|$.
\end{proof}

\begin{proof}[Proof of Corollary \ref{cor1.1}]
Theorem \ref{thm1.4} implies \eqref{eq1.14.1} and
\[
-\Delta(|y|^{-2}v(y))\le C|y|^{-2} \qquad \text{for} \quad |y|>1
\]
and thus for $|y|>1$ we have
\begin{align*}
-|y|^{-2}\Delta v(y)&=-\Delta(|y|^{-2} v(y))+(\Delta|y|^{-2})v(y)
+ 2\nabla|y|^{-2}\cdot\nabla v(y)\\
&\le -\Delta(|y|^{-2} v(y))+C\left(|y|^{-4}\Gamma_\infty(|y|)+|y|^{-3}
\frac{d}{d|y|} \Gamma_\infty(|y|)\right)\\
&\le C\begin{cases}
|y|^{-2} & \text{if $n=3$}\\
|y|^{-2}\log 5|y| & \text{if $n=2$}
\end{cases}\\
&\le C|y|^{-2}\left|\frac{d^2}{d|y|^2} \Gamma_\infty(|y|)\right|
\end{align*}
which implies \eqref{eq1.14.2}.
\end{proof}

\section{Proof of Theorem \ref{thm1.1}}
\label{sec5}

\indent

As noted in the introduction,
the sufficiency of condition \eqref{eq1.3} in Theorem \ref{thm1.1} and
the estimate \eqref{eq1.5} follow from Theorem \ref{thm1.3}, which we
proved in the last section. Consequently, we can complete the proof of
Theorem \ref{thm1.1} by proving the following proposition.

\begin{pro}\label{pro5.1}
  Suppose $n\ge 2$ and $m\ge 1$ are integers such that \eqref{eq1.3}
  does not hold. Let $\psi\colon (0,1)\to (0,\infty)$ be a
  continuous function. Then there exists a $C^\infty$ positive solution
  of
\begin{equation}\label{eq4.3.1}
 -\Delta^m u \ge 0\quad \text{in}\quad B_1(0)-\{0\}\subset {\bb R}^n
\end{equation}
such that
\begin{equation}\label{eq4.3.2}
 u(x)\ne O(\psi(|x|)) \quad \text{as}\quad x\to 0.
\end{equation}
\end{pro}

\begin{proof}
  Let $\{x_j\}^\infty_{j=1} \subset {\bb R}^n-\{0\}$ be a sequence
  such that $4|x_{j+1}| < |x_j| < 1$. Choose $\alpha_j>0$ such that
\begin{equation}\label{eq4.18}
 \frac{\alpha_j}{\psi(x_j)}\to \infty \quad \text{as}\quad j\to \infty.
\end{equation}
Since \eqref{eq1.3} does not hold, it follows from
\eqref{eq3.1}--\eqref{eq3.3} that $\lim\limits_{x\to 0} - \Phi(x) =
\infty$ and $-\Phi(x) > 0$ for $0<|x|<5$. Hence we can choose $R_j\in
(0, |x_j|/4)$ such that
\begin{equation}\label{eq4.19}
\intl_{|z|<R_j} - \Phi(z)\,dz > R^n_j 2^j\alpha_j,\quad \text{for}
\quad j=1,2,\ldots~.
\end{equation}
Let $\varphi\colon {\bb R}\to [0,1]$ be a $C^\infty$ function such
that $\varphi(t) = 1$ for $t\le 1$ and $\varphi(t) = 0$ for $t\ge
2$. Define $f_j\in C^\infty_0(B_{\frac{|x_j|}2}(x_j))$ by
\[
 f_j(x) = \frac1{2^jR^n_j} \varphi\left(\frac{|x-x_j|}{R_j}\right).
\]
Then the functions $f_j$ have disjoint supports and
\[
 \intl_{{\bb R}^n} f_j(x)\,dx = \intl_{|x-x_j|<2R_j} f_j(x)\,dx
\le \frac{C(n)}{2^j}.
\]
Thus $f := \sum\limits^\infty_{j=1} f_j\in L^1({\bb R}^n) \cap
C^\infty({\bb R}^n - \{0\})$ and hence the function $u\colon B_1(0)
- \{0\}\to {\bb R}$ defined by
\[
 u(x) := \intl_{|y|<1} - \Phi(x-y) f(y)\,dy
\]
is a $C^\infty$ positive solution of \eqref{eq4.3.1}. Also
\begin{align*}
u(x_j) &\ge \intl_{|y|<1} - \Phi(x_j-y) f_j(y)\,dy\\
&\ge \frac1{2^jR^n_j} \intl_{|x-x_j|<R_j} - \Phi(x_j-y)\,dy\\
&= \frac1{2^jR^n_j} \intl_{|z|<R_j} - \Phi(z)\,dz > \alpha_j
\end{align*}
by \eqref{eq4.19}. Hence \eqref{eq4.18} implies that $u$ satisfies
\eqref{eq4.3.2}.
\end{proof}


TITLE: How to find points of the edge of one sphere inside another sphere.
QUESTION [2 upvotes]: I am highly unqualified for this kind of discussion, but I need it for a CS project that I am working on at the moment.
I have one large sphere and inside it is a smaller sphere. When this smaller sphere collides with the edge of the larger sphere, I want to get a grid of points that form the edge of the larger sphere in a relatively simplistic calculation (aka I don't want to test a large chunk of points to see if they form the edge). Here is a 2D version of what I want to do that I made in MS Paint:

REPLY [1 votes]: Let $r$ be radius of big circle and $s$ be radius of smaller. Assume big circle's middle is at origin and small circle's origin is at $(a,0)$ with $a>0$. In other words small circle's center is on positive half of $x$ axis.
Then the formulas for the circles are $r^2=x^2+y^2$ and $s^2=(x-a)^2+y^2$. To find the value of $x$ for where the circles intersect, then solve for $x$ using these two equations. Since $y^2=r^2-x^2$, substitute that into second equation to get $$s^2=(x-a)^2+r^2-x^2 \Rightarrow x = \frac{a^2+r^2-s^2}{2a} \tag{1}$$.
Then any value of $x$ between that computed using (1) and $r$ is in the range of the red arc (from OP). So points can be computed by plugging values of $x$ in that range into equation for big circle.


TITLE: Arrangements around a circle
QUESTION [1 upvotes]: $5$ mathematicians, $5$ biologists, $5$ chemists, $5$ physicists, and $5$ economists sit around a large round table. Prove that the $25$ people can be seated such that, if $A$ and $B$ are two different people with the same specialty (for example, two mathematicians), then the people sitting to the immediate left of $A$ and to the immediate left of $B$ are of different specialties (for example, a biologist and a chemist).

Should I try to use induction?

REPLY [1 votes]: This is a slightly easier version of problem $1$ of the second day of the 1998 Iberoamerican Olimpiad available here.
We can solve it by induction. We prove the statement, if there are $n$ science fields and $n$ scientists from each field we can sit them so that that if $A$ and $B$ belong to the same field then the person to the left of $A$ and the person to the left of $B$ belong to different fields.
Base case: (I trust you can find suitable arrangements for $n=1$ and $2$.
Inductive step. We take a suitable arrangement for $n$ people. We must add $n$ people belonging to the new field and one person from each of the old $n$ fields of science. To do this choose any two seats in the old arrangement and introduce the $2n$ new empty seats in between them. Suppose the new field of science is Wolframology, We fill the $2n$ new fields of science by placing a Wolframologist in the first place, then a scientist from a diferent field , then a wolframologist, and so on. Alternating between a Wolframologist and one of the old sciences. If the two seats we picked initially where of sciences $A$ and $B$ just make sure that the final seat picked is occupied by a scientist of science $A$. This arrangement works because al of the Wolframologists have scientists from different fields to their left and all of the other new scientists have Wolframologists to their left.
You can find other solutions to the problem in the link that I purveyed.


TITLE: Core language representation of path application with extension types
QUESTION [3 upvotes]: Suppose I have a concat function with a signature using extension types:
def concat
 (p : [i] A {}) -- faceless
 (q : [i] A {i=0 ↦ p 1}) -- one face
 : [i] A {i=0 ↦ p 0, i=1 ↦ q 1}

I am using Cubical Agda's approach to represent interval-elimination, say, p i where p : [i] A {rua} is implemented as IApp(Ref(p), Arg(Ref(i)), rua) where rua contains the faces in the type of p. This gives the reduction sufficient (I believe) type information so in the type checker I can have normalize : Term -> Term instead of normalize : Term -> Type -> Term.
So here, p 0 is represented as IApp(Ref(p), Arg(Ref(i)), no-face) because that's what the type signature says. So there is no special type-directed reduction for it.
However, when I supply {an argument x that actually has some faces} to it (so like, x : [i] A {i=0 ↦ y}), type-checking x : [i] A {} loses the faces I needed, and leads to some type errors (the LHS of the result path is a stuck term x 0 because p has no face (even though x does have)).
I wonder if:

My representation of interval application is incorrect, or
This is a known issue with extension types itself, or
Am I doing substitution wrongly, or
Is there something else that I should be aware of?

REPLY [3 votes]: Your core representation of extension type application is the right one. The issue in the example is in the conversion from an extension with faces to the faceless. In the surface language, it can be implicit (as some form of subtyping), but in the core language it should be explicit.
Given p : [i] A {faces}, we forget its faces by eta-expansion (using lambda
for extension abstraction): (λ i. p i) : [i] A {}. Here the p i application
is represented according to your scheme, as IApp(p, i, faces).
When concat is applied to (λ i. p i), the return type is instantiated to
[i] A {i=0 ↦ (λ i. p i) 0, i=1 ↦ q 1}, and (λ i. p i) 0 reduces to p 0,
but this application is annotated with the original faces of p. So everything
is well-typed and we don't lose track of the faces.


TITLE: Is there an opposite of proof by contradiction?
QUESTION [1 upvotes]: Suppose I want to prove $a=b$.
I start by assuming $a=b$. I simplify the expressions and arrive at something which is always true like $1=1$. Does this mean that the original statement is true?

REPLY [2 votes]: $-1=1 \implies (-1)^2=1^2 \implies 1=1$.
But $-1=1$ is obviously not true.


TITLE: Complete convergence is equivalent to convergence a.s. under independence
QUESTION [6 upvotes]: $X_1,X_2,\ldots$ is a sequence of random variables that are complete convergent to $X$ if $$\sum_{n=1}^{\infty} P(\mid X_n-X\mid >\epsilon)<\infty \space\forall\epsilon > 0$$. Show if $X_n$ are independent, then complete convergence is equivalent to convergence a.s.
I showed that complete convergence implies convergence a.s. using the Borel-Cantelli lemma, but I'm not sure how to use show the converse using independence. This is what I have so far:
$$X_n\rightarrow_{a.s.} X \implies X_n\rightarrow_{p} 0$$ WLOG, $X=0$.
$$\forall\epsilon >0, P(\mid X_n\mid > \epsilon)\rightarrow 0$$
$$P(\limsup_{n\rightarrow\infty} \mid X_n\mid > \epsilon)=0$$
Since they are independent, then $\{\mid X\mid > \epsilon\}$ are independent, and can I use Borel-Cantelli (ii) to say $\sum P(\mid X_n\mid >\epsilon) < \infty$?

REPLY [0 votes]: I think that the conclusion to your proof could be:
$$P(\limsup \ |X_n|> \epsilon) = 0 \to P(\liminf \ |X_n|< \epsilon) = 1 \to P(\cup\cap |X_n| < \epsilon)=1$$
Now:
$$\lim_{n \to \infty}P(\cap_{m>n \ } |X_n| < \epsilon)=1 \to \lim_{n \to \infty}P( |X_n| < \epsilon)=1 $$
using the independence, that is the intersection could become a infinity product of probability, therefore $p^{\infty}$ but taking the reciprocal power both to $p$ and to the rhs (that is $1$), we have the result.
Could be this the final proof?


TITLE: Rod cutting: requesting a proof for $2^{n-1}$ possible ways
QUESTION [3 upvotes]: The rod cutting problem states that: Given a rod of length $n$ inches and a table of prices $P_i$ for $i=1,\dots,n$, determine the maximum revenue $R_n$.
In CLRS chapter 15 Rod cutting page 360:

We can cut up a rod of length $n$ in $2^{n-1}$ different ways

I can intuitively understand why this is so; basically we can construct a binary tree of height $\log N$. But can someone provide me a proof of why this is so?

REPLY [2 votes]: For Example:- n = 4
 --- --- --- ---
|   |   |   |   |  --> Rod of length 4 inches
 --- --- --- ---       ^ is showing where we can make cuts
    ^   ^   ^

Now, Above given ^ position either we make a cut or not i.e; 0 for not making a cut and 1 for making a cut. We get $ 2^3 $ binary combinations are as follows:
           ---     --- --- ---
1 0 0 --> |   |   |   |   |   |
           ---     --- --- ---
           --- ---     --- ---
0 1 0 --> |   |   |   |   |   |
           --- ---     --- ---
           --- --- ---     ---
1 0 0 --> |   |   |   |   |   |
           --- --- ---     ---
           ---     ---     --- ---
1 1 0 --> |   |   |   |   |   |   |
           ---     ---     --- ---
           ---     --- ---     ---
1 0 1 --> |   |   |   |   |   |   |
           ---     --- ---     ---
           --- ---     ---     ---
0 1 1 --> |   |   |   |   |   |   |
           --- ---     ---     ---
           ---     ---     ---     ---
1 1 1 --> |   |   |   |   |   |   |   |
           ---     ---     ---     ---
           --- --- --- ---
1 1 1 --> |   |   |   |   |
           --- --- --- ---

Hence, A Rod of length "n" inches can be cut into $ 2^{n-1} $ pieces.


TITLE: What function can I use to fit through the points (0,1), (13,0) and (p,q)?
QUESTION [0 upvotes]: I'm trying to find a function that will go through $(0,1)$, $(13,0)$, with another point in between, say at $(6,p)$ where $0\le p\le 1$, that I can vary up and down to make the curve similar to a straight line, or as steep as possible when x is near 0.
Isn't it just a general exponential function?
I'm trying to find a function that enables me to 'flex' the curve as described above, by modifying only one variable.  I'm sure I saw a function like that once, but maybe I'm wrong.

REPLY [1 votes]: An exponential function won't work unless you add in a constant term, because exponential functions are never $0$.
With three points, the simplest choice for fitting would be a quadratic function, but there are lots of other possibilities. Which one you use should depend on some knowledge about where your function is supposed to represent -- but in the absence of such information I'd just go with the polynomial.


text:
(*******************************************************************************

  Project: Refining Authenticated Key Agreement with Strong Adversaries

  Module:  sklvl1.thy (Isabelle/HOL 2016-1)
  ID:      $Id: sklvl1.thy 133183 2017-01-31 13:55:43Z csprenge $
  Author:  Joseph Lallemand, INRIA Nancy <joseph.lallemand@loria.fr>
           Christoph Sprenger, ETH Zurich <sprenger@inf.ethz.ch>

  Level-1 Diffie-Hellman guard protocol augmented with two nonces.
  Refines model dhlvl1, moving towards SKEME/IKEv1 protocol.

  Copyright (c) 2015-2016 Joseph Lallemand and Christoph Sprenger
  Licence: LGPL

*******************************************************************************)

section \<open>SKEME Protocol (L1)\<close>

theory sklvl1
imports dhlvl1
begin

declare option.split_asm [split]

(**************************************************************************************************)
subsection \<open>State and Events\<close>
(**************************************************************************************************)

abbreviation ni :: nat where "ni \<equiv> 4"
abbreviation nr :: nat where "nr \<equiv> 5"

text \<open>Proofs break if @{term "1"} is used, because @{method "simp"} replaces it with
@{term "Suc 0"}\dots.\<close>

abbreviation
  "xni \<equiv> Var 7"

abbreviation
  "xnr \<equiv> Var 8"

text \<open>Domain of each role (protocol-dependent).\<close>

fun domain :: "role_t \<Rightarrow> var set" where
  "domain Init = {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
| "domain Resp = {xny, xni, xnr, xgnx, xgny, xsk, xEnd}"

consts
  guessed_frame :: "rid_t \<Rightarrow> frame"

text \<open>Specification of the guessed frame:
\begin{enumerate}
\item Domain.
\item Well-typedness.
  The messages in the frame of a run never contain implementation material
  even if the agents of the run are dishonest.
  Therefore we consider only well-typed frames.
  This is notably required for the session key compromise; it also helps proving
  the partitionning of ik,
  since we know that the messages added by the protocol do not contain ltkeys in their
  payload and are therefore valid implementations.
\item We also ensure that the values generated by the frame owner are correctly guessed.
\item The new frame extends the previous one (from @{theory Key_Agreement_Strong_Adversaries.dhlvl1})
\end{enumerate}
\<close>
specification (guessed_frame)
  guessed_frame_dom_spec [simp]:
    "dom (guessed_frame R) = domain (role (guessed_runs R))"
  guessed_frame_payload_spec [simp, elim]:
    "guessed_frame R x = Some y \<Longrightarrow> y \<in> payload"
  guessed_frame_Init_xnx [simp]:
    "role (guessed_runs R) = Init \<Longrightarrow> guessed_frame R xnx = Some (NonceF (R$nx))"
  guessed_frame_Init_xgnx [simp]:
    "role (guessed_runs R) = Init \<Longrightarrow> guessed_frame R xgnx = Some (Exp Gen (NonceF (R$nx)))"
  guessed_frame_Init_xni [simp]:
    "role (guessed_runs R) = Init \<Longrightarrow> guessed_frame R xni = Some (NonceF (R$ni))"
  guessed_frame_Resp_xny [simp]:
    "role (guessed_runs R) = Resp \<Longrightarrow> guessed_frame R xny = Some (NonceF (R$ny))"
  guessed_frame_Resp_xgny [simp]:
    "role (guessed_runs R) = Resp \<Longrightarrow> guessed_frame R xgny = Some (Exp Gen (NonceF (R$ny)))"
  guessed_frame_Resp_xnr [simp]:
    "role (guessed_runs R) = Resp \<Longrightarrow> guessed_frame R xnr = Some (NonceF (R$nr))"
  guessed_frame_xEnd [simp]:
    "guessed_frame R xEnd = Some End"
  guessed_frame_eq [simp]:
    "x \<in> {xnx, xny, xgnx, xgny, xsk, xEnd} \<Longrightarrow> dhlvl1.guessed_frame R x = guessed_frame R x"
apply (rule exI [of _
    "\<lambda>R.
      if role (guessed_runs R) = Init then
        (dhlvl1.guessed_frame R) (xni \<mapsto> NonceF (R$ni), xnr \<mapsto> End)
      else
        (dhlvl1.guessed_frame R) (xnr \<mapsto> NonceF (R$nr), xni \<mapsto> End)"],
  auto simp add: domIff intro: role_t.exhaust)
done

record skl1_state =
  l1_state +
  signalsInit2 :: "signal \<Rightarrow> nat"
  signalsResp2 :: "signal \<Rightarrow> nat"

type_synonym skl1_obs = "skl1_state"

text \<open>Protocol events:
\begin{itemize}
\item step 1: create @{term "Ra"}, @{term "A"} generates @{term "nx"} and @{term "ni"},
  computes $@{term "g"}^@{term "nx"}$
\item step 2: create @{term "Rb"}, @{term "B"} reads @{term "ni"} and $@{term "g"}^@{term "nx"}$
  insecurely,
  generates @{term "ny"} and @{term "nr"}, computes $@{term "g"}^@{term "ny"}$,
  computes $@{term "g"}^@{term "nx*ny"}$,
  emits a running signal for @{term "Init"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "nx*ny"}$
\item step 3: @{term "A"} reads $@{term "g"}^@{term "ny"}$ and $@{term "g"}^@{term "nx"}$
  authentically,
  computes $@{term "g"}^@{term "ny*nx"}$, emits a commit signal for @{term "Init"}, @{term "ni"},
  @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
  a running signal for @{term "Resp"}, @{term "ni"}, @{term "nr"}, $@{term "g"}^@{term "ny*nx"}$,
  declares the secret $@{term "g"}^@{term "ny*nx"}$
\item step 4: @{term "B"} reads @{term "nr"}, @{term "ni"}, $@{term "g"}^@{term "nx"}$
  and $@{term "g"}^@{term "ny"}$ authentically,
  emits a commit signal for @{term "Resp"}, @{term "ni"}, @{term "nr"},
  $@{term "g"}^@{term "nx*ny"}$,
  declares the secret $@{term "g"}^@{term "nx*ny"}$
\end{itemize}
\<close>
definition
  skl1_step1 :: "rid_t \<Rightarrow> agent \<Rightarrow> agent \<Rightarrow> ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
  "skl1_step1 Ra A B \<equiv> {(s, s').
    \<comment> \<open>guards:\<close>
    Ra \<notin> dom (progress s) \<and>
    guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<and>
    \<comment> \<open>actions:\<close>
    s' = s\<lparr>
      progress := (progress s)(Ra \<mapsto> {xnx, xni, xgnx})
      \<rparr>
  }"

definition
  skl1_step2 ::
    "rid_t \<Rightarrow> agent \<Rightarrow> agent \<Rightarrow> msg \<Rightarrow> msg \<Rightarrow> ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
  "skl1_step2 Rb A B Ni gnx \<equiv> {(s, s').
    \<comment> \<open>guards:\<close>
    guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<and>
    Rb \<notin> dom (progress s) \<and>
    guessed_frame Rb xgnx = Some gnx \<and>
    guessed_frame Rb xni = Some Ni \<and>
    guessed_frame Rb xsk = Some (Exp gnx (NonceF (Rb$ny))) \<and>
    \<comment> \<open>actions:\<close>
    s' = s\<lparr> progress := (progress s)(Rb \<mapsto> {xny, xni, xnr, xgny, xgnx, xsk}),
            signalsInit :=
              if can_signal s A B then
                addSignal (signalsInit s)
                          (Running A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle>)
              else
                signalsInit s,
            signalsInit2 :=
              if can_signal s A B then
                addSignal (signalsInit2 s) (Running A B (Exp gnx (NonceF (Rb$ny))))
              else
                signalsInit2 s
          \<rparr>
  }"

definition
  skl1_step3 ::
    "rid_t \<Rightarrow> agent \<Rightarrow> agent \<Rightarrow> msg \<Rightarrow> msg \<Rightarrow> ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
  "skl1_step3 Ra A B Nr gny \<equiv> {(s, s').
    \<comment> \<open>guards:\<close>
    guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<and>
    progress s Ra = Some {xnx, xni, xgnx} \<and>
    guessed_frame Ra xgny = Some gny \<and>
    guessed_frame Ra xnr = Some Nr \<and>
    guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx))) \<and>
    (can_signal s A B \<longrightarrow> \<comment> \<open>authentication guard\<close>
      (\<exists> Rb. guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<and>
             in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} \<and>
             guessed_frame Rb xgny = Some gny \<and>
             guessed_frame Rb xnr = Some Nr \<and>
             guessed_frame Rb xni = Some (NonceF (Ra$ni)) \<and>
             guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))))) \<and>
    (Ra = test \<longrightarrow> Exp gny (NonceF (Ra$nx)) \<notin> synth (analz (ik s))) \<and>

    \<comment> \<open>actions:\<close>
    s' = s\<lparr> progress := (progress s)(Ra \<mapsto> {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}),
            secret := {x. x = Exp gny (NonceF (Ra$nx)) \<and> Ra = test} \<union> secret s,
            signalsInit :=
              if can_signal s A B then
                addSignal (signalsInit s)
                          (Commit A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle>)
              else
                signalsInit s,
            signalsInit2 :=
              if can_signal s A B then
                addSignal (signalsInit2 s) (Commit A B (Exp gny (NonceF (Ra$nx))))
              else
                signalsInit2 s,
            signalsResp :=
              if can_signal s A B then
                addSignal (signalsResp s)
                          (Running A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle>)
              else
                signalsResp s,
            signalsResp2 :=
              if can_signal s A B then
                addSignal (signalsResp2 s) (Running A B (Exp gny (NonceF (Ra$nx))))
              else
                signalsResp2 s
          \<rparr>
  }"

definition
  skl1_step4 ::
    "rid_t \<Rightarrow> agent \<Rightarrow> agent \<Rightarrow> msg \<Rightarrow> msg \<Rightarrow> ('a skl1_state_scheme * 'a skl1_state_scheme) set"
where
  "skl1_step4 Rb A B Ni gnx \<equiv> {(s, s').
    \<comment> \<open>guards:\<close>
    guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<and>
    progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} \<and>
    guessed_frame Rb xgnx = Some gnx \<and>
    guessed_frame Rb xni = Some Ni \<and>
    (can_signal s A B \<longrightarrow> \<comment> \<open>authentication guard\<close>
      (\<exists> Ra. guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<and>
             in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} \<and>
             guessed_frame Ra xgnx = Some gnx \<and>
             guessed_frame Ra xni = Some Ni \<and>
             guessed_frame Ra xnr = Some (NonceF (Rb$nr)) \<and>
             guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))))) \<and>
    (Rb = test \<longrightarrow> Exp gnx (NonceF (Rb$ny)) \<notin> synth (analz (ik s))) \<and>

    \<comment> \<open>actions:\<close>
    s' = s\<lparr> progress := (progress s)(Rb \<mapsto> {xny, xni, xnr, xgnx, xgny, xsk, xEnd}),
            secret := {x. x = Exp gnx (NonceF (Rb$ny)) \<and> Rb = test} \<union> secret s,
            signalsResp :=
              if can_signal s A B then
                addSignal (signalsResp s)
                          (Commit A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle>)
              else
                signalsResp s,
            signalsResp2 :=
              if can_signal s A B then
                addSignal (signalsResp2 s) (Commit A B (Exp gnx (NonceF (Rb$ny))))
              else
                signalsResp2 s
          \<rparr>
  }"

text \<open>Specification.\<close>

definition
  skl1_trans :: "('a skl1_state_scheme * 'a skl1_state_scheme) set" where
  "skl1_trans \<equiv> (\<Union>m Ra Rb A B x y.
     skl1_step1 Ra A B \<union>
     skl1_step2 Rb A B x y \<union>
     skl1_step3 Ra A B x y \<union>
     skl1_step4 Rb A B x y \<union>
     l1_learn m \<union>
     Id
  )"

definition
  skl1_init :: "skl1_state set"
where
  "skl1_init \<equiv> { \<lparr>
    ik = {},
    secret = {},
    progress = Map.empty,
    signalsInit = \<lambda>x. 0,
    signalsResp = \<lambda>x. 0,
    signalsInit2 = \<lambda>x. 0,
    signalsResp2 = \<lambda>x. 0
    \<rparr> }"

definition
  skl1 :: "(skl1_state, skl1_obs) spec" where
  "skl1 \<equiv> \<lparr>
    init = skl1_init,
    trans = skl1_trans,
    obs = id
  \<rparr>"

lemmas skl1_defs =
  skl1_def skl1_init_def skl1_trans_def
  l1_learn_def
  skl1_step1_def skl1_step2_def skl1_step3_def skl1_step4_def

lemmas skl1_nostep_defs =
  skl1_def skl1_init_def skl1_trans_def

lemma skl1_obs_id [simp]: "obs skl1 = id"
by (simp add: skl1_def)

lemma run_ended_trans:
  "run_ended (progress s R) \<Longrightarrow>
   (s, s') \<in> trans skl1 \<Longrightarrow>
   run_ended (progress s' R)"
by (auto simp add: skl1_nostep_defs)
   (auto simp add: skl1_defs ik_dy_def domIff)

lemma can_signal_trans:
  "can_signal s' A B \<Longrightarrow>
  (s, s') \<in> trans skl1 \<Longrightarrow>
  can_signal s A B"
by (auto simp add: can_signal_def run_ended_trans)

(**************************************************************************************************)
subsection \<open>Refinement: secrecy\<close>
(**************************************************************************************************)

fun option_inter :: "var set \<Rightarrow> var set option \<Rightarrow> var set option"
where
  "option_inter S (Some x) = Some (x \<inter> S)"
 |"option_inter S None = None"

definition med_progress :: "progress_t \<Rightarrow> progress_t"
where
  "med_progress r \<equiv> \<lambda> R. option_inter {xnx, xny, xgnx, xgny, xsk, xEnd} (r R)"

lemma med_progress_upd [simp]:
  "med_progress (r(R \<mapsto> S)) = (med_progress r) (R \<mapsto> S \<inter> {xnx, xny, xgnx, xgny, xsk, xEnd})"
by (auto simp add: med_progress_def)

lemma med_progress_Some:
  "r x = Some s \<Longrightarrow> med_progress r x = Some (s \<inter> {xnx, xny, xgnx, xgny, xsk, xEnd})"
by (auto simp add: med_progress_def)

lemma med_progress_None [simp]: "med_progress r x = None \<longleftrightarrow> r x = None"
by (cases "r x", auto simp add: med_progress_def)

lemma med_progress_Some2 [dest]:
  "med_progress r x = Some y \<Longrightarrow> \<exists> z. r x = Some z \<and> y = z \<inter> {xnx, xny, xgnx, xgny, xsk, xEnd}"
by (cases "r x", auto simp add: med_progress_def)

lemma med_progress_dom [simp]: "dom (med_progress r) = dom r"
apply (auto simp add: domIff med_progress_def)
apply (rename_tac x y, case_tac "r x", auto)
done

lemma med_progress_empty [simp]: "med_progress Map.empty = Map.empty"
by (rule ext, auto)

text \<open>Mediator function.\<close>

definition
  med11 :: "skl1_obs \<Rightarrow> l1_obs"
where
  "med11 t \<equiv> \<lparr>ik = ik t,
              secret=secret t,
              progress = med_progress (progress t),
              signalsInit = signalsInit2 t,
              signalsResp = signalsResp2 t\<rparr>"

text \<open>relation between states\<close>
definition
  R11 :: "(l1_state * skl1_state) set"
where
  "R11 \<equiv> {(s,s').
    s = med11 s'
    }"

lemmas R11_defs = R11_def med11_def

lemma in_progress_med_progress:
  "x \<in> {xnx, xny, xgnx, xgny, xsk, xEnd}
  \<Longrightarrow> in_progress (med_progress r R) x \<longleftrightarrow> in_progress (r R) x"
by (cases "r R", auto)
   (cases "med_progress r R", auto)+

lemma in_progressS_eq: "in_progressS S S' \<longleftrightarrow> (S \<noteq> None \<and> (\<forall> x \<in> S'. in_progress S x))"
by (cases S, auto)

lemma in_progressS_med_progress:
  "in_progressS (r R) S
  \<Longrightarrow> in_progressS (med_progress r R) (S \<inter> {xnx, xny, xgnx, xgny, xsk, xEnd})"
by (auto simp add: in_progressS_eq in_progress_med_progress)

lemma can_signal_R11 [simp]:
  "(s1, s2) \<in> R11 \<Longrightarrow>
   can_signal s1 A B \<longleftrightarrow> can_signal s2 A B"
by (auto simp add: can_signal_def R11_defs in_progress_med_progress)

text \<open>Protocol-independent events.\<close>

lemma skl1_learn_refines_learn:
  "{R11} l1_learn m, l1_learn m {>R11}"
by (auto simp add: PO_rhoare_defs R11_defs)
   (simp add: l1_defs)

text \<open>Protocol events.\<close>

lemma skl1_step1_refines_step1:
  "{R11} l1_step1 Ra A B, skl1_step1 Ra A B {>R11}"
by (auto simp add: PO_rhoare_defs R11_defs l1_step1_def skl1_step1_def)

lemma skl1_step2_refines_step2:
  "{R11} l1_step2 Rb A B gnx, skl1_step2 Rb A B Ni gnx {>R11}"
by (auto simp add: PO_rhoare_defs R11_defs  l1_step2_def)
   (auto simp add: skl1_step2_def)

lemma skl1_step3_refines_step3:
  "{R11} l1_step3 Ra A B gny, skl1_step3 Ra A B Nr gny {>R11}"
apply (auto simp add: PO_rhoare_defs R11_defs l1_step3_def)
apply (auto simp add: skl1_step3_def, auto dest: med_progress_Some)
apply (drule in_progressS_med_progress, auto)+
done

lemma skl1_step4_refines_step4:
  "{R11} l1_step4 Rb A B gnx, skl1_step4 Rb A B Ni gnx {>R11}"
apply (auto simp add: PO_rhoare_defs R11_defs l1_step4_def)
apply (auto simp add: skl1_step4_def, auto dest: med_progress_Some)
apply (drule in_progressS_med_progress, auto)+
done

text \<open>Refinement proof.\<close>

lemmas skl1_trans_refines_l1_trans =
  skl1_learn_refines_learn
  skl1_step1_refines_step1 skl1_step2_refines_step2
  skl1_step3_refines_step3 skl1_step4_refines_step4

lemma skl1_refines_init_l1 [iff]:
  "init skl1 \<subseteq> R11 `` (init l1)"
by (auto simp add: R11_defs l1_defs skl1_defs)

lemma skl1_refines_trans_l1 [iff]:
  "{R11} trans l1, trans skl1 {> R11}"
by (auto 0 3 simp add: l1_def skl1_def l1_trans_def skl1_trans_def
             intro: skl1_trans_refines_l1_trans)

lemma obs_consistent_med11 [iff]:
  "obs_consistent R11 med11 l1 skl1"
by (auto simp add: obs_consistent_def R11_defs)

text \<open>Refinement result.\<close>

lemma skl1_refines_l1 [iff]:
  "refines
     R11
     med11 l1 skl1"
by (auto simp add:refines_def PO_refines_def)

lemma  skl1_implements_l1 [iff]: "implements med11 l1 skl1"
by (rule refinement_soundness) (fast)

(**************************************************************************************************)
subsection \<open>Derived invariants: secrecy\<close>
(**************************************************************************************************)

lemma skl1_obs_secrecy [iff]: "oreach skl1 \<subseteq> s0_secrecy"
apply (rule external_invariant_translation [OF l1_obs_secrecy _ skl1_implements_l1])
apply (auto simp add: med11_def s0_secrecy_def)
done

lemma skl1_secrecy [iff]: "reach skl1 \<subseteq> s0_secrecy"
by (rule external_to_internal_invariant [OF skl1_obs_secrecy], auto)

(**************************************************************************************************)
subsection \<open>Invariants: @{term "Init"} authenticates @{term "Resp"}\<close>
(**************************************************************************************************)

subsubsection \<open>inv1\<close>
(**************************************************************************************************)

text \<open>If an initiator commit signal exists for @{term "Ra$ni"}, @{term "Nr"},
  $(@{term "g"}^@{term "ny"})^@{term "Ra$nx"}$, then @{term "Ra"} is
  @{term "Init"}, has passed step 3, and has the nonce @{term "Nr"}, and
  \<open>(g^ny)^(Ra$nx)\<close> as the key in its frame.
\<close>
definition
  skl1_inv1 :: "skl1_state set"
where
  "skl1_inv1 \<equiv> {s. \<forall> Ra A B gny Nr.
    signalsInit s (Commit A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle>) > 0 \<longrightarrow>
      guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<and>
      progress s Ra = Some {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} \<and>
      guessed_frame Ra xnr = Some Nr \<and>
      guessed_frame Ra xsk = Some (Exp gny (NonceF (Ra$nx)))
   }"

lemmas skl1_inv1I = skl1_inv1_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv1E [elim] = skl1_inv1_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv1D = skl1_inv1_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma skl1_inv1_init [iff]:
  "init skl1 \<subseteq> skl1_inv1"
by (auto simp add: skl1_def skl1_init_def skl1_inv1_def)

lemma skl1_inv1_trans [iff]:
  "{skl1_inv1} trans skl1 {> skl1_inv1}"
apply (auto simp add: PO_hoare_defs skl1_nostep_defs intro!: skl1_inv1I)
apply (auto simp add: skl1_defs ik_dy_def skl1_inv1_def domIff dest: Exp_Exp_Gen_inj2 [OF sym])
done

lemma PO_skl1_inv1 [iff]: "reach skl1 \<subseteq> skl1_inv1"
by (rule inv_rule_basic) (auto)

subsubsection \<open>inv2\<close>
(**************************************************************************************************)

text \<open>If a @{term "Resp"} run @{term "Rb"} has passed step 2 then (if possible)
an initiator running signal has been emitted.\<close>

definition
  skl1_inv2 :: "skl1_state set"
where
  "skl1_inv2 \<equiv> {s. \<forall> gnx A B Rb Ni.
    guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<longrightarrow>
    in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} \<longrightarrow>
    guessed_frame Rb xgnx = Some gnx \<longrightarrow>
    guessed_frame Rb xni = Some Ni \<longrightarrow>
    can_signal s A B \<longrightarrow>
      signalsInit s (Running A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle>) > 0
  }"

lemmas skl1_inv2I = skl1_inv2_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv2E [elim] = skl1_inv2_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv2D = skl1_inv2_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma skl1_inv2_init [iff]:
  "init skl1 \<subseteq> skl1_inv2"
by (auto simp add: skl1_def skl1_init_def skl1_inv2_def)

lemma skl1_inv2_trans [iff]:
  "{skl1_inv2} trans skl1 {> skl1_inv2}"
apply (auto simp add: PO_hoare_defs intro!: skl1_inv2I)
apply (drule can_signal_trans, assumption)
apply (auto simp add: skl1_nostep_defs)
apply (auto simp add: skl1_defs ik_dy_def skl1_inv2_def)
done

lemma PO_skl1_inv2 [iff]: "reach skl1 \<subseteq> skl1_inv2"
by (rule inv_rule_basic) (auto)

subsubsection \<open>inv3 (derived)\<close>
(**************************************************************************************************)

text \<open>If an @{term "Init"} run before step 3 and a @{term "Resp"} run after step 2 both know
  the same half-keys and nonces (more or less), then the number of @{term "Init"} running signals
  for the key is strictly greater than the number of @{term "Init"} commit signals.
  (actually, there are 0 commit and 1 running).
\<close>

definition
  skl1_inv3 :: "skl1_state set"
where
  "skl1_inv3 \<equiv> {s. \<forall> A B Rb Ra gny Nr.
    guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<longrightarrow>
    in_progressS (progress s Rb) {xny, xni, xnr, xgnx, xgny, xsk} \<longrightarrow>
    guessed_frame Rb xgny = Some gny \<longrightarrow>
    guessed_frame Rb xnr = Some Nr \<longrightarrow>
    guessed_frame Rb xni = Some (NonceF (Ra$ni)) \<longrightarrow>
    guessed_frame Rb xgnx = Some (Exp Gen (NonceF (Ra$nx))) \<longrightarrow>
    guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<longrightarrow>
    progress s Ra = Some {xnx, xgnx, xni} \<longrightarrow>
    can_signal s A B \<longrightarrow>
      signalsInit s (Commit A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle>)
    < signalsInit s (Running A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle>)
  }"

lemmas skl1_inv3I = skl1_inv3_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv3E [elim] = skl1_inv3_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv3D = skl1_inv3_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma skl1_inv3_derived: "skl1_inv1 \<inter> skl1_inv2 \<subseteq> skl1_inv3"
apply (auto intro!:skl1_inv3I)
apply (auto dest!: skl1_inv2D)
apply (rename_tac x A B Rb Ra)
apply (case_tac
  "signalsInit x (Commit A B
     \<langle>NonceF (Ra $ ni), NonceF (Rb $ nr),
      Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))\<rangle>) > 0", auto)
apply (fastforce dest: skl1_inv1D elim: equalityE)
done

subsection \<open>Invariants: Resp authenticates Init\<close>
(**************************************************************************************************)

subsubsection \<open>inv4\<close>
(**************************************************************************************************)

text \<open>If a @{term "Resp"} commit signal exists for @{term "Ni"}, @{term "Rb$nr"},
  $(@{term "g"}^@{term "nx"})^@{term "Rb$ny"}$
  then @{term "Rb"} is @{term "Resp"}, has finished its run, and has the nonce @{term "Ni"} and
  $(@{term "g"}^@{term "nx"})^@{term "Rb$ny"}$ as the key in its frame.
\<close>
definition
  skl1_inv4 :: "skl1_state set"
where
  "skl1_inv4 \<equiv> {s. \<forall> Rb A B gnx Ni.
    signalsResp s (Commit A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle>) > 0 \<longrightarrow>
      guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<and>
      progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk, xEnd} \<and>
      guessed_frame Rb xgnx = Some gnx \<and>
      guessed_frame Rb xni = Some Ni
   }"

lemmas skl1_inv4I = skl1_inv4_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv4E [elim] = skl1_inv4_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv4D = skl1_inv4_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma skl1_inv4_init [iff]:
  "init skl1 \<subseteq> skl1_inv4"
by (auto simp add: skl1_def skl1_init_def skl1_inv4_def)

lemma skl1_inv4_trans [iff]:
  "{skl1_inv4} trans skl1 {> skl1_inv4}"
apply (auto simp add: PO_hoare_defs skl1_nostep_defs intro!: skl1_inv4I)
apply (auto simp add: skl1_inv4_def skl1_defs ik_dy_def domIff dest: Exp_Exp_Gen_inj2 [OF sym])
done

lemma PO_skl1_inv4 [iff]: "reach skl1 \<subseteq> skl1_inv4"
by (rule inv_rule_basic) (auto)

subsubsection \<open>inv5\<close>
(**************************************************************************************************)

text \<open>If an @{term "Init"} run @{term "Ra"} has passed step3 then (if possible) a
@{term "Resp"} running signal has been emitted.\<close>

definition
  skl1_inv5 :: "skl1_state set"
where
  "skl1_inv5 \<equiv> {s. \<forall> gny A B Ra Nr.
    guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<longrightarrow>
    in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} \<longrightarrow>
    guessed_frame Ra xgny = Some gny \<longrightarrow>
    guessed_frame Ra xnr = Some Nr \<longrightarrow>
    can_signal s A B \<longrightarrow>
      signalsResp s (Running A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle>) > 0
  }"

lemmas skl1_inv5I = skl1_inv5_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv5E [elim] = skl1_inv5_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv5D = skl1_inv5_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma skl1_inv5_init [iff]:
  "init skl1 \<subseteq> skl1_inv5"
by (auto simp add: skl1_def skl1_init_def skl1_inv5_def)

lemma skl1_inv5_trans [iff]:
  "{skl1_inv5} trans skl1 {> skl1_inv5}"
apply (auto simp add: PO_hoare_defs intro!: skl1_inv5I)
apply (drule can_signal_trans, assumption)
apply (auto simp add: skl1_nostep_defs)
apply (auto simp add: skl1_defs ik_dy_def dest: skl1_inv5D)
done

lemma PO_skl1_inv5 [iff]: "reach skl1 \<subseteq> skl1_inv5"
by (rule inv_rule_basic) (auto)

subsubsection \<open>inv6 (derived)\<close>
(**************************************************************************************************)

text \<open>If a @{term "Resp"} run before step 4 and an @{term "Init"} run after step 3 both know
  the same half-keys (more or less), then the number of @{term "Resp"} running signals
  for the key is strictly greater than the number of @{term "Resp"} commit signals.
  (actually, there are 0 commit and 1 running).
\<close>

definition
  skl1_inv6 :: "skl1_state set"
where
  "skl1_inv6 \<equiv> {s. \<forall> A B Rb Ra gnx Ni.
    guessed_runs Ra = \<lparr>role=Init, owner=A, partner=B\<rparr> \<longrightarrow>
    in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd} \<longrightarrow>
    guessed_frame Ra xgnx = Some gnx \<longrightarrow>
    guessed_frame Ra xni = Some Ni \<longrightarrow>
    guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb$ny))) \<longrightarrow>
    guessed_frame Ra xnr = Some (NonceF (Rb$nr)) \<longrightarrow>
    guessed_runs Rb = \<lparr>role=Resp, owner=B, partner=A\<rparr> \<longrightarrow>
    progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk} \<longrightarrow>
    can_signal s A B \<longrightarrow>
      signalsResp s (Commit A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle>)
    < signalsResp s (Running A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle>)
  }"

lemmas skl1_inv6I = skl1_inv6_def [THEN setc_def_to_intro, rule_format]
lemmas skl1_inv6E [elim] = skl1_inv6_def [THEN setc_def_to_elim, rule_format]
lemmas skl1_inv6D = skl1_inv6_def [THEN setc_def_to_dest, rule_format, rotated 1, simplified]

lemma skl1_inv6_derived:
  "skl1_inv4 \<inter> skl1_inv5 \<subseteq> skl1_inv6"
proof (auto intro!: skl1_inv6I)
  fix s::skl1_state fix A B Rb Ra
  assume HRun:"guessed_runs Ra = \<lparr>role = Init, owner = A, partner = B\<rparr>"
              "in_progressS (progress s Ra) {xnx, xni, xnr, xgnx, xgny, xsk, xEnd}"
              "guessed_frame Ra xgny = Some (Exp Gen (NonceF (Rb $ ny)))"
              "guessed_frame Ra xnr = Some (NonceF (Rb $ nr))"
              "can_signal s A B"
  assume HRb: "progress s Rb = Some {xny, xni, xnr, xgnx, xgny, xsk}"
  assume I4:"s \<in> skl1_inv4"
  assume I5:"s \<in> skl1_inv5"
  from I4 HRb have "signalsResp s (Commit A B \<langle>NonceF (Ra$ni), NonceF (Rb$nr),
                      Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))\<rangle>) > 0 \<Longrightarrow> False"
    proof (auto dest!: skl1_inv4D)
      assume "{xny, xni, xnr, xgnx, xgny, xsk, xEnd} = {xny, xni, xnr, xgnx, xgny, xsk}"
      thus ?thesis by force
    qed
  then have HC:"signalsResp s (Commit A B \<langle>NonceF (Ra$ni), NonceF (Rb$nr),
                      Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))\<rangle>) = 0"
    by auto
  from I5 HRun have "signalsResp s (Running A B \<langle>NonceF (Ra$ni), NonceF (Rb$nr),
                      Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))\<rangle>) > 0"
    by (auto dest!: skl1_inv5D)
  with HC show "signalsResp s (Commit A B \<langle>NonceF (Ra$ni), NonceF (Rb$nr),
                      Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))\<rangle>)
              < signalsResp s (Running A B \<langle>NonceF (Ra$ni), NonceF (Rb$nr),
                      Exp (Exp Gen (NonceF (Rb $ ny))) (NonceF (Ra $ nx))\<rangle>)"
    by auto
qed

(**************************************************************************************************)
subsection \<open>Refinement: injective agreement  (Init authenticates Resp)\<close>
(**************************************************************************************************)

text \<open>Mediator function.\<close>

definition
  med0sk1iai :: "skl1_obs \<Rightarrow> a0i_obs"
where
  "med0sk1iai t \<equiv> \<lparr>a0n_state.signals = signalsInit t\<rparr>"

text \<open>Relation between states.\<close>

definition
  R0sk1iai :: "(a0i_state * skl1_state) set"
where
  "R0sk1iai \<equiv> {(s,s').
    a0n_state.signals s = signalsInit s'
    }"

text \<open>Protocol-independent events.\<close>

lemma skl1_learn_refines_a0_ia_skip_i:
  "{R0sk1iai} Id, l1_learn m {>R0sk1iai}"
apply (auto simp add: PO_rhoare_defs R0sk1iai_def)
apply (simp add: l1_learn_def)
done

text \<open>Protocol events.\<close>

lemma skl1_step1_refines_a0i_skip_i:
  "{R0sk1iai} Id, skl1_step1 Ra A B {>R0sk1iai}"
by (auto simp add: PO_rhoare_defs R0sk1iai_def skl1_step1_def)

lemma skl1_step2_refines_a0i_running_skip_i:
  "{R0sk1iai} a0i_running A B \<langle>Ni, NonceF (Rb$nr),Exp gnx (NonceF (Rb$ny))\<rangle> \<union> Id,
              skl1_step2 Rb A B Ni gnx {>R0sk1iai}"
by (auto simp add: PO_rhoare_defs R0sk1iai_def,
    simp_all add: skl1_step2_def a0i_running_def, auto)

lemma skl1_step3_refines_a0i_commit_skip_i:
  "{R0sk1iai \<inter> (UNIV \<times> skl1_inv3)}
      a0i_commit A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle> \<union> Id,
      skl1_step3 Ra A B Nr gny
   {>R0sk1iai}"
apply (auto simp add: PO_rhoare_defs R0sk1iai_def)
apply (auto simp add: skl1_step3_def a0i_commit_def)
apply (frule skl1_inv3D, auto)+
done

lemma skl1_step4_refines_a0i_skip_i:
  "{R0sk1iai} Id, skl1_step4 Rb A B Ni gnx {>R0sk1iai}"
by (auto simp add: PO_rhoare_defs R0sk1iai_def, auto simp add: skl1_step4_def)

text \<open>refinement proof\<close>
lemmas skl1_trans_refines_a0i_trans_i =
  skl1_learn_refines_a0_ia_skip_i
  skl1_step1_refines_a0i_skip_i skl1_step2_refines_a0i_running_skip_i
  skl1_step3_refines_a0i_commit_skip_i skl1_step4_refines_a0i_skip_i

lemma skl1_refines_init_a0i_i [iff]:
  "init skl1 \<subseteq> R0sk1iai `` (init a0i)"
by (auto simp add: R0sk1iai_def a0i_defs skl1_defs)

lemma skl1_refines_trans_a0i_i [iff]:
  "{R0sk1iai \<inter> (UNIV \<times> (skl1_inv1 \<inter> skl1_inv2))} trans a0i, trans skl1 {> R0sk1iai}"
proof -
  let ?pre' = "R0sk1iai \<inter> (UNIV \<times> skl1_inv3)"
  show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
  proof (rule relhoare_conseq_left)
    show "?pre \<subseteq> ?pre'"
      using skl1_inv3_derived by blast
  next
    show "{?pre'} ?t1, ?t2 {> ?post}"
      apply (auto simp add: a0i_def skl1_def a0i_trans_def skl1_trans_def)
      prefer 2 using skl1_step2_refines_a0i_running_skip_i apply (simp add: PO_rhoare_defs, blast)
      prefer 2 using skl1_step3_refines_a0i_commit_skip_i apply (simp add: PO_rhoare_defs, blast)
      apply (blast intro!:skl1_trans_refines_a0i_trans_i)+
      done
  qed
qed

lemma obs_consistent_med01iai [iff]:
  "obs_consistent R0sk1iai med0sk1iai a0i skl1"
by (auto simp add: obs_consistent_def R0sk1iai_def med0sk1iai_def)

text \<open>refinement result\<close>
lemma skl1_refines_a0i_i [iff]:
  "refines
     (R0sk1iai \<inter> (reach a0i \<times> (skl1_inv1 \<inter> skl1_inv2)))
     med0sk1iai a0i skl1"
by (rule Refinement_using_invariants, auto)

lemma  skl1_implements_a0i_i [iff]: "implements med0sk1iai a0i skl1"
by (rule refinement_soundness) (fast)

(**************************************************************************************************)
subsection \<open>Derived invariants: injective agreement (@{term "Init"} authenticates @{term "Resp"})\<close>
(**************************************************************************************************)

lemma skl1_obs_iagreement_Init [iff]: "oreach skl1 \<subseteq> l1_iagreement_Init"
apply (rule external_invariant_translation
         [OF PO_a0i_obs_agreement _ skl1_implements_a0i_i])
apply (auto simp add: med0sk1iai_def l1_iagreement_Init_def a0i_agreement_def)
done

lemma skl1_iagreement_Init [iff]: "reach skl1 \<subseteq> l1_iagreement_Init"
by (rule external_to_internal_invariant [OF skl1_obs_iagreement_Init], auto)

(**************************************************************************************************)
subsection \<open>Refinement: injective agreement  (@{term "Resp"} authenticates @{term "Init"})\<close>
(**************************************************************************************************)

text \<open>Mediator function.\<close>
definition
  med0sk1iar :: "skl1_obs \<Rightarrow> a0i_obs"
where
  "med0sk1iar t \<equiv> \<lparr>a0n_state.signals = signalsResp t\<rparr>"

text \<open>Relation between states.\<close>
definition
  R0sk1iar :: "(a0i_state * skl1_state) set"
where
  "R0sk1iar \<equiv> {(s,s').
    a0n_state.signals s = signalsResp s'
    }"

text \<open>Protocol independent events.\<close>

lemma skl1_learn_refines_a0_ia_skip_r:
  "{R0sk1iar} Id, l1_learn m {>R0sk1iar}"
apply (auto simp add: PO_rhoare_defs R0sk1iar_def)
apply (simp add: l1_learn_def)
done

text \<open>Protocol events.\<close>

lemma skl1_step1_refines_a0i_skip_r:
  "{R0sk1iar} Id, skl1_step1 Ra A B {>R0sk1iar}"
by (auto simp add: PO_rhoare_defs R0sk1iar_def skl1_step1_def)

lemma skl1_step2_refines_a0i_skip_r:
  "{R0sk1iar} Id, skl1_step2 Rb A B Ni gnx {>R0sk1iar}"
by (auto simp add: PO_rhoare_defs R0sk1iar_def, auto simp add:skl1_step2_def)

lemma skl1_step3_refines_a0i_running_skip_r:
  "{R0sk1iar}
     a0i_running A B \<langle>NonceF (Ra$ni), Nr, Exp gny (NonceF (Ra$nx))\<rangle> \<union> Id,
     skl1_step3 Ra A B Nr gny
   {>R0sk1iar}"
by (auto simp add: PO_rhoare_defs R0sk1iar_def,
    simp_all add: skl1_step3_def a0i_running_def, auto)

lemma skl1_step4_refines_a0i_commit_skip_r:
  "{R0sk1iar \<inter> UNIV\<times>skl1_inv6}
      a0i_commit A B \<langle>Ni, NonceF (Rb$nr), Exp gnx (NonceF (Rb$ny))\<rangle> \<union> Id,
      skl1_step4 Rb A B Ni gnx
   {>R0sk1iar}"
apply (auto simp add: PO_rhoare_defs R0sk1iar_def)
apply (auto simp add: skl1_step4_def a0i_commit_def)
apply (auto dest!: skl1_inv6D [rotated 1])
done

text \<open>Refinement proof.\<close>

lemmas skl1_trans_refines_a0i_trans_r =
  skl1_learn_refines_a0_ia_skip_r
  skl1_step1_refines_a0i_skip_r skl1_step2_refines_a0i_skip_r
  skl1_step3_refines_a0i_running_skip_r skl1_step4_refines_a0i_commit_skip_r

lemma skl1_refines_init_a0i_r [iff]:
  "init skl1 \<subseteq> R0sk1iar `` (init a0i)"
by (auto simp add: R0sk1iar_def a0i_defs skl1_defs)

lemma skl1_refines_trans_a0i_r [iff]:
  "{R0sk1iar \<inter> (UNIV \<times> (skl1_inv4 \<inter> skl1_inv5))} trans a0i, trans skl1 {> R0sk1iar}"
proof -
  let ?pre' = "R0sk1iar \<inter> (UNIV \<times> skl1_inv6)"
  show ?thesis (is "{?pre} ?t1, ?t2 {>?post}")
  proof (rule relhoare_conseq_left)
    show "?pre \<subseteq> ?pre'"
      using skl1_inv6_derived by blast
  next
    show "{?pre'} ?t1, ?t2 {> ?post}"
      apply (auto simp add: a0i_def skl1_def a0i_trans_def skl1_trans_def)
      prefer 3 using skl1_step3_refines_a0i_running_skip_r apply (simp add: PO_rhoare_defs, blast)
      prefer 3 using skl1_step4_refines_a0i_commit_skip_r apply (simp add: PO_rhoare_defs, blast)
      apply (blast intro!:skl1_trans_refines_a0i_trans_r)+
      done
  qed
qed

lemma obs_consistent_med0sk1iar [iff]:
  "obs_consistent R0sk1iar med0sk1iar a0i skl1"
by (auto simp add: obs_consistent_def R0sk1iar_def med0sk1iar_def)

text \<open>Refinement result.\<close>

lemma skl1_refines_a0i_r [iff]:
  "refines
     (R0sk1iar \<inter> (reach a0i \<times> (skl1_inv4 \<inter> skl1_inv5)))
     med0sk1iar a0i skl1"
by (rule Refinement_using_invariants, auto)

lemma  skl1_implements_a0i_r [iff]: "implements med0sk1iar a0i skl1"
by (rule refinement_soundness) (fast)

(**************************************************************************************************)
subsection \<open>Derived invariants: injective agreement (@{term "Resp"} authenticates @{term "Init"})\<close>
(**************************************************************************************************)

lemma skl1_obs_iagreement_Resp [iff]: "oreach skl1 \<subseteq> l1_iagreement_Resp"
apply (rule external_invariant_translation
         [OF PO_a0i_obs_agreement _ skl1_implements_a0i_r])
apply (auto simp add: med0sk1iar_def l1_iagreement_Resp_def a0i_agreement_def)
done

lemma skl1_iagreement_Resp [iff]: "reach skl1 \<subseteq> l1_iagreement_Resp"
by (rule external_to_internal_invariant [OF skl1_obs_iagreement_Resp], auto)

end

subset_name: curated


TITLE: References on "not-quite" Finsler geometry?
QUESTION [8 upvotes]: In typical studies of Finsler geometry, the metric function $F: TM \to [0,\infty)$ is assumed to be smooth away from the zero section, and $F$ is assume to be sufficiently convex. Under these assumptions the geodesic spray is well-defined.

Formally writing down the Euler-Lagrange equation for the length minimizer one sees that to apply Picard-Lindelof we would want $F$ to be at least $C^{2,1}$ (for simplicity let's work on a local coordinate patch).
The convexity comes in because the ELE looks formally like
$$ A(\gamma, \dot{\gamma}) \cdot \ddot{\gamma} = N(\gamma, \dot{\gamma}) $$
where $\gamma$ is vector valued and $A$ is a matrix of coefficients; the convexity would ensure that $A$ is invertible.

Are there any articles/surveys that describes (preferably with examples), what exactly goes wrong to the geodesic structure of the manifold if either $F$ is too rough, or if $F$ has flat points? Naively, I would expect to see something like the following:

If $F$ is too rough, there may be some sort for "refraction" in the geodesic spray.
If $F$ is insufficiently convex (so that $A$ is singular), locally the geometry picks up some sub-Riemannian flavor.

Has this been examined in the literature?

REPLY [1 votes]: I think a starting point could be
Minguzzi, E., Convex neighborhoods for Lipschitz connections and sprays, Monatsh. Math. 177, No. 4, 569-625 (2015). ZBL1330.53021.
He does a detailed analysis of the Picard-Lindelöf argument and it works for any signature.


TITLE: How does Godel use diagonalization to prove the 1st incompleteness theorem?
QUESTION [2 upvotes]: I'm looking for an intuitive explanation of this without too much jargon as I am new to set theory. I understand Cantor's diagonal proof as well as the basic idea of 'this statement cannot be proved false,' I'm just struggling to link the two together.
Cheers

REPLY [2 votes]: Goedel provides a way of representing both mathematical formulas and finite sequences of mathematical formulas each as a single positive integer (by replacing each symbol with a number, and then using the numbers as exponents in the prime factorization).
If you can identify when a number corresponds to an axiom, and your "rules of inference" (valid logical arguments; such as Modus ponens, that allows you to deduce $Q$ if you have both $P\to Q$ and $P$) can be modeled by certain finite processes (you can have a computer do them), then there is a way of checking whether a given number corresponds to a formal proof, and so given two numbers, $N$ and $M$, you can check:

Is $N$ the number of a sequence of formulas?
If so, is the sequence of formulas a formal proof?
If so, is the last line of the proof the formula with number $M$?

If the answer to all three questions is 3, then you know that $N$ is the number of a proof for the formula with number $M$, and in particular that there is a proof for that formula.
Conversely, if you can prove a given formula $F$, then you can convert the proof into a number $N$, the formula into a number $M$, and then the number $N$ will be the number of a proof for the formula $M$.
This entire thing can be coded as a relationship between numbers. Just like you can say "$n$ is a multiple of $m$", or "$k$ is a power of $q$", or "$p$ is a prime", you can also say "$N$ is a proof for $M$." This is a statement that can be described purely in terms of the numerical properties of $N$ and $M$.
Goedel constructs a formula which essentially says: "There is no number $N$ which is a proof for the number you get by starting with the number $k$, and performing the following operations to it."
Now, this is itself a formula, so it has a number. It turns out that if you calculate the number of this formula, you get exactly the number you get by starting with the number $k$ and performing the operations described by the statement.
So even though the statement is, on its face, about number (it just says "There is no number $N$ which is in the relation of 'being a proof' for the number $f(k)$"), when you interpret the relationship 'being a proof' and you interpret the number $f(k)$, the statement is talking about itself.
One reason the process is sometimes called diagonalization is that you are essentially looking for a number $k$, corresponding to the value of the entire statement, which has $k=f(k)$ (so that the statement will "refer to itself"). That is, you are trying to find a number $k$ in the "diagonal" of the graph.


TITLE: Why if $x = \frac{q}{p^n}, $ then there are two expansions for $x$? (documented duplicate)
QUESTION [0 upvotes]: This problem is very well documented here at the MSE, e.g. Expansions of a Real Number $x$

Let $p$ be a natural number greater than $1$, and let $x$ be a real number with $0\leq x\leq 1$. Show that there is a sequence of integers $\{a_{n}\}$ with $0\leq a_{n}<p$ for each $n$ such that $$x=\sum_{n=1}^{\infty}\frac{a_{n}}{p^{n}}$$ and that the sequence is unique except when $x$ is of the form $\frac{q}{p^{n}}$, $0<p<q$, in which case there are exactly two such sequences.

But I am struggling to understand something even more basic that those answers, because I don't really get why if $x = \frac{q}{p^n}, $ then there are two expansions for $x$. I don't see why this takes into account the two decimal expansions of 1 in base 10, for example (Characterization of non-unique decimal expansions). So I am lost at seeing why taking $x = \frac{q}{p^n}$ generalizes that behaviour of the 2 possible expansions.

REPLY [1 votes]: A favorite example of this phenomenon, which you mentioned in your question, is the equation
$$x = 1 = .99999\ldots
$$
Although this does not fit your question, where it is required that $x \in (0,1)$, let me alter the example a tiny bit:
$$x=.1 = .099999\ldots
$$
On the left hand side of this equation one has $x=\frac{q}{p^n}$ where $q=1$, $p=10$, and $n=1$.
And on the right hand side one has the alternate expression
$$x = \sum_{i=1}^\infty \frac{a_n}{10^n}
$$
where $a_1=0$ and $a_2=a_3=\cdots=9$.


TITLE: What would be called as the shape of $xy=10$ in 3-dimensional space?
QUESTION [0 upvotes]: As title says, what would be called as the shape of $xy=10$ in 3-dimensional space? It doesn't seem to be paraboloid nor hyperboloid...

REPLY [4 votes]: Such a shape is often called a hyperbolic cylinder, which as you say is neither a paraboloid nor a hyperboloid.
As a general rule a quadric in 3 dimensions whose equation does not involve one variable (like $z$) will be called a cylinder. For example $x^2 + 2y^2 = 1$ forms an elliptic cylinder, as the equation defines an ellipse in 2 dimensional space.
Addition to respond to comment on question:
To see the equivalence with the standard form for a hyperbolic cylinder, make the change of variables $x \mapsto X + Y$, and $y\mapsto X-Y$, then $xy=10$ becomes $(X+Y)(X-Y)=10$ or $X^2 - Y^2 =10$.


TITLE: Diferential equation with $\sinh$
QUESTION [0 upvotes]: I'm trying to solve the following differential equation for $z\in [0,\infty]$:
\begin{equation}
\frac{\partial^{2}\phi}{\partial z^{2}}=A\sinh\left[B\phi\left(z\right)\right]
\end{equation}
with boundary condition $\phi(z=0)=W$ and $\frac{\partial\phi(z)}{\partial z}|_{z\rightarrow \infty} = 0$.
I started solving this by multiplying both sides by $\frac{\partial\phi(z)}{\partial z}$ and integrating in z. This gave me
\begin{equation}
\frac{1}{2}\left(\frac{\partial\phi}{\partial z}\right)^{2}=\frac{1}{B}\cosh\left[B\phi\left(z\right)\right]+C
\end{equation}
However, I have no idea how to proceed from here. I initially thought about squaring everything, but it seems only more complicate to integrate $\sqrt{\cosh[] + C}$. Any ideas?
Thanks!
I have a book that says there is a closed analytical formula for that

REPLY [2 votes]: Starting with the equation
$$\frac{d^{2}\phi}{dz^{2}}=A\sinh\left(B\phi\right)$$ switch variables to get
$$-\frac{z''}{[z']^3}=A\sinh\left(B\phi\right)$$ So, reduction of order $(p=z')$
$$-\frac{p'}{p^3}=A\sinh\left[B\phi\right]\implies p=\pm\frac{\sqrt{B}}{\sqrt{2A \cosh (B \phi)+k_1}}$$ The problem is that now we shall face elliptic integrals.
Before any simplification (still ignoring the signs of $A$, $B$ and $k_1$
$$z+c_2=\pm\frac{2 i \sqrt{\frac{2 A \cosh (B \phi)+k_1}{2 A+k_1}}}{\sqrt{B} \sqrt{2 A \cosh (B
   \phi)+k_1}}\, F\left(i\frac{ B \phi}{2}|\frac{4 A}{2 A+k_1}\right)$$
Inversing the monster would not be very pleasant.