245255

# On approximation of solutions of operator-differential equations with their
entire solutions of exponential type

V. M. Gorbachuk  National Technical University ”KPI”, 37 Peremogy Prosp.,
Kyiv, 06256, Ukraine<EMAIL_ADDRESS>
(Date: 01/04/2016; Revised 12/04/2016)

###### Abstract.

We consider an equation of the form $y^{\prime}(t)+Ay(t)=0,\ t\in[0,\infty)$,
where $A$ is a nonnegative self-adjoint operator in a Hilbert space. We give
direct and inverse theorems on approximation of solutions of this equation
with its entire solutions of exponential type. This establishes a one-to-one
correspondence between the order of convergence to $0$ of the best
approximation of a solution and its smoothness degree. The results are
illustrated with an example, where the operator $A$ is generated by a second
order elliptic differential expression in the space $L_{2}(\Omega)$ (the
domain $\Omega\subset\mathbb{R}^{n}$ is bounded with smooth boundary) and a
certain boundary condition.

###### Key words and phrases:

Hilbert and Banach spaces, differential-operator equation, weak solution,
$C_{0}$-semigroup of linear operators, entire vector-valued function, entire
vector-valued function of exponential type, the best approximation, direct and
inverse theorems of the approximation theory.

###### 2000 Mathematics Subject Classification:

Primary 34G10

1. Let $A$ be a nonnegative self-adjoint operator in a Hilbert space $\mathfrak{H}$ with a scalar product $(\cdot,\cdot)$. Denote by $C_{\\{1\\}}(A)$ the set of all its exponential type entire vectors (see [4]), namely,

$\displaystyle C_{\\{1\\}}(A)=\Big{\\{}f\in
C^{\infty}(A)=\bigcap_{n=1}^{\infty}\mathcal{D}(A^{n})\big{|}\exists\alpha>0,\
\exists c$ $\displaystyle=c(f)>0:$ $\displaystyle\|A^{n}f\|$
$\displaystyle\leq c\alpha^{n},\
n\in\mathbb{N}_{0}=\mathbb{N}\cup\\{0\\}\Big{\\}}$

(everywhere in the sequel $c$ denotes various numerical constants
corresponding to the situations under consideration, $\mathcal{D}(A)$ is a
domain of $A$ and $\|f\|=\sqrt{(f,f)}$). The number

$\sigma(f,A)=\inf\left\\{\alpha>0\bigl{|}\exists c>0,\ \forall
n\in\mathbb{N}_{0}:\|A^{n}f\|\leq c\alpha^{n}\right\\}$

is called the type of the vector $f$ with respect to the operator $A$.

As has been shown in [3] that

$C_{\\{1\\}}(A)=\left\\{f\in\mathfrak{H}\bigl{|}f=E(\lambda)g,\
\forall\lambda>0,\ \forall g\in\mathfrak{H}\right\\},$

where $E(\lambda)=E([0,\lambda])$ is the spectral measure of $A$.

Now, consider the equation

$y^{\prime}(t)+Ay(t)=0,\quad t\in\mathbb{R}_{+}=[0,\infty).$ $None$

By a weak solution of this equation we mean a continuous vector-valued
function $y(t):\mathbb{R}_{+}\mapsto\mathfrak{H}$ such that for any
$t\in\mathbb{R}_{+}$,

$\int_{0}^{t}y(s)\,ds\in\mathcal{D}(A)\quad\text{and}\quad
y(t)=-A\int_{0}^{t}y(s)\,ds+y(0).$

Denote by $S$ the set of all weak solutions of (1). As it was established in
[1],

$S=\left\\{y(t):\mathbb{R}_{+}\mapsto\mathfrak{H}\big{|}\
y(t)=e^{-At}f,f\in\mathfrak{H}\right\\},$ $None$

where

$e^{-At}f=\int_{0}^{\infty}e^{-\lambda t}\,dE(\lambda)f.$

Note that the set of all strong (or simply) solutions of (1) is given by
formula (2) with $f$ ranging over whole $\mathcal{D}(A)$.

It is not difficult to verify that $S$ is a Hilbert space with the norm

$\|y\|_{S}=\sup_{t\in\mathbb{R}_{+}}\left\|e^{-At}f\right\|=\|f\|.$ $None$

If the operator $A$ is bounded, then each weak solution $y(t)$ of equation (1)
can be extended to an entire $\mathfrak{H}$-valued vector function $y(z)$ of
exponential type,

$\sigma(y)=\inf\left\\{\alpha>0:\|y(z)\|\leq ce^{\alpha|z|}\right\\}.$

But it is not the case if $A$ is unbounded. The set $S_{0}$ of all weak
solutions of (1) admitting an extension to an entire vector function of
exponential type is described by the following theorem.

###### Theorem 1

A weak solution $y(t)$ of equation (1) belongs to $S_{0}$ if and only if it
can be represented in form (2) with $f\in C_{\\{1\\}}(A)$. The set $S_{0}$ is
dense in $S$, and $\sigma(y)=\sigma(f,A)$.

###### Proof.

Let $f\in C_{\\{1\\}}(A)$. Then $f=E(\alpha)f$, where $\alpha=\sigma(f,A)$. By
(2),

$y(t)=\int_{0}^{\alpha}e^{-\lambda t}\,dE(\lambda)f.$

From this it follows that $y(t)$ can be extended to an entire vector-valued
function $y(z)$ and

$\|y(z)\|^{2}=\int_{0}^{\alpha}e^{-2\text{Re}z\lambda}\,d(E(\lambda)f,f)\leq
e^{2\sigma(f,A)|z|}\|f\|^{2},$

that is, $y(z)$ is an entire $\mathfrak{H}$-valued function of exponential
type $\sigma(y)\leq\sigma(f,A)$.

Conversely, if $y(t)=e^{-At}f$ admits an extension to an entire vector-valued
function of exponential type $\sigma(y)$, then, by virtue of

$\|y(-t)\|^{2}=\int_{0}^{\infty}e^{2\lambda t}\,d(E(\lambda)f,f)\leq
ce^{2\sigma(y)t},\quad t\geq 0,$

we have

$\int_{\sigma(y)}^{\infty}e^{2t(\lambda-\sigma(y))}\,d(E(\lambda)f,f)\leq c.$

Passing to the limit under the integral sign as $t\to\infty$, we conclude, on
the basis of the Fatou theorem, that the measure generated by the monotone
function $(E(\lambda)f,f)$ is concentrated on the interval $[0,\sigma(y)]$.
Hence, $\sigma(f,A)\leq\sigma(y)$.

Density of $S_{0}$ in $S$ follows from the density in $\mathfrak{H}$ of the
set $\\{E([0,\alpha])f,\forall\alpha>0,\forall f\in\mathfrak{H}\\}$. ∎

In view of Theorem 1, it is reasonable to ask whether it is possible to
approximate an arbitrary weak solution of equation (1) with its exponential
type entire solutions. An answer to the question is given below. We prove
direct an inverse theorems which ascertain the relationship between the degree
of smoothness of a solution and the rate of convergence to $0$ of its best
approximation. In doing so, the operator approach developed in [7, 4, 5] plays
an important role.

2. Recall some definitions and notations of the approximation theory required to formulate further results.

For $y\in S$ and a number $r>0$, we put

$\mathcal{E}_{r}(y)=\inf_{y_{0}\in S_{0}:\sigma(y_{0})\leq r}\|y-y_{0}\|_{S}.$

Thus, $\mathcal{E}_{r}(y)$ is the best approximation of a weak solution $y(t)$
of equation (1) with its entire solutions of exponential type not exceeding
$r$. If $y$ is fixed, the function $\mathcal{E}_{r}(y)$ does not increase and,
since $\overline{{S}_{0}}=S,\ \mathcal{E}_{r}(y)\to 0$ as $r\to\infty$.

For $f\in\mathfrak{H}$, set also

$\mathcal{E}_{r}(f,A)=\inf_{f_{0}\in C_{\\{1\\}}(A):\sigma(f_{0},A)\leq
r}\|f-f_{0}\|=\|(I-E(r))f\|.$

If $y(t)=e^{-At}f$, then, by virtue of (3),

$\mathcal{E}_{r}(y)=\mathcal{E}_{r}(f,A).$ $None$

Besides, for any $k\in\mathbb{N}_{0}$, we introduce the function

$\omega_{k}(t,y)=\sup_{|h|\leq
t}\sup_{s\in\mathbb{R}_{+}}\Big{\|}\sum_{j=0}^{k}(-1)^{k-j}C_{k}^{j}y(s+jh)\Big{\|},\quad
k\in\mathbb{N};\quad\omega_{0}(t,y)\equiv\|y\|_{S},\quad t>0.$

Taking into account (2) and the equality $e^{-As}y(t)=y(t+s)$, we conclude
that

$\forall k\in\mathbb{N}_{0}:\omega_{k}(t,y)=\sup_{|h|\leq
t}\left\|\left(e^{-Ah}-I\right)^{k}y\right\|_{S}$

($I$ is the identity operator).

The following theorem establishes a relation between $\mathcal{E}_{r}(y)$ and
$\omega_{k}(t,y)$, and it is an analog of the well-known Jackson’s theorem on
approximation of a continuous periodic function by trigonometric polynomials.

###### Theorem 2

Let $y\in S$. Then

$\forall k\in\mathbb{N},\ \exists c_{k}>0:\mathcal{E}_{r}(y)\leq
c_{k}\omega_{k}\left(\frac{1}{r},y\right),\quad r>0.$ $None$

###### Proof.

By (2), $y(t)=e^{-At}f,\ f\in\mathfrak{H}$. From (3), (4), it follows that

$\displaystyle\omega_{k}^{2}(t,y)=$ $\displaystyle\sup_{0\leq s\leq
t}\left\|\left(e^{-As}-I\right)^{k}y\right\|_{S}^{2}\geq\left\|\left(e^{-At}-I\right)^{k}y\right\|_{S}^{2}=\sup_{s\in\mathbb{R}_{+}}\left\|\left(e^{-At}-I\right)^{k}e^{-As}f\right\|^{2}$
$\displaystyle=$
$\displaystyle\left\|\left(e^{-At}-I\right)^{k}f\right\|^{2}=\int_{0}^{\infty}\left(e^{-\lambda
t}-1\right)^{2k}\,d(E(\lambda)f,f)$ $\displaystyle\geq$
$\displaystyle\int_{\frac{1}{t}}^{\infty}\left(e^{-\lambda
t}-1\right)^{2k}\,d(E(\lambda)f,f)\geq\left(1-e^{-1}\right)^{2k}\mathcal{E}_{\frac{1}{t}}(y).$

So,

$\forall
t>0:\mathcal{E}_{\frac{1}{t}}(y)\leq\left(1-e^{-1}\right)^{k}\omega_{k}(t,y).$

Setting $r=\frac{1}{t}$ and $c_{k}=\left(1-e^{-1}\right)^{k}$, we obtain (5).
∎

Denote by $C^{n}(\mathbb{R}_{+},\mathfrak{H})$ the set of all $n$ times
continuously differentiable on $\mathbb{R}_{+}$ $\mathfrak{H}$-valued vector-
valued functions. Since the operator $A$ is closed, the inclusion $y\in S\cap
C^{n}(\mathbb{R}_{+},\mathfrak{H})$ implies that $y^{(k)}\in S,\
k=1,2,\dots,n$.

###### Theorem 3

Suppose that $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H}),\ n\in\mathbb{N}_{0}$.
Then

$\forall r>0,\ \forall
k\in\mathbb{N}_{0}:\mathcal{E}_{r}(y)\leq\frac{c_{k+n}}{r^{n}}\omega_{k}\left(\frac{1}{r},y^{(n)}\right),$

where the constants $c_{k}$ are the same as in Theorem 2.

###### Proof.

Let $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H}),r>0$ and $0\leq t<\frac{1}{r}$.
Using properties of a contraction $C_{0}$-semigroup, we get

$\left\|\left(e^{-At}-I\right)^{k+n}y(s)\right\|=\left\|\left(e^{-At}-I\right)^{n}\left(e^{-At}-I\right)^{k}y(s)\right\|$
$\leq\int_{0}^{t}\dots\int_{0}^{t}\left\|e^{-A(s_{1}+\dots
s_{n})}\right\|\left\|\left(e^{-At}-I\right)^{k}A^{n}y(s)\right\|\,ds_{1}\dots
ds_{n}$ $\leq t^{n}\left\|\left(e^{-At}-I\right)^{k}y^{(n)}(s)\right\|,$

whence

$\omega_{k+n}\left(\frac{1}{r},y\right)\leq\frac{1}{r^{n}}\omega_{k}\left(\frac{1}{r},y^{(n)}\right)$

and, because of (5),

$\mathcal{E}_{r}(y)\leq
c_{k+n}\omega_{k+n}\left(\frac{1}{r},y\right)\leq\frac{c_{k+n}}{r^{n}}\omega_{k}\left(\frac{1}{r},y^{(n)}\right),$

which is what had to be proved. ∎

Setting, in Theorem 3, $k=0$ and taking into account that
$\omega_{0}(t,y^{(n)})=\|y^{(n)}\|_{S}$, we arrive at the following assertion.

###### Corollary 1

Let $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H}),\ n\in\mathbb{N}$. Then

$\forall r>0:\mathcal{E}_{r}(y)\leq\frac{c_{n}}{r^{n}}\|y^{(n)}\|_{S}.$

For numbers $h>0$ and $k\in\mathbb{N}_{0}$, we put

$\Delta_{h}^{k}=\left(e^{-Ah}-I\right)^{k}=\sum_{j=0}^{k}(-1)^{k-j}C_{k}^{j}e^{-Ajh}.$

###### Lemma 1

If $y\in S_{0}$ and $\sigma(y)=\alpha$, then

$\forall h>0,\ \forall
k,n\in\mathbb{N}_{0}:\left\|\Delta_{h}^{k}y^{(n)}\right\|_{S}\leq(\alpha
h)^{k}\alpha^{n}\|y\|_{S}.$ $None$

Proof. It follows from the inequality

$1-\lambda h-e^{-\lambda h}\leq 0\quad(\lambda\geq 0,\ h>0)$

and the representation $y(t)=e^{-At}f$ that

$\displaystyle\left\|\Delta_{h}^{k}y^{(n)}\right\|^{2}=$
$\displaystyle\int_{0}^{\alpha}\left(1-e^{-\lambda h}\right)^{2k}e^{-2\lambda
t}\lambda^{2n}\,d(E(\lambda)f,f)$ $\displaystyle\leq$
$\displaystyle\int_{0}^{\alpha}(\lambda
h)^{2k}\lambda^{2n}\,d(E(\lambda)f,f)\leq(\alpha h)^{2k}\alpha^{2n}\|f\|.$

This and (3) imply

$\qquad\qquad\qquad\qquad\quad\left\|\Delta_{h}^{k}y^{(n)}\right\|_{S}\leq(\alpha
h)^{k}\alpha^{n}\|f\|=(\alpha
h)^{k}\alpha^{n}\|y\|_{S}.\qquad\qquad\qquad\qquad\quad\qed$

Taking in (6) $k=0$, we arrive at an analog of Bernstein’s inequality, namely

$\forall n\in\mathbb{N}:\left\|y^{(n)}\right\|\leq\alpha^{n}\|y\|_{S}.$ $None$

Putting there $n=0$, we obtain

$\forall n\in\mathbb{N}:\left\|\Delta_{h}^{k}y\right\|_{S}\leq(\alpha
h)^{k}\|y\|_{S}=(\alpha h)^{k}\alpha^{n}\|y\|_{S}.$

It should be noted that the inequality

$\mathcal{E}_{r}(y)\leq\frac{c}{r^{n}},\quad r>0,\quad n\in\mathbb{N},$ $None$

does not yet imply the inclusion $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H})$.
Nevertheless, the following statement, inverse to Theorem 3, is valid.

###### Theorem 4

Suppose that $y\in S$, and let $\omega(t)$ be a continuity module type
function, i.e.,

$1)\ \omega(t)$ is continuous and nondecreasing on $\mathbb{R}_{+}$;

$2)\ \omega(0)=0$;

$3)\ \exists c>0,\ \forall t>0:\omega(2t)\leq c\omega(t)$.
In order that $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H})$, it is sufficient that
there exist a number $m>0$ such that

$\forall r>0,\ \forall
n\in\mathbb{N}:\mathcal{E}_{r}(y)\leq\frac{m}{r^{n}}\omega\left(\frac{1}{r}\right).$
$None$

###### Proof.

Assume that, for $y\in S$, condition (9) is fulfilled. Then there exists a
sequence $y_{i}\in S:\sigma(y_{i})<2^{i}\ (i\in\mathbb{N})$ such that

$\|y-y_{i}\|_{S}\to 0\quad\text{as}\quad i\to\infty.$

In view of (7) and the inequality $\sigma(y_{i}-y_{i-1})<2^{i}\
(i\in\mathbb{N})$, we have

$\displaystyle\left\|y_{i}^{(n)}-y_{i-1}^{(n)}\right\|_{S}\leq$ $\displaystyle
2^{in}\|y_{i}-y_{i-1}\|_{S}\leq 2^{in}(\|y-y_{i}\|_{S}+\|y-y_{i-1}\|_{S})$
$\displaystyle\leq$ $\displaystyle
2^{in}\left(\frac{m}{2^{in}}\omega\left(\frac{1}{2^{i}}\right)+\frac{m}{2^{(i-1)n}}\omega\left(\frac{1}{2^{i-1}}\right)\right).$

From this it follows that

$\left\|y_{i}^{(n)}-y_{i-1}^{(n)}\right\|_{S}\leq
m2^{n}\left(\frac{1}{2^{n}}+c\right)\omega\left(\frac{1}{2^{i}}\right),$

and therefore

$\left\|y_{i}^{(n)}-y_{i-1}^{(n)}\right\|_{S}\to 0\quad\text{as}\quad
i\to\infty.$

Since the space $S$ is complete, there exists $\widetilde{y}\in S$ such that

$\left\|y_{i}^{(n)}-\widetilde{y}\right\|_{S}\to 0\quad\text{when}\quad
i\to\infty.$

Thus, $y_{i}\to y,\ y_{i}^{(n)}\to\widetilde{y}\ (i\to\infty)$ in the space S.
Taking into account that the operator $\frac{d^{n}}{dt^{n}}$ is closed in $S$,
we conclude that $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H})$ and
$y^{(n)}(t)\equiv\widetilde{y}(t)$. ∎

Replacing in inequality (8) $n$ by $n+\varepsilon$ and thus strengthening it,
we shall arrive at the following consequence.

###### Corollary 2

Let, for $y\in S$,

$\exists c>0,\
\exists\varepsilon>0:\mathcal{E}_{r}(y)\leq\frac{c}{r^{n+\varepsilon}}.$

Then $y\in C^{n}(\mathbb{R}_{+},\mathfrak{H})$.

3. Now let $\\{m_{n}\\}_{n\in\mathbb{N}_{0}}$ be a nondecreasing sequence of numbers (there is no loss of generality in assuming that $m_{0}=1$). We put

$C_{\\{m_{n}\\}}=C_{\\{m_{n}\\}}(\mathbb{R}_{+},\mathfrak{H})=\bigcup_{\alpha>0}C_{m_{n}}^{\alpha},\quad
C_{(m_{n})}=C_{(m_{n})}(\mathbb{R}_{+},\mathfrak{H})=\bigcap_{\alpha>0}C_{m_{n}}^{\alpha},$

where

$\displaystyle C_{m_{n}}^{\alpha}$
$\displaystyle=C_{m_{n}}^{\alpha}(\mathbb{R}_{+},\mathfrak{H})$
$\displaystyle=\Big{\\{}y\in
C^{\infty}(\mathbb{R}_{+},\mathfrak{H})\bigl{|}\exists c=c(y)>0,\ \forall
k\in\mathbb{N}_{0}:\sup_{t\in\mathbb{R}_{+}}\Big{\|}y^{(k)}(t)\Big{\|}\leq
cm_{k}\alpha^{k}\Big{\\}}$

is a Banach space with respect to the norm

$\|y\|_{C_{m_{n}}^{\alpha}}=\sup_{k\in\mathbb{N}}\frac{\sup_{t\in\mathbb{R}_{+}}\left\|y^{(k)}(t)\right\|}{\alpha^{k}m_{k}}.$

The spaces $C_{\\{m_{n}\\}}$ and $C_{(m_{n})}$ are equipped with the
topologies of inductive and projective limits of the spaces
$C_{m_{n}}^{\alpha}$, respectively. Note that the spaces $C_{\\{n!\\}},\
C_{(n!)}\ (m_{n}=n!)$ and $C_{\\{1\\}}\ (m_{n}\equiv 1)$ are nothing that,
respectively, the spaces of bounded on $\mathbb{R}_{+}$ with all their
derivatives analytic, entire, and entire of exponential type
$\mathfrak{H}$-valued vector functions.

In what follows, we assume in addition that $\\{m_{n}\\}_{n\in\mathbb{N}_{0}}$
satisfies the condition

$\forall\alpha>0,\ \exists c=c(\alpha):m_{n}\geq c\alpha^{n}$ $None$

and put

$\tau(\lambda)=\sum_{n=0}^{\infty}\frac{\lambda^{n}}{m_{n}}.$ $None$

It is clear that $\tau(\lambda)$ is entire, $\tau(\lambda)\geq 1$ for
$\lambda\geq 0$, and $\tau(\lambda)\uparrow\infty$ as $\lambda\to\infty$.

###### Theorem 5

Suppose the condition

$\exists c>0,\ \exists h>1,\ \forall n\in\mathbb{N}_{0}:m_{n+1}\leq
ch^{n}m_{n}$ $None$

to be fulfilled for the sequence $\\{m_{n}\\}_{n\in\mathbb{N}_{0}}$. Then the
following equivalence relations hold:

$\begin{array}[]{rcl}y\in
C^{\infty}(\mathbb{R}_{+},\mathfrak{H})&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(y)=O\left(\frac{1}{r^{\alpha}}\right)\quad(r\to\infty),\\\
y\in
C_{\\{m_{n}\\}}&\Longleftrightarrow&\exists\alpha>0:\mathcal{E}_{r}(y)=O\left(\tau^{-1}(\alpha
r)\right)\quad(r\to\infty),\\\ y\in
C_{(m_{n})}&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(y)=O\left(\tau^{-1}(\alpha
r)\right)\quad(r\to\infty)\\\ \end{array}$

$(\tau(\lambda)$ is defined by (11)).

###### Proof.

Let $C^{\infty}(A)$ denote the set of all infinitely differentiable vectors of
the operator $A$,

$C^{\infty}(A)=\bigcap_{n\in\mathbb{N}_{0}}\mathcal{D}(A^{n}).$

For a number $\alpha>0$, we put

$C_{m_{n}}^{\alpha}(A)=\left\\{f\in C^{\infty}(A)\bigl{|}\exists c=c(f)>0,\
\forall n\in\mathbb{N}_{0}:\left\|A^{n}f\right\|\leq
c\alpha^{n}m_{n}\right\\}.$

The set $C_{m_{n}}^{\alpha}(A)$ is a Banach space with respect to the norm

$\|f\|_{C_{m_{n}}^{\alpha}(A)}=\sup_{n\in\mathbb{N}_{0}}\frac{\left\|A^{n}f\right\|}{\alpha^{n}m_{n}}.$

Then

$C_{\\{m_{n}\\}}(A)=\bigcup_{\alpha>0}C_{m_{n}}^{\alpha}(A)\ \text{and}\
C_{(m_{n})}(A)=\bigcap_{\alpha>0}C_{m_{n}}^{\alpha}(A)$

are linear locally convex spaces with topologies of the inductive and the
projective limits, respectively.

Let

$\mathcal{E}_{r}(f,A)=\inf_{f_{0}\in C_{\\{1\\}}(A)}\|f-f_{0}\|.$

As it has been shown in [4], the following equivalence relations take place:

$\begin{array}[]{rcl}f\in
C^{\infty}(A)&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(f,A)=O\left(\frac{1}{r^{\alpha}}\right)\quad(r\to\infty),\\\
f\in
C_{\\{m_{n}\\}}(A)&\Longleftrightarrow&\exists\alpha>0:\mathcal{E}_{r}(f,A)=O\left(\tau^{-1}(\alpha
r)\right)\quad(r\to\infty),\\\ f\in
C_{(m_{n})}(A)&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(f,A)=O\left(\tau^{-1}(\alpha
r)\right)\quad(r\to\infty).\\\ \end{array}$ $None$

Consider the map $F:\mathfrak{H}\mapsto S$,

$Ff=e^{-At}f.$

Since, for $y\in S$, there exists a unique vector $f\in\mathfrak{H}$ such that
$y=e^{-At}f$, this transformation is one-to-one. From (3) it follows that $F$
maps $\mathfrak{H}$ onto $S$ isometrically and

$F\left(C^{\infty}(A)\right)=C^{\infty}(\mathbb{R}_{+},\mathfrak{H}),\quad
F\left(C_{\\{m_{n}\\}}(A)\right)=C_{\\{m_{n}\\}},\quad
F\left(C_{(m_{n})}(A)\right)=C_{(m_{n})}.$ $None$

The proof of the theorem follows from (13), (14) because of
$\mathcal{E}_{r}(f,A)=\mathcal{E}_{r}\left(e^{-At}f\right)$. ∎

If $m_{n}=n^{n\beta}\ (\beta>0)$, then $\tau(r)=e^{-r^{1/\beta}}$ and Theorem
5 yields the following assertion.

###### Corollary 3

The following equivalence relations are valid:

$\begin{array}[]{rcl}y\in
C_{\\{n^{n\beta}\\}}(A)&\Longleftrightarrow&\exists\alpha>0:\mathcal{E}_{r}(y)=O\left(e^{-\alpha
r^{1/\beta}}\right)\quad(r\to\infty),\\\ y\in
C_{(n^{n\beta})}(A)&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(y)=O\left(e^{-\alpha
r^{1/\beta}}\right)\quad(r\to\infty).\\\ \end{array}$

Recall that an entire $\mathfrak{H}$-valued vector function $x(\lambda)$ has a
finite order of growth if

$\exists\gamma>0,\
\forall\lambda\in\mathbb{C}:\|x(\lambda)\|\leq\exp(|\lambda|^{\gamma}).$

The greatest lower bound $\rho(x)$ of such $\gamma$ is the order of
$x(\lambda)$. The type of an entire vector-valued function $x(\lambda)$ of an
order $\rho$ is determined as

$\sigma(x)=\inf\left\\{a>0:\|x(\lambda)\|\leq\exp(a|\lambda|^{\rho})\right\\}.$

Since the semigroup $\left\\{e^{-At}\right\\}_{t\geq 0}$ is analytic, every
weak solution $y(t)$ of equation (1) is analytic on $(0,\infty)$. It is not
difficult to show that it is analytic on $[0,\infty)$ if and only if $y\in
C_{\\{n^{n}\\}}$.

By Corollary 3,

$\exists\alpha>0:\mathcal{E}_{r}(y)=O\left(e^{-\alpha
r}\right)\quad(r\to\infty).$

As for the extendability of $y(t)$ to an entire vector function of order
$\rho$ and finite type, the answer to the question gives the next theorem.

###### Theorem 6

In order that a weak solution of equation (1) admit an extension to an entire
$\mathfrak{H}$-valued vector function $y(z)$, it is necessary and sufficient
that

$\forall\alpha>0:\mathcal{E}_{r}(y)=O\left(e^{-\alpha
r}\right)\quad(r\to\infty).$ $None$

The extension $y(z)$ is of finite order $\rho$ and finite type if and only if

$\exists\alpha>0:\mathcal{E}_{r}(y)=O\left(e^{-\alpha
r^{1/\beta}}\right)\quad(r\to\infty),$

where $\beta$ and $\rho$ are connected with each other by the formula

$\beta=\frac{\rho-1}{\rho}<1.$

Note that we may always suppose $\rho>1$. Indeed, if $\rho\leq 1$ and the type
is finite, then $y\in S_{0}$ and it has no sense to approximate a solution
from $S_{0}$ by solutions from the same space.

Proof of Theorem 6. Let $y(t)$ be a weak solution of equation (1). By
Corollary 3, $y\in C_{(n^{n})}$, so $y(t)$ admits an extension to an entire
vector function if and only if relation (15) is fulfilled.

Assume that $y(t)$ admits an extension to an entire $\mathfrak{H}$-valued
vector function $y(z)$ which has an order $\rho$ and a finite type $\sigma$.
Then

$\forall\sigma_{1}>\sigma,\ \exists c=c(\sigma_{1}):\|y(z)\|\leq
ce^{\sigma_{1}|z|^{\rho}}.$

Hence,

$\forall r>0,\ \forall
n\in\mathbb{N}_{0}:\left\|y^{(n)}(z)\right\|\leq\frac{n!}{2\pi}\int_{|z-\zeta|=r}\frac{\|y(\zeta)\|}{|z-\zeta|^{n+1}}\,d\zeta\leq\frac{c\sigma_{1}n!}{r^{n}}\exp\left(2\sigma_{1}r^{\rho}\right).$

Taking into account that the function
$\frac{\exp\left(ar^{\rho}\right)}{r^{n}}$ reaches its minimum at the point
$\left(\frac{n}{a\rho}\right)^{1/\rho}$ and using Stirling’s formula

$n!=n^{n}e^{-n}\sqrt{2\pi
n}\left(1+O\left(\frac{1}{n}\right)\right)\quad(n\to\infty),$

we get

$\left\|y^{(n)}(z)\right\|\leq
c\left(2e^{1-\rho}\sigma_{1}\rho\right)^{\frac{1}{\rho}}n^{\frac{\rho-1}{\rho}n},$

which shows that $y\in C_{\\{n^{n\beta}\\}}$, where

$\beta\leq\frac{\rho-1}{\rho}\Longleftrightarrow\rho\geq\frac{1}{1-\beta},\quad\beta<1.$
$None$

By Corollary 3,

$\exists\alpha>0:\mathcal{E}_{r}(y)=O\left(e^{-\alpha
r^{1/\beta}}\right)\quad(r\to\infty).$ $None$

Conversely, let (17) hold true. Then Corollary 3 implies that $y\in
C_{\\{n^{n\beta}\\}}\ (0<\beta<1)$ is an entire vector-valued function and it
can be represented by the series
$\sum_{k=0}^{\infty}\frac{y^{(k)}(0)}{k!}z^{k}$. For its order of growth
$\rho$ we have

$\rho=\varlimsup_{n\to\infty}\frac{n\ln
n}{\ln\frac{n!}{\left\|y^{(n)}(0)\right\|}}\leq\varlimsup_{n\to\infty}\frac{n\ln
n}{\ln\left(n!n^{-n\beta}\right)}=\frac{1}{1-\beta},$

that is,

$\rho\leq\frac{1}{1-\beta}.$ $None$

It follows from (16) and (18) that

$\qquad\qquad\qquad\qquad\qquad\qquad\quad\rho=\frac{1}{1-\beta},\quad
0<\beta<1.\qquad\qquad\qquad\qquad\qquad\qquad\quad\qed$

4. The direct and inverse theorems of the approximation theory are usually formulated for Banach space. Proving them is slightly more complex than in the case of a Hilbert space. Below we show how, for example, Theorem 5 can be reformulated in a Banach space. To this end we introduce the following notations:

$\mathfrak{H}^{n}=\mathcal{D}(A^{n}),\|f\|_{\mathfrak{H}^{n}}=\left(\|f\|^{2}+\|A^{n}f\|^{2}\right)^{1/2}.$

The space $\mathfrak{H}^{n}$ is continuously and densely embedded into
$\mathfrak{H}$. Denote by $\mathfrak{H}^{-n}$ the completion of $\mathfrak{H}$
in the norm $\|f\|_{\mathfrak{H}^{-n}}=\left\|\left(A+I\right)^{-n}f\right\|$,
the so called negative space associated with the positive space
$\mathfrak{H}^{n}$ in the chain

$\mathfrak{H}^{n}\subseteq\mathfrak{H}\subseteq\mathfrak{H}^{-n}$

(see [2]). By a suitable choice of the norms in $\mathfrak{H}^{n}$ and
$\mathfrak{H}^{-n}$, one can attain the relation

$\|f\|_{\mathfrak{H}^{-n}}\leq\|f\|\leq\|f\|_{\mathfrak{H}^{n}}.$

###### Theorem 7

Let $\mathfrak{B}$ be a Banach space inside the chain

$\mathfrak{H}^{k_{1}}\subseteq\mathfrak{B}\subseteq\mathfrak{H}^{-k_{2}}$
$None$

of continuously and densely embedded into each other spaces with some
$k_{1},k_{2}\in\mathbb{N}$, and let a sequence
$\\{m_{n}\\}_{n\in\mathbb{N}_{0}}$ possess the properties (10) and (12). Then
for a weak solution $y(t)$ of equation (1), the following equivalence
relations hold true:

$\begin{array}[]{rcl}y\in
C^{\infty}(\mathbb{R}_{+},\mathfrak{H})&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(y,\mathfrak{B})=O\left(r^{-\alpha}\right)\quad(r\to\infty),\\\
y\in
C_{\\{m_{n}\\}}&\Longleftrightarrow&\exists\alpha>0,:\mathcal{E}_{r}(y,\mathfrak{B})=O\left(\tau^{-1}(\alpha
r)\right)\quad(r\to\infty),\\\ y\in
C_{(m_{n})}&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{r}(y,\mathfrak{B})=O\left(\tau^{-1}(\alpha
r)\right)\quad(r\to\infty),\\\ \end{array}$

where

$\mathcal{E}_{r}(y,\mathfrak{B})=\inf_{y_{0}\in S_{0}:\sigma(y_{0})\leq
r}\sup_{s\in\mathbb{R}_{+}}\|y(s)-y_{0}(s)\|_{\mathfrak{B}},$

$\tau(\lambda)$ is defined by (11), $\|\cdot\|_{\mathfrak{B}}$ is the norm in
$\mathfrak{B}$.

###### Proof.

Show first that the spaces $C_{\\{m_{n}\\}}(A)$ and $C_{(m_{n})}(A)$
considered as subspaces of $\mathfrak{H}$ coincide with the corresponding
subspaces $C_{\\{m_{n}\\}}^{k}(A)$ and $C_{(m_{n})}^{k}(A)$ constructed in the
Hilbert space $\mathfrak{H}^{k}$ from the restriction
$A\upharpoonright\mathfrak{H}^{k}$ which is a nonnegative self-adjoint
operator in $\mathfrak{H}^{k}$.

So, let $f\in C_{\\{m_{n}\\}}(A)$. Then

$\exists\alpha>0,\ \exists
c>0:\left\|A^{i}f\right\|_{\mathfrak{H}^{k}}=\left(\left\|A^{i}f\right\|^{2}+\left\|A^{i+k}f\right\|^{2}\right)^{1/2}$
$\qquad\qquad\qquad\leq
c\left(\alpha^{2i}m_{i}^{2}+\alpha^{2(i+k)}m_{k+i}^{2}\right)^{1/2}\leq\widetilde{c}\left(\alpha
h^{k}\right)^{i}m_{i},$ $None$

i.e., $C_{\\{m_{n}\\}}(A)\subseteq C_{\\{m_{n}\\}}^{k}(A)$. From (19) we also
have the embedding $C_{(m_{n})}(A)\subseteq C_{(m_{n})}^{k}(A)$. The inverse
embeddings are consequences of the estimate
$\left\|A^{i}f\right\|_{\mathfrak{B}}\leq\left\|A^{i}f\right\|_{\mathfrak{H}^{k}}$.
Thus we have

$C_{\\{m_{n}\\}}(A)=C_{\\{m_{n}\\}}^{k}(A),\quad
C_{(m_{n})}(A)=C_{(m_{n})}^{k}(A).$ $None$

It is also evident that $C_{k}^{\infty}(A)=C^{\infty}(A)$.

Since for a vector $g\in C_{\\{1\\}}(A)\ (m_{n}\equiv 1)$ of type
$\sigma(g,A)\leq k$, the inequality

$\left\|A^{i}f\right\|_{\mathfrak{H}^{k}}=\left(\left\|A^{i}g\right\|^{2}+\left\|A^{i+k}g\right\|^{2}\right)^{1/2}\leq
c\left(\alpha^{2i}+\alpha^{2(i+k)}\right)^{1/2}\leq\widetilde{c}\alpha^{i},\quad\widetilde{c}=\left(1+\alpha^{2k}\right)^{1/2},$

is valid, the space $C_{\\{1\\}}(A)$ coincides with $C_{\\{1\\}}^{k}(A)$.
Moreover, the type of $g$ for the operator $A$ in the space $C_{\\{1\\}}(A)$
is the same as the one for $A\upharpoonright\mathfrak{H}^{k}$ in the space
$C_{\\{1\\}}^{k}(A)$.

Denote by $\widetilde{A}$ the closure of $A$ in the space $\mathfrak{H}^{-k}$.
It is easy to make sure that $\widetilde{A}$ is a nonnegative self-adjoint
operator in $\mathfrak{H}^{-k}$ and if the space $\mathfrak{H}$ is considered
as a subspace of $\mathfrak{H}^{-k}$, then we arrive at the previous
situation. For this reason,

$C_{\\{m_{n}\\}}(A)=C_{\\{m_{n}\\}}^{-k}(A),\quad
C_{(m_{n})}(A)=C_{(m_{n})}^{-k}(A),$ $None$

and

$\forall g\in
C_{\\{1\\}}(A)=C_{\\{1\\}}^{k}(A):\sigma(g,A)=\sigma(g,\widetilde{A}).$

Taking into account that the restriction (extension) of the semigroup
$\left\\{e^{-At}\right\\}_{t\in\mathbb{R}_{+}}$ to the space
$\mathfrak{H}^{k_{1}},\ k_{1}>0,$ (to $\mathfrak{H}^{-k_{2}},\ k_{2}>0)$ is an
analytic contractive $C_{0}$-semigroup in $\mathfrak{H}^{k_{1}}$ (in
$\mathfrak{H}^{-k_{2}}$), the embeddings
$C_{\\{m_{n}\\}}^{k}(A)\subseteq\mathfrak{B},\
C_{(m_{n})}(A)\subseteq\mathfrak{B}$ and the chain (19), we obtain for
$y(t)=e^{-At}f,\ f\in C_{\\{m_{n}\\}}(A)$ and $y_{0}(t)=e^{-At}g,\ g\in
C_{\\{1\\}}(A)$ that

$\left\|e^{-At}f-e^{-As}g\right\|_{\mathfrak{B}}\leq\left\|e^{-At}f-e^{-As}g\right\|_{\mathfrak{H}^{k_{1}}}\leq\|f-g\|_{\mathfrak{H}^{k_{1}}},$

whence

$\mathcal{E}_{r}(y,\mathfrak{B})=\inf_{y_{0}\in S_{0}:\sigma(y_{0})\leq
r}\sup{s\in\mathbb{R}_{+}}\left\|e^{-As}f-e^{-As}g\right\|_{\mathfrak{B}}\leq\|f-g\|_{\mathfrak{H}^{k_{1}}},$

that is,

$\mathcal{E}_{r}(y,\mathfrak{B})\leq\mathcal{E}_{r}(f,A\upharpoonright\mathfrak{H}^{k_{1}}).$
$None$

From (19) it follows that

$\forall
t\in\mathbb{R}_{+}:\left\|e^{-At}f-e^{-At}g\right\|_{\mathfrak{H}^{-k_{2}}}\leq\left\|e^{-At}f-e^{-At}g\right\|_{\mathfrak{B}}.$

This implies that

$\|f-g\|_{\mathfrak{H}^{-k_{2}}}=\sup_{t\in\mathbb{R}_{+}}\left\|e^{-At}f-e^{-At}g\right\|_{\mathfrak{H}^{-k_{2}}}\leq\sup_{t\in\mathbb{R}_{+}}\left\|e^{-At}f-e^{-At}g\right\|_{\mathfrak{B}}$

and, hence,

$\inf_{g\in C_{\\{1\\}}(A):\sigma(g)\leq
r}\|f-g\|_{\mathfrak{H}^{-k_{2}}}\leq\inf_{y_{0}\in S_{0}:\sigma(y_{0})\leq
r}\sup_{t\in\mathbb{R}_{+}}\|y(t)-y_{0}(t)\|_{\mathfrak{B}}.$

Thus,

$\mathcal{E}_{r}(f,\widetilde{A})\leq\mathcal{E}_{r}(y,\mathfrak{B}).$ $None$

Inequalities (23) and (24), with regard to (19), (21), (22) and Theorem 5,
complete the proof of Theorem 7. ∎

5. Let $A$ be a self-adjoint operator in $\mathfrak{H}$ whose spectrum is discrete. Assume that its eigenvalues $\lambda_{k}=\lambda_{k}(A),\ k\in\mathbb{N},$ satisfy the condition $\sum_{k=1}^{\infty}\lambda_{k}^{-p}<\infty$ with some $p>0$. Suppose also that $\lambda_{k}$ are enumerated in ascending order and each one is counted according to its multiplicity and denote by $\\{e_{n}\\}_{n\in\mathbb{N}}$ the orthonormal basis in $\mathfrak{H}$ consisting of eigenvectors of $A$. Then the spectral function $E(\lambda)$ of the operator $A$ has the form

$E(\lambda)f=\sum_{\lambda_{k}\leq\lambda}f_{k}e_{k},$

where $f_{k}=(f_{k},e_{k})$ are the Fourier coefficients of $f$, and

$\mathcal{E}_{r}(f,A)=\sum_{\lambda_{k}>r}f_{k}e_{k}.$

As it has been shown in [6], the following assertion holds true.

###### Proposition 1

The following equivalence relations are valid:

$\begin{array}[]{rcl}f\in C^{\infty}(A)&\Longleftrightarrow&\forall\alpha>0,\
\exists c=c(\alpha)>0:|f_{k}|\leq c\lambda_{k}^{-\alpha},\\\ f\in
C_{\\{1\\}}(A)&\Longleftrightarrow&\exists n_{0}\in\mathbb{N}:f_{k}=0\
\text{as}\ k\geq n_{0},\\\ f\in
C_{\\{m_{n}\\}}(A)&\Longleftrightarrow&\exists\alpha>0,\ \exists
c>0:|f_{k}|\leq c\tau^{-1}(\alpha\lambda_{k}),\\\ f\in
C_{(m_{n})}(A)&\Longleftrightarrow&\forall\alpha>0,\ \exists
c=c(\alpha)>0:|f_{k}|\leq c\tau^{-1}(\alpha\lambda_{k}).\\\ \end{array}$

(The function $\tau(\lambda)$ was defined in (11)).

Let now $y(t)$ be a weak solution of (1). Then

$y(t)=\sum_{k=1}^{\infty}e^{-\lambda_{k}t}f_{k}e_{k},\quad\sum_{k=1}^{\infty}|f_{k}|^{2}<\infty.$
$None$

The solution $y(t)$ is an entire vector-valued function of exponential type
$(y\in S_{0})$ if and only if

$\exists n_{0}\in\mathbb{N}:f_{k}=0\ \text{as}\ k\geq n_{0}.$

Proposition 1, Theorems 3, 5 and (13) imply the following.

###### Theorem 8

The following equivalence relations take place:

$\begin{array}[]{rcl}y\in
C^{n}(\mathbb{R}_{+},\mathfrak{H})&\Longleftrightarrow&\mathcal{E}_{\lambda_{k}}(y)=o\left(\lambda_{k+1}^{-n}\right)\quad(n\to\infty),\\\
y\in
C^{\infty}(\mathbb{R}_{+},\mathfrak{H})&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{\lambda_{k}}(y)=O\left(\lambda_{k+1}^{-\alpha}\right)\quad(n\to\infty),\\\
y\in
C_{\\{m_{n}\\}}&\Longleftrightarrow&\exists\alpha>0:\mathcal{E}_{\lambda_{k}}(y)=O\left(\tau^{-1}(\alpha\lambda_{k+1})\right)\quad(n\to\infty),\\\
y\in
C_{(m_{n})}&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{\lambda_{k}}(y)=O\left(\tau^{-1}(\alpha\lambda_{k+1})\right)\quad(n\to\infty).\\\
\end{array}$

6. Put $\mathfrak{H}=L_{2}(\Omega)$, where $\Omega$ is a bounded domain in $\mathbb{R}^{q}$ with piecewise smooth boundary $\partial\Omega$, and denote by $B^{\prime}$ the operator generated in $L_{2}(\Omega)$ by the differential expression

$(\mathcal{L}u)(x)=-\sum_{i=1}^{q}\sum_{k=1}^{q}\frac{\partial}{\partial
x_{i}}\left(a_{ik}(x)\frac{\partial u(x)}{\partial x_{k}}\right)+c(x)u(x),$
$None$

on

$\mathcal{D}(B^{\prime})=\left\\{u\in
C^{2}(\overline{\Omega})\bigl{|}u\upharpoonright_{\partial\Omega}=0\right\\}.$
$None$

It is assumed that $a_{ik}(x),c(x)\in C^{\infty}(\overline{\Omega}),\ c(x)\geq
0$. Suppose also the expression (26) to be of elliptic type in
$\overline{\Omega}$. In this case all the eigenvalues $\mu_{i}(x),\ i=1,\dots
q$, of the matrix $\|a_{ik}(x)\|_{i,k=1}^{q},\ x\in\overline{\Omega}$, have
the same sign; without loss of generality we may assume $\mu_{i}(x)>0,\
x\in\overline{\Omega}$.

It is not hard to make sure that $B^{\prime}$ is a positive definite Hermitian
operator with dense domain in $L_{2}(\Omega)$. So, $B^{\prime}$ admits a
closure to a positive definite selfadjoint operator $B$ on $L_{2}(\Omega)$. We
shall call $B$ the operator generated by (26), (27). The spectrum of $B$ is
discrete, and for its eigenvalues,
$\lambda_{1}(B)<\lambda_{2}(B)<\dots<\lambda_{n}(B)<\dots$, the estimate

$c_{1}n^{2/q}\leq\lambda_{n}(B)\leq c_{2}n^{2/q},\quad
0<c_{i}={\rm{const}},\quad i=1,2.$ $None$

is valid (see [8]). Denote by $e_{n}(x),\ n\in\mathbb{N}$, the orthonormal
basis in $L_{2}(\Omega)$, consisting of eigenfunctions of $B$.

In the case where $\Omega$ is a $q$-dimensional cube, $0<x_{k}<a,\
k=1,\dots,q,\ a>0$, and
$\mathcal{L}=-\sum_{i=1}^{q}\frac{\partial^{2}}{\partial x_{i}^{2}}$, the
following formulas for the eigenvalues $\lambda_{n_{1}\dots n_{q}},\
n_{k}\in\mathbb{N}$, and eigenfunctions $e_{n_{1}\dots n_{q}}(x)$ of the
operator $B$ hold:

$\lambda_{n_{1}\dots n_{q}}=\frac{\pi^{2}}{a^{2}}\sum_{k=1}^{q}n_{k}^{2};\quad
e_{n_{1}\dots
n_{q}}(x)=\left(\frac{2}{a}\right)^{q/2}\prod_{k=1}^{q}\sin\frac{\pi}{a}x_{k}.$

Let $y(t)=u(t,x)\in C(\mathbb{R}_{+},L_{2}(\Omega))$ be a weak solution of the
problem

$\left(\frac{\partial}{\partial
t}-\sum_{k=1}^{q}\sum_{i=1}^{q}\frac{\partial}{\partial
x_{k}}\left(a_{ki}(x)\frac{\partial}{\partial
x_{i}}\right)+c(x)\right)u(t,x)=0,$ $None$ $\forall t>0,\ \forall
x\in\partial\Omega:u(t,x)=0,$ $None$

where the conditions on $a_{ki}(x)$ and $c(x)$ are the same as before. Then
$u(t,x)$ admits a representation of form (25). Set

$L_{2}^{n}=\mathcal{D}(B^{n}),\quad\|f\|_{L_{2}^{n}}=\left(\|f\|^{2}+\left\|B^{n}f\right\|^{2}\right)^{1/2},$

where $B$ is an operator generated in the space $L_{2}(\Omega)$ by expression
(26) and boundary value condition (27). The space $L_{2}^{n}$ is continuously
and densely embedded into $L_{2}(\Omega)$. Denote by $L_{2}^{-n}$ the negative
space corresponding to the positive one $L_{2}^{n}\subset L_{2}(\Omega)$. In
the case where $\mathcal{L}=-\sum_{k=1}^{q}\frac{\partial^{2}}{\partial
x_{k}^{2}}$, $L_{2}^{n}$ is none other than the well-known Sobolev space
$\stackrel{{\scriptstyle\circ}}{{W}}_{2}^{2n}(\Omega)$.

Using estimate (28) for $\lambda_{k}(B)$ and Theorem 8, we obtain in a way
analogous to that used in the proof of Theorem 7 the following assertion.

###### Theorem 9

Let $\mathfrak{B}$ be a Banach space and let

$L_{2}^{n_{1}}\subseteq\mathfrak{B}\subseteq L_{2}^{-n_{2}},\quad
n_{1},n_{2}\in\mathbb{N},$

be a chain of continuously and densely embedded into each other spaces.
Suppose also the sequence $\left\\{m_{n}\right\\}_{n=1}^{\infty}$ to satisfy
(10) and (12). Then

$\begin{array}[]{rcl}y(t)=u(t,x)\in
C^{\infty}(\mathbb{R}_{+},L_{2}(\Omega))&\Longleftrightarrow&\alpha>0:\mathcal{E}_{\lambda_{k}}^{\mathfrak{B}}(y)=O\left(\frac{1}{(k+1)^{\alpha}}\right),\\\
y(t)\in
C_{\\{m_{n}\\}}&\Longleftrightarrow&\exists\alpha>0:\mathcal{E}_{\lambda_{k}}^{\mathfrak{B}}(y)=O\left(\tau^{-1}\left(\alpha(k+1)^{2/q}\right)\right),\\\
y(t)\in
C_{(m_{n}}&\Longleftrightarrow&\forall\alpha>0:\mathcal{E}_{\lambda_{k}}^{\mathfrak{B}}(y)=O\left(\tau^{-1}\left(\alpha(k+1)^{2/q}\right)\right),\\\
\end{array}$

where

$\mathcal{E}_{\lambda_{k}}^{\mathfrak{B}}(y)=\inf_{y_{0}\in
S_{0}:\sigma(y_{0})\leq\lambda_{k}}\sup_{s\in\mathbb{R}_{+}}\|y(s)-y_{0}(s)\|_{\mathfrak{B}}.$

It is relevant to remark that in the case where $a_{ki}(x)=\delta_{ki}$ and
$c(x)\equiv 0$, by virtue of the embedding theorems for Sobolev spaces, one
can take the space $C(\overline{\Omega})$ of continuous in $\overline{\Omega}$
functions or $L_{p}(\Omega),\ 1\leq p<\infty,$ as $\mathfrak{B}$ and consider
not only the Dirichlet but some other boundary value problems, in particular,
the Neumann problem.

## References

  * [1]
  * [2] J. M. Ball, _Continuity properties of nonlinear semigroups_ , J. Functional Analysis 17 (1974), no. 1, 91–103.
  * [3]
  * [4] Yu. M. Berezanskiĭ, _Selfadjoint Operators in Spaces of Functions of Infinitely Many Variables_ , Transl. Math. Monographs, vol. 63, American Mathematical Society, Providence, RI, 1986.
  * [5]
  * [6] M. L. Gorbachuk, _On analytic solutions of operator-differential equations_ , Ukrainian Math. J. 52 (2000), no. 5, 680–693.
  * [7]
  * [8] M. L. Gorbachuk and V. I. Gorbachuk, _Operator approach to approximation problems_ , St. Petersburg Math. J. 9 (1998), no. 6, 1097–1110.
  * [9]
  * [10] M. L. Gorbachuk, Ya. I. Grushka, and S. M. Torba, _Direct and inverse theorems in the theory of approximations by the Ritz method_ , Ukrainian Math. J. 57 (2005), no. 5, 751–764.
  * [11]
  * [12] V. I. Gorbachuk, _On summability of expansions in eigenfunctions of self-adjoint operators_ , Soviet Math. Dokl. 35 (1987), no. 1, 11–15.
  * [13]
  * [14] N. P. Kupcov, _Direct and inverse theorems of approximation theory and semigroups of operators_ , Uspehi Mat. Nauk 23 (1968), no. 4, 117–178. (Russian)
  * [15]
  * [16] S. G. Mikhlin, _Linear Partial Differential Equations_ , Vysshaya Shkola, Moscow, 1977. (Russian)
  * [17]


# Considerations on Approaches and Metrics in Automated Theorem
Generation/Finding in Geometry

Pedro Quaresma Partially supported by FCT – Foundation for Science and
Technology, I.P., within the scope of the project CISUC – UID/CEC/00326/2020
and by European Social Fund, through the Regional Operational Program Centro
2020. CISUC / Department of Mathematics,
University of Coimbra, Portugal<EMAIL_ADDRESS>Department of Pure and Applied
Sciences, University of Urbino, ItalyFormal Methods and Tools, University of
Twente, Enschede, the Netherlands Pierluigi Graziani Partially supported by
Italian Ministry of Education, University and Research through the PRIN 2017
project “The Manifest Image and the Scientific Image” prot.
2017ZNWW7F_004.Department of Pure and Applied Sciences, University of Urbino,
Italy<EMAIL_ADDRESS>Formal Methods and Tools, University of
Twente, Enschede, the Netherlands Stefano M. Nicoletti Funded by ERC
Consolidator Grant 864075 (_CAESAR_).Formal Methods and Tools, University of
Twente, Enschede, the Netherlands<EMAIL_ADDRESS>
###### Abstract

The pursue of what are properties that can be identified to permit an
automated reasoning program to generate and find new and interesting theorems
is an interesting research goal (pun intended). The automatic discovery of new
theorems is a goal in itself, and it has been addressed in specific areas,
with different methods. The separation of the “weeds”, uninteresting, trivial
facts, from the “wheat”, new and interesting facts, is much harder, but is
also being addressed by different authors using different approaches. In this
paper we will focus on geometry. We present and discuss different approaches
for the automatic discovery of geometric theorems (and properties), and
different metrics to find the interesting theorems among all those that were
generated. After this description we will introduce the first result of this
article: an undecidability result proving that having an algorithmic procedure
that decides for every possible Turing Machine that produces theorems, whether
it is able to produce also interesting theorems, is an undecidable problem.
Consequently, we will argue that judging whether a theorem prover is able to
produce interesting theorems remains a non deterministic task, at best a task
to be addressed by program based in an algorithm guided by heuristics
criteria. Therefore, as a human, to satisfy this task two things are
necessary: an expert survey that sheds light on what a theorem prover/finder
of interesting geometric theorems is, and—to enable this analysis—other
surveys that clarify metrics and approaches related to the interestingness of
geometric theorems. In the conclusion of this article we will introduce the
structure of two of these surveys —the second result of this article— and we
will discuss some future work.

##  1 Introduction

In _Automated Reasoning: 33 Basic Research Problems_ , Larry Wos, wrote about
the problems that computer programs that reason face. Problem 31 is still open
and object of active research [57, 58]:

> _Wos’ Problem 31_ —What properties can be identified to permit an automated
> reasoning program to find new and interesting theorems, as opposed to
> proving conjectured theorems?

Two problems in a single sentence: _new_ and _interesting_ theorems. The
automatic discovery of new theorems is a goal in itself, it has been addressed
in specific areas, with different methods. The separation of the “weeds”,
uninteresting, trivial facts, from the “wheat”, new and interesting facts, is
much harder, but is being addressed also, by different authors using different
approaches.

Paraphrasing, again, Wos, “since a reasoning program can be instructed to draw
some (possible large) set of conclusions” what should be the “criteria that
permit the program to select from those the ones (if any) that correspond to
interesting results.”

Different fields have come across the finding of new and interesting theorems’
questions.

Regarding the novelty side: there are different views of approaching new
mathematical results. One of those approaches is the systematic exploration of
a given broad area of mathematical knowledge, generating, by different means,
new theorems and expecting to find interesting ones among those generated
(that will be analysed in section 4) [15, 16, 20, 26, 31, 36, 37, 47]. Another
approach is given by the pursue of mathematical discovery in specific areas,
e.g. _Computing Locus Equations_ [2, 10], _Automated Discovery of Angle
Theorems_ [55], _Automated Discovery of Geometric Theorems Based on Vector
Equations_ [43], _Automated Generation of Geometric Theorems from Images of
Diagrams_ [14], _Automatic Discovery of Theorems in Elementary Geometry_ [49].
These approaches do not aim to address the problem of automated theorem
finding in itself but, for example, to find complementary hypotheses for a
given geometric statements to become true [49] i.e. automatic discovery for
specific areas.111We left aside the notion of discovery in education, given
that, in that area, the goal is the student’s discovery of “new” (for them)
theorems, giving the student the possibility of freely making conjectures and
having an interactive/automatic deduction support in the exploration of those
“new” theorems [11, 33, 38, 39].

Regarding the interestingness side we are aware that relevant literature can
be found in different areas. For example in automated theorem proving [20, 26,
31, 47] and in sociological studies on the concept of proving [21, 40, 41], in
cognitive and educational science studies on the concept of proving [3, 12,
22, 34, 46, 53] and in semiotics and epistemology of mathematics [4, 5, 6, 9,
13].

Despite the cited studies, the Wos’ problem is still on the table. On the
contrary, a new result of undecidability can be added to the problem, i.e.
having an algorithmic procedure that decides for every possible Turing Machine
that produces theorems, whether it is able to produce also interesting
theorems, is an undecidable problem. Consequently, we can argue that judging
whether a theorem prover is able to produce interesting theorems remains a non
deterministic task, at best a task to be addressed by program based in an
algorithm guided by heuristics criteria. Therefore, as a human, to satisfy
this task we need expert survey that sheds light on what a theorem
prover/finder of interesting geometric theorems is, and—to enable this
analysis—other surveys that clarify metrics and approaches related to the
interestingness of geometric theorems.

Structure of the paper. In section 2 the issue of Automated Theorem Generation
(ATG) is discussed. In section 3 we discuss the deductive approach in ATG. In
section 4 the issue of Automated Theorem Finding (ATF) is analysed. In section
5 we present an undecidability result concerning the problem of finding
interesting theorems and its conceptual consequences. In section 6 we will
introduce the structure of two surveys to empirically explore the
interestingness of theorems in geometry and its potential application in
theorem proving/finding (a third survey). Finally, we will discuss some future
work.

##  2 Automated Theorem Generation

Automated theorem generation, independently of being interesting, or not, can
be addressed in several ways [47].

#### The Inductive approach,

is a natural approach. Conclusions are drawn by going from the specific to the
general. Exploring a given domain, seeking for properties that emerge from a
set of particular cases and making a conjecture about the general case.

Dynamic Geometry Software (DGS) can be seen as software environments to
inductively explore new knowledge. Making a geometric construction,
constrained by a given set of geometric properties, and then moving the free
point around will show all the fix-points, conjecturing if those new fixed
relations between objects are true in all cases, or not. For example the
Pappus’ Theorem, in this case, a well-known theorem: are the intersection
points (see Figure 1) $G$, $H$ and $I$, collinear? By moving, in the DGS, the
free-points it seems that they are, it remains to prove it.

Figure 1: Pappus’ Theorem

The inductive approach has the advantage of being stimulated by observations
in the domain. but has the disadvantage that induction is unsound. A famous
example of such unsound inductive approach can be seen in the Euclid Parallel
lines Postulate, that nevertheless was very fruitful, giving raise to
different geometries.

#### The Generative approach,

i.e. the generation of conjectures, testing them for theorem-hood. The
simplest form of generation is syntactic, in which conjectures are created by
mechanical manipulation of symbols, e.g. [45]. The _MCS_ program generates
conjectures syntactically and filters them against models of the domain [60].
A stronger semantically based approach is taken by the _HR_ program, which
generates conjectures based on examples of concepts in the domain [19]. A
theory exploration system called _QuickSpec_ , works by interleaving term
generation with random testing to form candidate conjectures [35]. In [35] the
conjecture generation approaches are classified into three categories:
heuristic rule-based systems, term generation-and-testing and neural network-
based systems. The _RoughSpec_ system adds to _QuickSpec_ the notion of
_shapes_ of theorems, specifying the shapes of conjectures the user is
interested in, and thus limiting the search [23].

Like induction, generation is unsound. However, if the rules by which the
generation is performed are sufficiently conservative then this approach may
generate a higher fraction of theorems than the inductive approach.

#### The Manipulative Approach,

conjectures are generated from existing theorems. An existing theorem is
modified by operations such as generalisation, specialisation, combination,
etc. This approach is used in abstraction mapping, which converts a theorem to
a simpler theorem, and uses a solution to the simpler theorem to help find a
solution to the original theorem [44]. Manipulation of ATP theorems has also
been used to produce new theorems for testing the robustness of ATP systems’
performances [56].

An advantage of the manipulative approach is that, if the manipulations are
satisfiability preserving, then theorems, rather than conjectures, are
produced from existing theorems. However, the conjectures produced by the
manipulative approach are typically artificial in nature, and thus
uninteresting.

#### The Deductive Approach,

consequences are generated by application of sound inference rules to the
axioms and previously generated logical consequences. This can be done by an
appropriately configured saturation-based ATP system.

The advantage of this approach is that only logical consequences are ever
generated. The challenge of this approach is to avoid the many uninteresting
logical consequences that can be generated.

##  3 The Deductive Approach

Some systems addresses, explicitly, the generation of new geometric results
using different approaches. In the following some of these approaches are
described.

###  3.1 Strong Relevant Logic-based Forward Deduction Approach

In [28] the authors argue for the fundamental difference between the Automated
Theorem Proving (ATP) and the Automated Theorem Finding (ATF). ATP is the
process of finding a justification for an explicitly specified statement from
given premises which are already known facts or previously assumed hypotheses.
ATF is the process to find out or bring to light that which was previously
unknown. Where ATP is all about known (old) facts, ATF is about previously
unknown conclusions from given premises. Jingde Cheng [16] claims that
classical mathematical logic, its various classical conservative extensions,
and traditional (weak) relevant logics cannot satisfactorily underlie
epistemic processes in scientific discovery, presenting an approach based on
strong relevant logic. Hongbiao Gao et al. have followed this approach
applying it for several domains such as NBG set theory, Tarski’s Geometry and
Peano’s Arithmetic [27, 28, 30, 31]

###  3.2 Rule Based Systems

The rule-based automated deduction system are often used when the proof itself
is an object of interest (and not only the end result), given that the proofs
are developed from the hypothesis and sets of axioms, to the conclusion by
application of the inference rules, the proofs are “readable”.

Example of such approaches can be seen in systems like _QED-Tutrix_ [24, 25]
and _JGEx_ [59], both for geometry. In the tutorial system _QED-Tutrix_ , the
rule based automated theorem prover goal is to find the many possible branches
of the proof tree, in order to be able to help the student approaching the
proof of a geometric conjecture. In the _JGEx_ system we can have the proof in
a “readable” and “visual” renderings and also the set of all properties that
can be deduced from the construction.

One of the ATP built-in in _JGEx_ is an implementation of the geometry
deductive database method [17, 59]. Using a breadth-first forward chaining a
fix-point for the conjecture at hand is reached. For that geometric
construction and the rules of the method, the fix-point gives us all the
properties that can be deduced, some already known facts, but also new facts
(not necessary interesting ones).

The geometry deductive database method proceeds by using a simple algorithm
where, starting from the geometric construction $D_{0}$, the rules, $R$, are
applied over and over till a fix-point, $D_{k}$ is reached:

$\framebox{$D_{0}$}\quad\stackrel{{\scriptstyle
R}}{{\subset}}\quad\framebox{$D_{1}$}\quad\stackrel{{\scriptstyle
R}}{{\subset}}\quad\quad\cdots\quad\stackrel{{\scriptstyle
R}}{{\subset}}\quad\framebox{$D_{k}$}\quad(\mbox{fix-point})$ (1)

In figure 2 an example, using _JGEx_ , is shown. On the right, the geometric
construction, on the left, the fix-point, with all the facts that were found
for that construction.

Figure 2: Fix-point in _JGEx_

A new open source implementation of this method, _OGP-GDDM_
,222https://github.com/opengeometryprover/OpenGeometryProver is described in
[8]. It will be integrated in the _Open Geometry Prover Community Project_
(OGPCP) [7]. One of the medium-term goals of the _OGP-GDDM_ project, is to
develop a meta-prover, a program capable to receive different sets of rules
and synthesise a specific ATP for those rules.

###  3.3 Algebraic Approaches

A similar approach is taken in the well-known dynamic geometry system
_GeoGebra_.333https://www.geogebra.org/ The _GeoGebra Discovery_
version444https://github.com/kovzol/geogebra-discovery has the capability to
find, from a user defined geometric construction, properties about that
construction. _GeoGebra Discovery_ reports some facts that were systematically
checked from a list of possible features including identical points, parallel
or perpendicular lines, equal long segments, collinearity or concyclicity.
This is not a deductive method so the generation process must be externally
verified, _GeoGebra Discovery_ do that by recurring to a built-in algebraic
automated theorem prover based in the Gröbner bases method [36, 37].

##  4 Automated Theorem Finding

Apart from our research goal of finding the interesting geometric theorems
among all those that were automatically generated, the pursue of measures of
interestingness has applicability in the interactive and automated theorem
proving area. In that area a common use of interestingness is to improve the
efficiency of the programs, tailoring the search space, making the search
depth limited and guaranteeing that only comprehensible concepts are produced
[20].

A goal, pursued with different approaches by many researchers, is the creation
of strong AI methods capable of complex research-level proofs, mathematical
discovery, and automated formalisation of today’s vast body of mathematics
[48]. The _MATHsAiD_ (Mechanically Ascertaining Theorems from Hypotheses,
Axioms and Definitions) project aimed to build a tool for automated theorem-
discovery, from a set of user-supplied axioms and definitions. In the words of
its authors, _MATHsAiD 2.0_ can conjecture and prove interesting Theorems in
high-level theories, including Theorems of current mathematical significance,
without generating an unacceptable number of uninteresting theorems [42]. The
_TacticToe_ system, combines reinforcement-learning with Monte-Carlo proof
search on the level of _HOL4_ tactics [32]. The _ENIGMA-NG_ system uses
efficient neural and gradient-boosted inference guidance for the ATP _E_ ,
improving its efficiency [18]. This two systems, one for interactive provers
and the other to automatic provers, are examples of systems that uses
discovery and filtering for improving the efficiency of automated deduction
systems.

###  4.1 The Deductive Approach Algorithm

The different approaches found in the literature [19, 28, 47] share, in their
general lines, the same algorithm: for a given logical fragment, select a
initial set of facts and then a cycle of generation/filtering is applied until
some stopping condition is matched (see Fig. 3).

List of axioms/deduction rules for a given logic fragment New Fact List:
hypothesis + interesting theorems $\bullet$$\bullet$ New Fact Exist? Apply
Deduction Run-time Filter Interesting Theorems Filter List of Interesting
Theorems yesnoInteresting
Theorem(added)(discarded)no(discarded)tautologies/false conj.

Figure 3: New and Interesting Theorems Algorithm

###  4.2 Filtering Interesting Theorems

A first level of filtering (run-time filter) should discard the obvious
tautologies and also conjectures proved false by empirical evidence.

The filtering for interesting theorems or for uninteresting conjectures, two
sides of the same coin, is done by application of a series of filters. These
filters are still to be validated, being of speculative nature [20, 30, 31,
47].

Obviousness:

the number of inferences in its derivation. Obviousness estimates the
difficulty of proving a formula, it can be given by the number of inferences
in its derivation.

Weight:

the effort required to read a formula. The weight score of a formula is the
number of symbols it contains.

Complexity:

the effort required to understand a formula, the number of distinct function
and predicate symbols it contains.

Surprisingness:

measures new relationships between concepts and properties.

Intensity:

measures how much a formula summarises information from the leaf ancestors in
its derivation tree.

Adaptivity:

measures how tightly the universally quantified variables of a formula are
constrained (for formulae in clause normal form).

Focus:

measures the extent to which a formula is making a positive or negative
statement about the domain of application.

Usefulness:

measures how much an interesting theorem has contributed to proofs of further
interesting theorems.

In spite of the relevance of these metrics, it would be appropriate to
construct an expert survey with which we could validate them by referring to a
significant public of experts. We believe this kind of survey would be
relevant not only to face Wos’ problem, but also to better understand how to
construct and evaluate software that generates/finds interesting theorems.
Despite having only relevant metrics and approaches regarding Wos’ problem,
while not yet having formal results, we can prove a relevant result that
concerns the second issue, i.e., the question regarding Interesting Turing
Machines, i.e., programs capable of generating interesting new geometric
results.

##  5 Undecidability Result

In section 4.2 the application of filters was discussed, these filters are
based on some measures of interestingness that are still to be validated and
that are applied in an heuristic way. Is it possible to have a deterministic
approach, i.e., is it possible to write a computer program that in a
deterministic way, find interesting theorems? We show, as an application of
the Rice’s theorem [50, 51, 52] (see Lemma 1), that it is undecidable to
determine, for a given Turing Machine, whether the language recognised by it
has the (non-trivial) property of finding interesting theorems.

######  Definition 1 (Non-Trivial Property).

A property $p$ of a formal language is _non-trivial_ if:

  * •

there exist a recursively enumerable language having the property $p$;

  * •

there exist a recursively enumerable language not having the property $p$.

######  Lemma 1 (Rice’s Theorem).

Let $p$ be any non-trivial property of the language of a Turing machine. The
problem of determining whether a given Turing machine’s language has property
$p$ is undecidable.

######  Theorem 1 (Undecidability Result).

For any given Turing Machine, it is undecidable to determine, whether the
language recognised by it has the property of finding interesting theorems.

###### Proof.

All programs (Turing machines) capable of automated theorem proving and by
extension generating/finding geometric theorems rely on a formal language to
describe the geometric constructions, conjectures and proofs. For example we
can consider the (full) _First-Order Form_
(FOF)555http://tptp.cs.miami.edu/TPTP/QuickGuide/ of _TPTP_ [54] and the
formal axiomatic theories for geometry based on that language.666TPTP Axioms
Files for geometry, https://www.tptp.org/cgi-bin/SeeTPTP?Category=Axioms, e.g.
_Tarski geometry axiom_ , GEO001 and GEO002, _Deductive Databases Method in
Geometry_ , GEO012.

Let $p$ be the property of that language that says that theorem $t$ is
interesting, for any conceivable definition of interestingness, then there
exist a recursively enumerable language having the property $p$. It will be
enough to restrict the language in such a way that the theorem $t$, and only
this, would be recognised. But, it also exist a recursively enumerable
language not having the property $p$. It would be enough to restrict that
language in such a way that only tautologies would be recognised. Tautologies
are, for any conceivable definition of interestingness, uninteresting. We have
proved that $p$, the property that can establish if a given theorem is
interesting, is a non-trivial property.

Having establish that the property $p$ is non-trivial, then, by application of
Rice’s theorem, it is undecidable to determine for any given Turing machine
$M$, whether the language recognised by $M$ has the property $p$. ∎

In other words, it is undecidable to have a deterministic program that can
find interesting problems. At best this is a task to be addressed by programs
based on algorithms guided by heuristics criteria.

##  6 Designing Interesting Surveys

In light of our undecidability result, to understand what experts mean by, “a
program that is able to also prove interesting theorems”, must be done
referring to empirical data, via the formulation of an expert survey. However,
for it to be fulfilled, one has to first reach a minimal degree of agreement
on the definition of interestingness of theorems. How could one speak about
programs that produce such theorems? In order to achieve this agreement, an
empirical exploration of the notion of interestingness and of what it
concretely entails is paramount. This exploration requires to situate the
notion of interestingness historically and socio-culturally, considering
logical, epistemological, sociological, cognitive, semiotic and pedagogical
aspects of the issue. Probably—and as Wos already implies—interestingness
entails different tangible properties, which differ in given centuries,
geographical locations and societies. Moreover, in some cases we say that a
theorem is interesting for what we can call global reasons e.g., Euclid’s
theorem on the infinitude of the set of prime numbers, Zorn’s lemma and
Gödel’s Theorems are interesting due to their role in mathematics, logic and
computer science. Other times for local reasons e.g., in relation to what we
are teaching our students at that moment. In order to assess which tangible
properties—both global and local—interestingness entails today, we are
proposing to conduct two expert surveys with two statistically significant
pools of participants.

#### Influencing factors.

Gao et al. performed an extensive analysis of areas like Set Theory, Peano’s
arithmetic and Tarski’s Geometry, looking for the relevance of structural
factors, such as the degree of logical connectives in the theorem, the
propositional schema of the formula formalising the theorem, the abstract
level of predicates and functions in the theorem and the deduction distance of
a theorem [20, 29, 31, 47]. Some of these structural aspects might be related
to our cognitive dynamics. But also the epistemological role of a theorem with
respect to other theorems might be a relevant feature; or the educational role
that some theorems have with respect to some notions might influence their
interestingness. Finally, the history of a theorem—e.g. Fermat’s last
theorem—could add points to its interestingness, which, in the case of
Fermat’s last theorem, might be already caused by the technicalities of the
proof itself.

#### Designing the surveys.

Taking all these factors into consideration, we would propose to design three
surveys that question experts from different fields.

Before describing the surveys below some clarifications are necessary. We will
use the term “expert” to mean mathematics teachers at primary, middle, and
high schools, and professors or researchers in pure and applied mathematics at
universities or at research centres. Furthermore, we will focus on the case
study of geometry, hence interesting theorems in geometry. The reasons for
this restriction to geometry are as follows: on the one hand, considering all
fields of research in mathematics might require a too large number of experts
and could produce too many divergent ideas. On the other hand, having in mind
an application of the results in automatic theorem proving as a target, it
seems appropriate to move into an area were there are many different methods
and many automated provers implementing those methods. Finally, geometry is a
kind of language common to many areas of mathematics and has been a domain for
reflection since the early years of mathematics teaching.

Finally, these surveys are intended to involve mathematics teachers, but their
outcome does not target mathematics education. Of course, this is a possible
target, but it is not the primary goal of these starting surveys.

###  6.1 Three Surveys

In the first survey, we will ask the experts both to indicate some situations
in which they remember to have used the adjective interesting concerning a
theorem, and to explain the use of this expression. In addition, we will ask
experts to list several geometric theorems they find interesting, and to list
several geometric theorems they find not interesting, both from elementary and
higher geometry, explaining the reasons for their answers (see Appendix A).
This first survey is already under way, the steering committee is already
approaching it and the authors of accepted papers in the conference, _14th
International Conference on Automated Deduction in Geometry_ (ADG 2023)777 ADG
2023, 14th International Conference on Automated Deduction in Geometry,
Belgrade, Serbia, September 20-22, 2023., were invited to participate. We are
planning to enlarge it to our network of contacts and we invite the interested
reader to also participate, answering
it.888https://docs.google.com/forms/d/e/1FAIpQLScIXZbLPBHTLvmQ28P30Cm_-
lkOrM7e6rab7ho0WrAFwf_mbQ/viewform?usp=sf_link We are planning to begin
collect and analyse the answers in February, 2024.

We will use the information from this survey to define a list of
characteristics (A,B,C, …) of a theorem that offer sufficient reasons to
attribute interestingness to it. We will assign weights to the various
characteristics by considering the answers to this first survey.

After the first survey, we will implement a second one. This second survey
will consider a list of theorems that, in different percentages, have the
characteristics inferred from the first survey. We will submit the second
survey to a set of experts different from those used in the first survey. We
will ask these experts whether they find the theorems listed interesting or
not. We will ask them to rate, using a Likert scale,999A Likert scale is a
question which is a five-point or seven-point scale. The choices range from
Strongly Agree to Strongly Disagree so the survey maker can get a holistic
view of people’s opinions. It was developed in 1932 by the social psychologist
Rensis Likert. the degree of impact that having certain characteristics plays
in their attribution of interestingness (see Appendix B).

This second group will allow us to understand whether the characteristics
isolated through the first survey are sufficient conditions to affirm that a
theorem is interesting.

With an agreement on what an interesting theorem is, based on empirical
research, we could query experts in theorem generators/finders design, with
another survey (the third survey) asking how to design software able to
produce these interesting theorems.

After that, we will focus our empirical inquiry on programs, driven by
heuristics based on our findings, able to find interesting theorems.

We have established a _steering committee_ to design the surveys and who will
oversee the submission of the surveys to experts around the world.

The steering committee consists of the following scholars:

  * •

Thierry Dana-Picard, Jerusalem College of Technology, Jerusalem, Israel;

  * •

James Davenport, University of Bath, United Kingdom;

  * •

Pierluigi Graziani, University of Urbino, Urbino, Italy;

  * •

Pedro Quaresma, University of Coimbra, Coimbra, Portugal;

  * •

Tomás Recio, University Antonio de Nebrija, Madrid, Spain.

##  7 Conclusions

The pursuit of new and interesting theorems in geometry, by automatic means is
an interesting open problem. From the point of view of generating new
information the deductive approach seems the most appropriated, given that:
only logical consequences are ever generated and also the paths to those new
theorems can be analysed from the point of view of the geometric theory used,
i.e. in the process of generating new facts, geometric proofs of their
validity are produced. Already existing implementations, e.g. the deductive
databases method (DDM) implemented in _JGEx_ , and new implementations, e.g.
the _GeoGebra Discovery_ and the new implementation of the DDM, the _OGPCP-
GDDM_ prover, can be used. The separation of the uninteresting, trivial facts,
from the new and interesting facts is much harder. The current approaches are
based in ad-hoc measures, proposed by experts from the field, but
nevertheless, not substantiated by any study approaching that problem. Our
goal is to fulfil that gap, to produce a comprehensive survey, supported in a
large set of mathematicians, in order to be able to return to that question
and to develop filters supported by the findings of that survey.

#### Acknowledgements

The authors wish to thank Francisco Botana, Thierry Dana-Picard, James
Davenport and Tomás Recio for their support in the pursue of this long term
project.

## References

  * [1]
  * [2] Miguel Á. Abánades, Francisco Botana, Antonio Montes & Tomás Recio (2014): _An algebraic taxonomy for locus computation in dynamic geometry_.  Computer-Aided Design 56, pp. 22–33, 10.1016/j.cad.2014.06.008.
  * [3] Gilles Aldon, Pierre-Yves Cahuet, Viviane Durand-Guerrier, Mathias Front, Didier Krieger, Michel Mizony & Claire Tardy C (2010): _Expérimenter des problèmes innovants en mathématiques à l’école_.  INRP.  Available at https://hal.archives-ouvertes.fr/hal-00989132.
  * [4] Ferdinando Arzarello & Cristina Sabena (2010): _Semiotic and theoretic control in argumentation and proof activities_.  Educational Studies in Mathematics 77(2-3), pp. 189–206, 10.1007/s10649-010-9280-3.
  * [5] Michael Aschbacher (2005): _Highly complex proofs and implications of such proofs_.  Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 363(1835), pp. 2401–2406, 10.1098/rsta.2005.1655.
  * [6] Jeremy Avigad (2006): _Mathematical Method and Proof_.  Synthese 153(1), pp. 105–159, 10.1007/s11229-005-4064-5.  Available at http://www.jstor.org/stable/27653412.
  * [7] Nuno Baeta & Pedro Quaresma (2021): _Open Geometry Prover Community Project_.  Electronic Proceedings in Theoretical Computer Science 352, pp. 129–138, 10.4204/EPTCS.352.14.
  * [8] Nuno Baeta & Pedro Quaresma (2023): _Towards a Geometry Deductive Database Prover_.  Annals of Mathematics and Artificial Intelligence 91(6), pp. 851–863, 10.1007/s10472-023-09839-0.
  * [9] Henk Barendregt & Freek Wiedijk (2005): _The challenge of computer mathematics_.  Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 363(1835), pp. 2351–2375, 10.1098/rsta.2005.1650.
  * [10] Francisco Botana, Miguel A. Abánades & Jesús Escribano (2007): _Computing Locus Equations for Standard Dynamic Geometry Environments_.  In Yong Shi, G. Dick van Albada, Jack Dongarra & Peter M. A. Sloot, editors: International Conference on Computational Science, Lecture Notes in Computer Science 4488, Springer Berlin Heidelberg, pp. 227–234, 10.1007/978-3-540-72586-2_32.
  * [11] Francisco Botana & José L. Valcarce (2002): _A dynamic-symbolic interface for geometric theorem discovery_.  Computers and Education 38(1-3), pp. 21–35, 10.1016/S0360-1315(01)00089-6.
  * [12] Alan Bundy, Mateja Jamnik & Andrew Fugard (2005): _What is a proof?_ Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 363(1835), pp. 2377–2391, 10.1098/rsta.2005.1651.
  * [13] Tyler Burge (1998): _Computer proof, apriori knowledge, and other minds: The sixth philosophical perspectives lecture_.  Philosophical perspectives 12, pp. 1–37, 10.1093/acprof:oso/9780199672028.003.0013.
  * [14] Xiaoyu Chen, Dan Song & Dongming Wang (2014): _Automated generation of geometric theorems from images of diagrams_.  Annals of Mathematics and Artificial Intelligence 74(3-4), pp. 1–26, 10.1007/s10472-014-9433-7.
  * [15] Jingde Cheng (1995): _Entailment calculus as the logical basis of automated theorem finding in scientific discovery_.  In: Systematic Methods of Scientific Discovery: Papers from the 1995 Spring Symposium, AAAI Press, pp. 105–110.
  * [16] Jingde Cheng (2000): _A Strong Relevant Logic Model of Epistemic Processes in Scientific Discovery_.  In E. Kawaguchi, H. Kangassalo, H. Jaakkola & I.A. Hamid, editors: Information Modelling and Knowledge Bases XI, Frontiers in Artificial Intelligence and Applications 61, IOS Press, pp. 136–159, 10.1007/3-540-49292-5_42.
  * [17] Shang-Ching Chou, Xiao-Shan Gao & Jing-Zhong Zhang (2000): _A Deductive Database Approach to Automated Geometry Theorem Proving and Discovering_.  Journal of Automated Reasoning 25(3), pp. 219–246, 10.1023/A:1006171315513.
  * [18] Karel Chvalovský, Jan Jakubův, Martin Suda & Josef Urban (2019): _ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E_.  In: Lecture Notes in Computer Science, Springer International Publishing, pp. 197–215, 10.1007/978-3-030-29436-6_12.
  * [19] Simon Colton (2002): _The HR Program for Theorem Generation_.  In Andrei Voronkov, editor: Automated Deduction—CADE-18, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 285–289, 10.1007/3-540-45620-1_24.
  * [20] Simon Colton, Alan Bundy & Toby Walsh (2000): _On the notion of interestingness in automated mathematical discovery_.  International Journal of Human-Computer Studies 53(3), pp. 351–375, 10.1006/ijhc.2000.0394.
  * [21] Richard A De Millo, Richard J Lipton & Alan J Perlis (1979): _Social processes and proofs of theorems and programs_.  Communications of the ACM 22(5), pp. 271–280, 10.1145/359104.359106.
  * [22] Bruno D’Amore & MI Fandiño Pinilla (2016): _Una formula per la misurazione oggettiva della difficoltà di comprensione di un testo di matematica da parte degli studenti. Uso valutativo e uso didattico_.  La matematica e la sua didattica, 1 2, pp. 59–78.
  * [23] Sólrún Halla Einarsdóttir, Nicholas Smallbone & Moa Johansson (2020): _Template-based Theory Exploration: Discovering Properties of Functional Programs by Testing_.  In: IFL 2020: Proceedings of the 32nd Symposium on Implementation and Application of Functional Languages, ACM, 10.1145/3462172.3462192.
  * [24] Ludovic Font (2021): _Génération automatique de preuves pour un logiciel tuteur en géométrie_.  phdthesis, Polytechnique Montréal.  Available at https://publications.polymtl.ca/9090/.
  * [25] Ludovic Font, Philippe R. Richard & Michel Gagnon (2018): _Improving QED-Tutrix by Automating the Generation of Proofs_.  In Pedro Quaresma & Walther Neuper, editors: Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267, Open Publishing Association, pp. 38–58, 10.4204/EPTCS.267.3.
  * [26] Hongbiao Gao & Jingde Cheng (2015): _An epistemic programming approach for automated theorem finding_.  In: 2015 IEEE 14th International Conference on Cognitive Informatics & Cognitive Computing (ICCIxCC), IEEE, 10.1109/ICCI-CC.2015.7259365.
  * [27] Hongbiao Gao & Jingde Cheng (2017): _Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in Peano’s Arithmetic_.  In Ngoc Thanh Nguyen, Satoshi Tojo, Le Minh Nguyen & Bogdan Trawinski, editors: Intelligent Information and Database Systems, Lecture Notes in Computer Science 10192, Springer International Publishing, pp. 115–124, 10.1007/978-3-319-54430-4_12.
  * [28] Hongbiao Gao, Yuichi Goto & Jingde Cheng (2014): _A systematic methodology for automated theorem finding_.  Theoretical Computer Science 554, pp. 2–21, 10.1016/j.tcs.2014.06.028.
  * [29] Hongbiao Gao, Yuichi Goto & Jingde Cheng (2015): _A Set of Metrics for Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in NBG Set Theory_.  In: Intelligence Science and Big Data Engineering. Big Data and Machine Learning Techniques, Springer International Publishing, pp. 508–517, 10.1007/978-3-319-23862-3_50.
  * [30] Hongbiao Gao, Jianbin Li & Jingde Cheng (2018): _Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning: A Case Study in Tarski's Geometry_.  In: 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation (SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI), IEEE, 10.1109/SmartWorld.2018.00064.
  * [31] Hongbiao Gao, Jianbin Li & Jingde Cheng (2019): _Measuring Interestingness of Theorems in Automated Theorem Finding by Forward Reasoning Based on Strong Relevant Logic_.  In: 2019 IEEE International Conference on Energy Internet (ICEI), IEEE, pp. 356–361, 10.1109/ICEI.2019.00069.
  * [32] Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar & Michael Norrish (2021): _TacticToe: Learning to Prove with Tactics_.  Journal of Automated Reasoning 65(2), pp. 257–286, 10.1007/s10817-020-09580-x.
  * [33] Gila Hanna, David Reid & Michael de Villiers, editors (2019): _Proof Technology in Mathematics Research and Teaching_.  Springer, 10.1007/978-3-030-28483-1.
  * [34] Kirsti Hemmi, Erika Julin & Ray Pörn (2017): _Misconceptions and developmental proof_.  In: CERME 10.
  * [35] Moa Johansson & Nicholas Smallbone (2021): _Automated Conjecturing in QuickSpec_.  In: 1st Mathematical Reasoning in General Artificial Intelligence Workshop, ICLR 2021.
  * [36] Zoltán Kovács, Tomás Recio & M. Pilar Vélez (2021): _Automated reasoning tools in GeoGebra discovery_.  ACM Communications in Computer Algebra 55(2), pp. 39–43, 10.1145/3493492.3493495.
  * [37] Zoltán Kovács & Jonathan H. Yu (2022): _Automated Discovery of Geometrical Theorems in GeoGebra_.  In João Marcos, Walther Neuper & Pedro Quaresma, editors: Proceedings 10th International Workshop on Theorem Proving Components for Educational Software, Electronic Proceedings in Theoretical Computer Science 354, pp. 1–12, 10.4204/EPTCS.354.1.
  * [38] Fou-Lai Lin, Feng-Jui Hsieh, Gila Hanna & Michael de Villiers, editors (2009): _Proceedings of the ICMI Study 19 conference: Proof and Proving in Mathematics Education_. 1, The Department of Mathematics, National Taiwan Normal University.
  * [39] Fou-Lai Lin, Feng-Jui Hsieh, Gila Hanna & Michael de Villiers, editors (2009): _Proceedings of the ICMI Study 19 conference: Proof and Proving in Mathematics Education_. 2, The Department of Mathematics, National Taiwan Normal University.
  * [40] Donald MacKenzie (1995): _The automation of proof: A historical and sociological exploration_.  IEEE Annals of the History of Computing 17(3), pp. 7–29, 10.1109/85.397057.
  * [41] Donald MacKenzie (1999): _Slaying the Kraken: The sociohistory of a mathematical proof_.  Social studies of science 29(1), pp. 7–60, 10.1177/030631299029001002.
  * [42] R. L. McCasland, A. Bundy & P. F. Smith (2017): _MATHsAiD: Automated mathematical theory exploration_.  Applied Intelligence 47(3), pp. 585–606, 10.1007/s10489-017-0954-8.
  * [43] Xicheng Peng, Qihang Chen, Jingzhong Zhang & Mao Chen (2021): _Automated Discovery of Geometric Theorems Based on Vector Equations_.  Journal of Automated Reasoning 65(6), pp. 711–726, 10.1007/S10817-021-09591-2.
  * [44] D. A. Plaisted (1980): _Abstraction mappings in mechanical theorem proving_.  In: 5th Conference on Automated Deduction Les Arcs, France, July 8–11, 1980, Springer Berlin Heidelberg, pp. 264–280, 10.1007/3-540-10009-1_21.
  * [45] David A. Plaisted (1994): _The search efficiency of theorem proving strategies_.  In: Automated Deduction — CADE-12, Springer Berlin Heidelberg, pp. 57–71, 10.1007/3-540-58156-1_5.
  * [46] George Polya (2004): _How to solve it: A new aspect of mathematical method_.  246, Princeton university press.
  * [47] Yury Puzis, Yi Gao & G. Sutcliffe (2006): _Automated Generation of Interesting Theorems_.  In: FLAIRS Conference.
  * [48] Markus N. Rabe & Christian Szegedy (2021): _Towards the Automatic Mathematician_.  In André Platzer & Geoff Sutcliffe, editors: Automated Deduction – CADE 28, Springer International Publishing, pp. 25–37, 10.1007/978-3-030-79876-5_2.
  * [49] T. Recio & M. P. Vélez (1999): _Automatic Discovery of Theorems in Elementary Geometry_.  J. Autom. Reason. 23, pp. 63–82, 10.1023/A:1006135322108.  Available at http://dl.acm.org/citation.cfm?id=594128.594243.
  * [50] H. G. Rice (1953): _Classes of recursively enumerable sets and their decision problems_.  Transactions of the American Mathematical Society 74(2), pp. 358–366, 10.2307/1990888.
  * [51] Hartley Rogers Jr (1987): _Theory of recursive functions and effective computability_.  MIT press.
  * [52] Michael Sipser (1997): _Introduction to the Theory of Computation_.  PWS Publishing Company.
  * [53] Andreas J Stylianides & Guershon Harel (2018): _Advances in mathematics education research on proof and proving: An international perspective_.  Springer, 10.1007/978-3-319-70996-3.
  * [54] Geoff Sutcliffe (2017): _The TPTP Problem Library and Associated Infrastructure_.  Journal of Automated Reasoning 59(4), pp. 483–502, 10.1007/s10817-017-9407-7.
  * [55] Philip Todd (2021): _A Method for the Automated Discovery of Angle Theorems_.  In: Proceedings of ADG 2021, 352, Open Publishing Association, pp. 148–155, 10.4204/EPTCS.352.17.
  * [56] Andrei Voronkov (2000): _CASC-16-1/2_.  Preprint Series CSSPP-4, The University of Manchester.  Available at http://www.s.man.a.uk/preprints/index.html.
  * [57] Larry Wos (1988): _Automated Reasoning: 33 Basic Research Problems_.  Prentice-Hall.
  * [58] Larry Wos (1993): _The problem of automated theorem finding_.  Journal of Automated Reasoning 10(1), pp. 137–138, 10.1007/BF00881868.
  * [59] Zheng Ye, Shang-Ching Chou & Xiao-Shan Gao (2011): _An Introduction to Java Geometry Expert_.  In Thomas Sturm & Christoph Zengler, editors: Automated Deduction in Geometry, Lecture Notes in Computer Science 6301, Springer Berlin Heidelberg, pp. 189–195, 10.1007/978-3-642-21046-4_10.
  * [60] Jian Zhang (1999): _System Description: MCS: Model-Based Conjecture Searching_.  In: Automated Deduction — CADE-16, Springer Berlin Heidelberg, pp. 393–397, 10.1007/3-540-48660-7_37.

##  Appendix A First Survey—Interesting Theorems

With this survey the goal will be to find the characteristics that make a
theorem interesting, or not. A list of questions about geometric theorems
found to be interesting, or not interesting.

For an initial pool of expert on the area it is our intention to use the
network created for the submission of the COST proposal,
_iGEOMXXI_.101010OC-2020-1-24509, Building a Networked Environment for
Geometric Reasoning (iGEOMXXI), The submitted Action (not funded) focused on
the exploration of new paradigms and methodologies for supporting formal
reasoning in the field of Geometry. A network of 49 experts from 19 countries.
This survey will be available online, based on an online survey
tool.111111e.g. _LimeSurvey_ , https://www.limesurvey.org/

###  A.1 Interesting and Why?

A list of situations/explanations about interesting theorems.

Can you describe in detail a situation (during classes or lectures) in which
you have used the adjective interesting applied to a theorem in geometry?
$n$th Situation Can you explain in detail the reasons why you used the
adjective interesting in the first situation? $n$th Explanation

###  A.2 Five Interesting Theorems in Geometry

A list of 5 questions, each about an interesting theorem.

Can you list at least five theorems in geometry that you consider interesting?
Theorem $n$ Can you explain in detail the reason for your choice by listing at
least five adjectives that describe characteristics of the previous theorem
making it interesting?

###  A.3 Five Not Interesting Theorems in Geometry

A list of 5 questions, each about a not interesting theorem.

Can you list at least five theorems in geometry that you consider NOT
interesting? Theorem $n$ Can you explain in detail the reason for your choice
by listing at least five adjectives that describe characteristics of the
previous theorem making it NOT interesting?

##  Appendix B Second Survey—Characteristics of Interesting Theorems

This survey will only be designed after studying the results of the first
survey. The second survey will propose theorems (taken from the first survey)
and will provide characteristics (taken from the first survey) for each of
them. The survey will ask the participants to express their opinion on
characteristics that (presumably) make the theorems interesting or not
interesting.

This survey will be available online, based on an online survey
tool.99footnotemark: 9

Please express whether you consider the following theorems interesting or not,
and why? Is Theorem $n$ interesting?
$\square$ YES $\square$ NO
Why? Because it has the characteristic A.
$\square$ Strongly disagree $\square$ Disagree $\square$ Neutral $\square$
Agree $\square$ Strongly Agree Why? Because it has the characteristic B.
$\square$ Strongly disagree $\square$ Disagree $\square$ Neutral $\square$
Agree $\square$ Strongly Agree Why? Because it has the characteristic C.
$\square$ Strongly disagree $\square$ Disagree $\square$ Neutral $\square$
Agree $\square$ Strongly Agree Why? Because it has the characteristic D.
$\square$ Strongly disagree $\square$ Disagree $\square$ Neutral $\square$
Agree $\square$ Strongly Agree