# Geodesic orbit and weakly symmetric spray manifolds

Xiyun Xu  School of Mathematical Sciences, Capital Normal University, Beijing
100048, P.R. China<EMAIL_ADDRESS>and  Ming Xu  Corresponding author,
School of Mathematical Sciences, Capital Normal University, Beijing 100048,
P.R. China<EMAIL_ADDRESS>
###### Abstract.

In this paper, we introduce the geodesic orbit and weakly symmetric properties
in homogeneous spray geometry. When a homogeneous spray manifold is endowed
with a reductive decomposition, we can use the spray vector field to describe
these properties, and prove that a weakly symmetric spray manifold must be
geodesic orbit, which generalizes its analog in homogeneous Riemannian and
Finsler geometries.

Mathematics Subject Classification(2010): 22E46, 53C30
Keywords: homogeneous geodesic, homogeneous spray manifold, weakly symmetric
space, geodesic orbit space, spray structure, spray vector field

##  1\. Introduction

A connected Riemannian homogeneous manifold is called geodesic orbit (or g.o.
in short), if any geodesic is the orbit of a one-parameter subgroup of
isometries. This notion was introduced by O. Kowalski and L. Vanhecke in 1991
[16], as a generalization of naturally reductive homogeneity. Since then,
there have been many research works on this subject. See [1, 2, 5, 10, 11, 12]
and references therein. There are many important subclasses in g.o. Riemannian
manifolds, which include the weakly symmetric Riemannian manifolds. The notion
of weak symmetry was proposed by A. Selberg [20] and it has interesting
connections with spherical spaces, commutative spaces, Galfand pairs, etc. [3,
7, 23, 32, 35]. A connected homogeneous Riemannian manifold is weakly
symmetric if and only if any two points can be exchanged by an isometry, or
equivalently, for any geodesic $c(t)$ there exists an element $g\in G$ such
that $g\cdot c(t)=c(-t)$ for all $t\in\mathbb{R}$. It is a well known fact
that a weakly symmetric Riemannian manifold is g.o. (see [4, 6] for two
different proofs). Meanwhile, the g.o. and weakly symmetric properties were
generalized by S. Deng and his coworkers to Finsler geometry [9, 34] (see [26,
27, 31, 36] for some recent progresses). By similar arguments as in the
Riemannian case, one can prove that a weakly symmetric Riemannian manifold is
also g.o. [8].

Beyond Riemann-Finsler geometry, there is a more general spray geometry, where
the metrics are ignored and only the (properly parametrized) geodesics are
concerned [21]. Nowadays, this field has caught the attention of many
geometers [17, 18, 33], and it has been studied in the homogeneous context as
well [15, 28, 29, 30] Homogeneous spray geometry generalizes homogeneous
Finsler geometry. In fact, it generalizes homogeneous pseudo-Riemannian
geometry and homogeneous pseudo-Finsler geometry as well.

In this paper, we generalize the g.o. and weakly symmetric properties to
homogeneous spray geometry. To avoid iterations, we automatically assume the
homogeneous manifolds are connected and Lie groups have only countable
connected components.

######  Definition 1.1.

We call a homogeneous spray manifold $(G/H,\mathbf{G})$ g.o. if each geodesic
$c(t)$ with $t$ sufficiently close to $0$ is $G$-homogeneous, i.e., there
exists $X\in\mathfrak{g}=\mathrm{Lie}(G)$, $x\in G/H$ and $\epsilon>0$, such
that $c(t)=\exp tX\cdot x$ for $t\in(-\epsilon,\epsilon)$.

######  Definition 1.2.

We call a homogeneous spray manifold $(G/H,\mathbf{G})$ weakly symmetric if
for any geodesic $c(t)$ with $t$ sufficiently close to $0$, there exists $g\in
G$, such that $g\cdot c(t)=c(-t)$ for all $t$ where both $c(t)$ and $c(-t)$
are defined.

######  Remark 1.3.

A homogeneous spray manifold may not be complete (see Section 4.3 in [28] for
an explicit example), so it is not reasonable to assume that the geodesics
$c(t)$ in above definitions are defined for all $t\in\mathbb{R}$.

Next, we use the spray vector field $\eta$ [28, 29] to characterize these
properties. Now assume that $G/H$ admits a reductive decomposition
$\mathfrak{g}=\mathfrak{h}+\mathfrak{m}$. Then, $\eta$ is an
$\mathrm{Ad}(H)$-equivariant positively 2-homogeneous smooth map from
$\mathfrak{m}\backslash\\{0\\}$ to $\mathfrak{m}$. Conversely, any map
satisfying this description is the spray vector field for some homogeneous
spray structure on $G/H$ (see Theorem 5.5 in [29]). We usually view $\eta$ as
a smooth tangent vector field on $\mathfrak{m}\backslash\\{0\\}$.

######  Theorem 1.4.

Let $(G/H,\mathbf{G})$ be a homogeneous spray manifold with a reductive
decomposition $\mathfrak{g}=\mathfrak{h}+\mathfrak{m}$ and the spray vector
field $\eta$. Then $(G/H,\mathbf{G})$ is g.o. if and only if $\eta$ is tangent
to $\mathrm{Ad}(H)$-orbits in $\mathfrak{m}\backslash\\{0\\}$, i.e., at each
$y\in\mathfrak{m}\backslash\\{0\\}$, $\eta(y)\in
T_{y}(\mathrm{Ad}(H)y)=[\mathfrak{h},y]$.

Here the orbit $\mathrm{Ad}(H)y$ for $y\in\mathfrak{m}\backslash\\{0\\}$ is
viewed as a submanifold in $\mathfrak{m}\backslash\\{0\\}$ (see Theorem 2.9.7
in [22]). Theorem 1.4 helps us find g.o. spray manifolds. For example, any
homogeneous manifold $G/H$ with a reductive decomposition can be endowed with
a canonical g.o. spray structure $\mathbf{G}_{0}$ with vanishing spray vector
field (see page 30 in [29]). Theorem 1.4 also reveals the difference between
g.o. properties in Finsler geometry and spray geometry. For example, on
$S^{2n-1}=U(n)/U(n-1)$, any homogeneous Finsler metric is g.o. [26], but
non-g.o. homogeneous spray structures can be easily constructed.

######  Theorem 1.5.

Let $(G/H,\mathbf{G})$ be a homogeneous spray manifold with a reductive
decomposition $\mathfrak{g}=\mathfrak{h}+\mathfrak{m}$. Then
$(G/H,\mathbf{G})$ is weakly symmetric if and only if for each
$y\in\mathfrak{m}\backslash\\{0\\}$, there exists $g\in H$, such that
$\mathrm{Ad}(g)y=-y$. In particular, when $(G/H,\mathbf{G})$ is weakly
symmetric, its spray vector field $\eta$ is even, i.e., $\eta(y)=\eta(-y)$,
$\forall y\in\mathfrak{m}\backslash\\{0\\}$.

The first statement in Theorem 1.5 implies that the classification for weakly
symmetric spray manifolds is an algebraic problem [24]. Here is a simple
example. On any connected Lie group $G$, there is a canonical affine bi-
invariant spray structure $\mathbf{G}_{0}$ [28], which geodesics are orbits of
one-parameter subgroups in $G$. This $\mathbf{G}_{0}$ is a symmetric (so it is
also weakly symmetric) homogeneous spray structure when $G$ is viewed as the
homogeneous manifold $\widetilde{G}/\widetilde{H}$, where $\widetilde{G}$ is
generated by all left and right translations, and the inverse operation
$\tau(g)=g^{-1}$. However, $\mathbf{G}_{0}$ is g.o. but not weakly symmetric
when $G$ is viewed as the homogeneous manifold $G/\\{e\\}$.

Finally, we use Theorem 1.4 and Theorem 1.5 to prove

######  Theorem 1.6.

Any weakly symmetric spray manifold $(G/H,\mathbf{G})$ with a reductive
decomposition $\mathfrak{g=h+m}$ is g.o..

Theorem 1.6 generalizes its analogs in homogeneous Riemannian and Finsler
geometries. To prove this theorem, we applied a new approach, which is based
on the theoretical framework of homogeneous spray geometry [28, 29, 30]. There
is a remaining question:

######  Question 1.7.

If a weakly symmetric spray manifold does not admit a reductive decomposition,
must it still be g.o.?

This paper is scheduled as follows. In Section 2, we summarize some
preliminary knowledge in spray geometry and introduce the spray vector field
for a homogeneous spray manifold. In Section 3, we prove all the theorems.

##  2\. Preliminaries

###  2.1. Spray structure and geodesic

The spray structure on a smooth manifold $M$ is a smooth tangent vector field
$\mathbf{G}$ on $TM\backslash 0$, which can be locally presented as

$\mathbf{G}=y^{i}\partial_{x^{i}}-2\mathbf{G}^{i}\partial_{y^{i}}$

for any standard local coordinate $(x,y)=(x^{i},y^{i})$ (i.e., $x=(x^{i})\in
M$ and $y=y^{j}\partial_{x^{j}}\in T_{x}M$). Here the spray coefficients
$\mathbf{G}^{i}=\mathbf{G}^{i}(x,y)$ are required to be positively
2-homogeneous for its $y$-entry, i.e., $\mathbf{G}^{i}(x,\lambda
y)=\lambda^{2}\mathbf{G}^{i}(x,y),\forall\lambda>0$. We call $(M,\mathbf{G})$
a spray manifold.

A smooth curve $c(t)$ on $(M,\mathbf{G})$ with nowhere-vanishing $\dot{c}(t)$
is called a geodesic if its lifting $(c(t),\dot{c}(t))$ in $TM\setminus 0$ is
an integral curve of $\mathbf{G}$. Locally, a geodesic $c(t)=(c^{i}(t))$ can
be characterized by the following ODE,

$\ddot{c}(t)+2\mathbf{G}^{i}(c(t),\dot{c}(t))=0,\forall i.$

On a Finsler manifold $(M,F)$, the canonical spray structure $\mathbf{G}_{F}$
is determined by

$\mathbf{G}^{i}_{F}=\tfrac{1}{4}g^{il}([F^{2}]_{x^{k}y^{l}}y^{k}-[F^{2}]_{x^{l}}).$

The geodesic and many curvatures (including Riemann curvature, Ricci
curvature, S-curvature, etc.) of $(M,F)$ coincide with those of
$(M,\mathbf{G}_{F})$ respectively. See [21] for more details.

###  2.2. Homogeneous spray manifold

A connected spray manifold $(M,\mathbf{G})$ is called homogeneous if there
exists a connected Lie transformation group $G$ which acts transitively on $M$
and preserves the set of all geodesics. More precisely, it means that, for any
$g\in G$, its tangent map on $TM$ preserves $\mathbf{G}$ [29]. In this
situation, we may identify $M$ as a homogeneous manifold $G/H$.

We assume that $G/H$ has a reductive decomposition $\mathfrak{g=h+m}$, where
$\mathfrak{g}=\mathrm{Lie}(G)$ and $\mathfrak{h}=\mathrm{Lie}(H)$. The
reductiveness here means that the given decomposition is
$\mathrm{Ad}(H)$-invariant, or in the Lie algebraic level,
$[\mathfrak{h},\mathfrak{m}]\subset\mathfrak{m}$. Then the subspace
$\mathfrak{m}$ can be equivariantly identified with the tangent space
$T_{o}(G/H)$ at $o=eH$. Here the equivariance means that the
$\mathrm{Ad}(H)$-action on $\mathfrak{m}$ coincides with the isotropy action
on $T_{o}(G/H)$.

######  Remark 2.1.

A homogeneous Finsler manifold always has a reductive decomposition [8, 19],
but a homogeneous spray manifold may not.

###  2.3. Spray vector field

Let $(G/H,\mathbf{G})$ be a homogeneous spray manifold with a reductive
decomposition $\mathfrak{g}=\mathfrak{h}+\mathfrak{m}$. The spray vector field
$\eta:\mathfrak{m}\backslash\\{0\\}\rightarrow\mathfrak{m}$ for
$(G/H,\mathbf{G})$ is defined as follows [29]. Let $c(t)$ be a geodesic on
$(G/H,\mathbf{G})$ satisfying $c(0)=o$ and $\dot{c}(0)=y\in
T_{o}(G/H)\backslash\\{0\\}=\mathfrak{m}\backslash\\{0\\}$. By the following
lemma (Lemma 5.1 in [29]), we can uniquely lift $c(t)$ to a curve in $G$.

######  Lemma 2.2.

There exists a unique smooth curve $\overline{c}(t)$ on $G$ satisfying
$\overline{c}(0)=e$, $c(t)=\overline{c}(t)\cdot o$, and
$(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))=(\overline{c}(t)^{-1})_{*}(\dot{c}(t))\in\mathfrak{m}\setminus\\{0\\}$
when $t$ is sufficiently close to $0$.

######  Remark 2.3.

For simplicty, we will always assume the parameter $t$ in later discussions to
be sufficiently close to $0$ without repeating.

Denote by $y(t)=(L_{\overline{c}_{y}(t)^{-1}})_{*}(\dot{\overline{c}}_{y}(t))$
a smooth curve in $\mathfrak{m}\setminus\\{0\\}$, then we define the spray
vector field $\eta$ by $\eta(y)=-\frac{d}{dt}|_{t=0}y(t)$. Theorem 5.3 in [29]
is crucial for proving our theorems later. We reformulate it as follows.

######  Theorem 2.4.

Let $(G/H,\mathbf{G})$ be a connected homogeneous spray manifold with a
reductive decomposition $\mathfrak{g=h+m}$ and the spray vector field $\eta$.
Then there is a one-to-one correspondence between the following two sets:

  1. (1)

The set of all geodesics $c(t)$ with $c(0)=o$;

  2. (2)

The set of all integral curves $y(t)$ of $-\eta$ which is defined at $t=0$.

The correspondence is from $c(t)$ to
$y(t)=(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))$, where
$\overline{c}(t)$ is the lifting of $c(t)$ provided by Lemma 2.2.

We will also needs the following property of $\eta$ (see Lemma 5.2 and Theorem
5.5 in [29]).

######  Lemma 2.5.

Let $(G/H,\mathbf{G})$ be a connected homogeneous spray manifold with a
reductive decomposition $\mathfrak{g=h+m}$, then its spray vector field is
$\mathrm{Ad}(H)$-equivariant, i.e., $\forall g\in H$,
$y\in\mathfrak{m}\backslash\\{0\\}$,
$\eta(\mathrm{Ad}(g)y)=\mathrm{Ad}(g)\eta(y)$.

######  Remark 2.6.

Spray vector field was first introduced by L. Huang for a homogeneous Finsler
manifold with a reductive decomposition [14]. When we generalize this notion
to homogeneous spray geometry, reductive decomposition is not essential. All
above statements except the $\mathrm{Ad}(H)$-equivariance of $\eta$ are still
valid.

##  3\. Proofs of the main Results

###  3.1. Proof of Theorem 1.4

Let $(G/H,\mathbf{G})$ be a homogeneous spray manifold with a reductive
decomposition $\mathfrak{g=h+m}$ and the spray vector field $\eta$. First, we
assume the g.o. property and prove that $\eta$ is tangent to the
$\mathrm{Ad}(H)$-orbits in $\mathfrak{m}\backslash\\{0\\}$.

We choose a vector $y$ from $\mathfrak{m}\backslash\\{0\\}$ and denote by
$c(t)$ be the geodesic on $(G/H,\mathbf{G})$ which satisfies $c(0)=o$ and
$\dot{c}(0)=y\in\mathfrak{m}\backslash\\{0\\}$. Then the g.o. property
provides a vector $u\in\mathfrak{g}$, such that $c(t)=\exp tu\cdot o$. Notice
that $u-y\in\mathfrak{h}$. Lemma 2.2 provides a smooth curve $\overline{c}(t)$
in $G$ such that

$\displaystyle\overline{c}(0)=e,\quad c(t)=\exp tu\cdot o=\overline{c}(t)\cdot
o,$ (3.1)
$\displaystyle(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))\in\mathfrak{m}\backslash\\{0\\}.$
(3.2)

By (3.1), $h(t)=\exp(-tu)\overline{c}(t)$ is a smooth curve in $H$ satisfying
$h(0)=e$. Because

$\dot{\overline{c}}(t)=\tfrac{d}{dt}(\exp(tu)h(t))=(L_{\exp
tu})_{*}\dot{h}(t)+(R_{h(t)})_{*}(L_{\exp tu})_{*}u,$

we have

$\displaystyle(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))$
$\displaystyle=$ $\displaystyle(L_{h(t)^{-1}})_{*}[(L_{\exp(-tu)})_{*}(L_{\exp
tu})_{*}\dot{h}(t)+(R_{h(t)})_{*}u]$ (3.3) $\displaystyle=$
$\displaystyle(L_{h(t)^{-1}})_{*}\dot{h}(t)+\mathrm{Ad}({h(t)^{-1}})u$
$\displaystyle=$
$\displaystyle[(L_{h(t)^{-1}})_{*}\dot{h}(t)+\mathrm{Ad}({h(t)^{-1}})(u-y)]+[\mathrm{Ad}({h(t)^{-1}})y].$

By the reductiveness of the given decomposition, the two summands in right
side of (3.3) belong to $\mathfrak{h}$ and $\mathfrak{m}$ respectively. So
(3.2) implies
$y(t)=(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))=\mathrm{Ad}({h(t)^{-1}})y$.
So $y(t)$ is a smooth curve on $\mathrm{Ad}(H)y$, and then its tangent vector
$\tfrac{d}{dt}|_{t=0}y(t)=[y,\dot{h}(0)]=-\eta(y)$ is contained in
$T_{y}(\mathrm{Ad}(H)y)=[\mathfrak{h},y]$. One side of Theorem 1.4 is proved.

Next, we assume that $\eta$ is tangent to $\mathrm{Ad}(H)$-orbits in
$\mathfrak{m}\backslash\\{0\\}$ and prove the g.o. property. Choose any vector
$y$ from $\mathfrak{m}\backslash\\{0\\}$, then our assumption provides
$\eta(y)=[v,y]$ for some $v\in\mathfrak{h}$.

Claim A: $y(t)=\mathrm{Ad}(\exp(-tv))y$ is the integral curve of $-\eta$ which
satisfies $y(0)=y$.

It is obvious that $y(0)=y$. By Lemma 2.5,

$\eta(y(t))=\mathrm{Ad}(\exp(-tv))\eta(y)=\mathrm{Ad}(\exp(-tv))[v,y]=[u,\mathrm{Ad}(\exp(-tv))y].$
(3.4)

On the other hand,

$\dot{y}(t)=\tfrac{d}{dt}e^{-t\mathrm{ad}(v)}y=-\mathrm{ad}(v)e^{-t\mathrm{ad}(v)}y=-[v,\mathrm{Ad}(\exp(-tv))y].$
(3.5)

Comparing (3.4) and (3.5), we get $\dot{y}(t)=-\eta(y(t))$. Claim A is proved.

Let $c(t)$ be the geodesic on $(G/H,\mathbf{G})$ which satisfies $c(0)=o$ and
$\dot{c}(0)=y$. Then Theorem 2.4 tells us
$y(t)=(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))$. Denote by $g(t)$
the curve in $G$ determined by $\overline{c}(t)=g(t)\exp(tv)$. Obviously
$g(0)=0$. Similar calculation as in (3.3) or in the proof of Lemma 5.1 in [29]
shows

$\displaystyle(L_{\overline{c}(t)^{-1}})_{*}(\dot{\overline{c}}(t))$
$\displaystyle=$ $\displaystyle(L_{\exp(-tv)})_{*}\tfrac{d}{dt}\exp
tv+\mathrm{Ad}(\exp(-tv))((L_{g(t)^{-1}})_{*}\dot{g}(t))$ (3.6)
$\displaystyle=$ $\displaystyle
v+\mathrm{Ad}(\exp(-tv))((L_{g(t)^{-1}})_{*}\dot{g}(t))$ $\displaystyle=$
$\displaystyle[v+\mathrm{Ad}(\exp(-tv))(((L_{g(t)^{-1}})_{*}\dot{g}(t))_{\mathfrak{h}})]$
$\displaystyle+[\mathrm{Ad}(\exp(-tv))(((L_{g(t)^{-1}})_{*}\dot{g}(t))_{\mathfrak{m}})],$

in which the subscripts $\mathfrak{h}$ and $\mathfrak{m}$ mean the projection
according to the given reductive decomposition. The two summands in the right
side of (3.6) belongs to $\mathfrak{h}$ and $\mathfrak{m}$ respectively.
Combine Claim A and (3.6), we see

$v+\mathrm{Ad}(\exp(-tv))(((L_{g(t)^{-1}})_{*}\dot{g}(t))_{\mathfrak{h}})=0\
\mbox{and}\ ((L_{g(t)^{-1}})_{*}\dot{g}(t))_{\mathfrak{m}}=y,$

i.e., $(L_{g(t)^{-1}})_{*}\dot{g}(t)\equiv y-v$. So $g(t)=\exp t(y-v)$ and
$c(t)=\overline{c}(t)\cdot=g(t)\exp tv\cdot o=\exp t(y-v)\cdot o$. We get the
g.o. property for $(G/H,\mathbf{G})$ and end the proof of Theorem 1.4.

###  3.2. Proof of Theorem 1.5

Let $(G/H,\mathbf{G})$ be a weakly symmetric spray manifold with a reductive
decomposition $\mathfrak{g=h+m}$. We choose a vector $y$ from
$\mathfrak{m}\backslash\\{0\\}$, and denote by $c_{1}(t)$ the geodesic on
$(G/H,\mathbf{G})$ which satisfies $c(0)=o$ and $\dot{c}(0)=y$. By Definition
1.2, there exists $g\in H$, such that the geodesic $c_{2}(t)=g\cdot c(t)$
coincides with $c_{1}(-t)$. Obviously
$\dot{c}_{2}(0)=\mathrm{Ad}(g)y=-\dot{c}_{1}(0)=-y$. This argument can be
reversed, which proves the first statement in Theorem 1.5.

Let $\overline{c}_{1}(t)$ be the lifting of $c_{1}(t)$ provided by Lemma 2.2.

Claim B: $\overline{c}_{2}(t)=\overline{c}_{1}(-t)$ is the lifting of
$c_{2}(t)$ provided by Lemma 2.2.

It is obvious that $\overline{c}_{2}(0)=\overline{c}_{1}(0)=e$ and
$c_{2}(t)=c_{1}(-t)=\overline{c}_{1}(-t)\cdot o=\overline{c}_{2}(t)\cdot o$.
Meanwhile, we have
$\dot{\overline{c}}_{2}(t)=\tfrac{d}{dt}\overline{c}_{1}(-t)=-\dot{\overline{c}}_{1}(-t)$,
and then

$\displaystyle(L_{\overline{c}_{2}(t)^{-1}})_{*}(\dot{\overline{c}}_{2}(t))=(L_{\overline{c}_{1}(-t)^{-1}})_{*}(-\dot{\overline{c}}_{1}(-t))=-(L_{\overline{c}_{1}(-t)^{-1}})_{*}(\dot{\overline{c}}_{1}(-t))\in\mathfrak{m}\backslash\\{0\\}.$

So $\overline{c}_{2}(t)=\overline{c}_{1}(-t)$ is the lifting of
$c_{2}(t)=c_{1}(-t)$ provided by Lemma 2.2, which proves Claim B.

By the definition of $\eta$, we have

$\eta(y)=-\tfrac{d}{dt}|_{t=0}[(L_{\overline{c}_{1}(t)^{-1}})_{*}\dot{\overline{c}}_{1}(t)]\quad\mbox{and}\quad\eta(-y)=-\tfrac{d}{dt}|_{t=0}[(L_{\overline{c}_{1}(t)^{-1}})_{*}\dot{\overline{c}}_{1}(t)].$

Direct calculation shows

$\displaystyle\eta(-y)$ $\displaystyle=$
$\displaystyle-\tfrac{d}{dt}|_{t=0}[(L_{\bar{c}_{2}(t)^{-1}})_{*}(\dot{\bar{c}}_{2}(t))]=\tfrac{d}{dt}|_{t=0}[(L_{\bar{c}_{1}(-t)^{-1}})_{*}(\dot{\bar{c}}_{1}(-t)]$
$\displaystyle=$
$\displaystyle-\tfrac{d}{ds}|_{s=-t=0}[(L_{\bar{c}_{1}(s)^{-1}})_{*}\dot{\bar{c}}_{1}(s)]=\eta(y),$

which proves Theorem 1.5.

###  3.3. Proof of Theorem 1.6

Let $(G/H,\mathbf{G})$ be a weakly symmetric spray manifold with a reductive
decomposition $\mathfrak{g=h+m}$ and the spray vector field $\eta$. We choose
any vector $y$ from $\mathfrak{m}\backslash\\{0\\}$ and denote by $y_{1}(t)$
the integral curve of $-\eta$ which satisfies $y_{1}(0)=y$. By Theorem 1.4, to
prove Theorem 1.6, we only need to prove that, for each value $t_{1}$,
$y_{1}(t_{1})$ is contained in $\mathrm{Ad}(H)y$. It should be notified that,
we have used here the quasi regularity of the submanifold $\mathrm{Ad}(H)y$ in
$\mathfrak{m}\backslash\\{0\\}$ (see page 117 in [13]).

By the first statement in Theorem 1.5, there exists $g_{1},g_{2}\in H$
satisfying $\mathrm{Ad}(g_{1})y=-y$ and
$\mathrm{Ad}(g_{2})y_{1}(\tfrac{t_{1}}{2})=-y_{1}(\tfrac{t_{1}}{2})$. Denote
by $y_{2}(t)=\mathrm{Ad}(g_{2})y_{1}(t+\tfrac{t_{1}}{2})$ another curve in
$\mathfrak{m}\backslash\\{0\\}$. Calculation shows

$\displaystyle\dot{y}_{2}(t)$ $\displaystyle=$
$\displaystyle\tfrac{d}{dt}(\mathrm{Ad}(g_{2})y_{1}(t+\tfrac{t_{1}}{2}))=\mathrm{Ad}(g_{2})\dot{y}_{1}(t+\tfrac{t_{1}}{2})=\mathrm{Ad}(g_{2})(-\eta(y_{1}(t+\tfrac{t_{1}}{2})))$
$\displaystyle=$
$\displaystyle-\eta(\mathrm{Ad}(g_{2})y_{1}(t+\tfrac{t_{1}}{2}))=-\eta(y_{2}(t)),$

in which Lemma 2.5 has been used for the fourth equality. It indicates that
$y_{2}(t)$ is the integral curve of $-\eta$ which passes
$-y_{1}(\tfrac{t_{1}}{2})$ at $t=0$. On the other hand, we have

$\tfrac{d}{dt}(-y_{1}(-t+\tfrac{t_{1}}{2}))=\tfrac{d}{ds}|_{s=-t+\tfrac{t_{1}}{2}}y_{1}(s)=-\eta(y_{1}(-t+\tfrac{t_{1}}{2}))=-\eta(-y_{1}(t+\tfrac{t_{1}}{2})),$

where the second statement in Theorem 1.5 has been used for the last equality.
It tells us that $-y_{1}(t+\tfrac{t_{1}}{2})$ is also the integral curve of
$-\eta$ which passes $-y_{1}(\tfrac{t_{1}}{2})$ at $t=0$. So we must have

$\mathrm{Ad}(g_{2})y_{1}(t+\tfrac{t_{1}}{2})\equiv-
y_{1}(-t+\tfrac{t_{1}}{2}).$ (3.7)

Input $t=\tfrac{t_{1}}{2}$ into (3.7), then we get
$\mathrm{Ad}(g_{2})y_{1}(t_{1})=-y_{1}(0)=-y=\mathrm{Ad}(g_{1})y$, i.e.,
$y_{1}(t_{1})\in\mathrm{Ad}(H)y$. The proof of Theorem 1.6 is finished.

Acknowledgement This paper is supported by National Natural Science Foundation
of China (No. 11821101, No. 12131012), and Beijing Natural Science Foundation
(No. 1222003).

## References

  * [1] D.V. Alekseevsky and A. Arvanitoyeorgos, Riemannian flag manifolds with homogeneous geodesics, Trans. Amer. Math. Soc., 359 (2007), 3769C3789.
  * [2] D.V. Alekseevsky and Yu.G. Nikonorov, Compact Riemannian manifolds with homogeneous geodesics, SIGMA Symmetry Integrability Geom. Methods Appl., 5 (2009), 093, 16 pages.
  * [3] D.N. Akhiezer and E.B. Vinberg, Weakly symmetric spaces and spherical varieties, Transform. Groups, 4 (1999), 3C24.
  * [4] V.N. Berestovskii, Yu.G. Nikonorov, On homogeneous geodesics and weakly symmetric spaces, Ann. Global Anal. Geom. 55 (3) (2019), 575-589.
  * [5] V.N. Berestovskii and Yu.G. Nikonorov, Riemannian Manifolds and Homogeneous Geodesics, Springer Monogr. Math., Springer, Cham, 2020.
  * [6] J. Berndt, O. Kowalski and L. Vanhecke, Geodesics in weakly symmetric spaces, Ann. Global Anal. Geom. 15 (2) (1997), 153-156.
  * [7] J. Berndt, L. Vanhecke, Geometry of weakly symmetric spaces, J. Math. Soc. Japan 48 (4) (1996), 745-760.
  * [8] S. Deng, Homogeneous Finsler spaces, Springer, New York (2012).
  * [9] S. Deng and Z. Hou, Weakly symmetric Finsler spaces, Comm. Comtemp. Math. 12 (2010), 309-323.
  * [10] Z. Du$\breve{s}$ek, O. Kowalski and S. Nik$\breve{c}$evi’c, New examples of Riemannian g.o. manifolds in dimension 7, Differential Geom. Appl., 21 (2004),65C78.
  * [11] C. Gordon, Homogeneous Riemannian manifolds whose geodesics are orbits, 155C174. In: Progress in Nonlinear Differential Equations. V. 20. Topics in geometry: in memory of Joseph DAtri. Birkh$\ddot{a}$user, 1996.
  * [12] C. Gordon and Yu.G. Nikonorov, Geodesic Orbit Riemannian Structures on $\mathbb{R}^{n}$ , J. Geom. Phys. 134 (2018), 235-243.
  * [13] W. Greub, S. Halperin and R. Vanstone, Connections, Curvature and Cohomology, II, Academic Press, New York, London, 1973.
  * [14] L. Huang, On the fundamental equations of homogeneous Finsler spaces, Differential Geom. Appl. 40 (2015), 40:187-208.
  * [15] L. Huang and X. Mo, Inverse problem of left invariant sprays on Lie group, Internat. J. Math. 32 (10) (2021), no. 2150076, 13 pages.
  * [16] O. Kowalski and L. Vanhecke, Riemannian manifolds with homogeneous geodesics, Boll. Un. Mat. Ital. B (7), 5 (1) (1991), 189-246.
  * [17] Y. Li and X. Mo, On Sakaguchi-type result in projective spray geometry, Ann. Math. Pura Appl. (4) 200 (5) (2021), 2181-2189.
  * [18] B. Li and Z. Shen, Sprays of isotropic curvature, Internat. J. Math. 29 (1) (2018), no. 1850003, 12 pages.
  * [19] Yu.G. Nikonorov, On the structure of geodesic orbit Riemannian spaces, Ann. Glob. Anal. Geom. 52 (3) (2017), 289-311.
  * [20] A. Selberg, Harmonic analysis and discontinuous groups in weakly symmetric Riemannian spaces, with applications to Dirichlet series, J. Indian Math. Soc. 20 (1956), 47-87.
  * [21] Z. Shen, Differential Geometry of Spray and Finsler Spaces, Kluwer Academic Publishers, 2001.
  * [22] V.S. Varadarajan, Lie Groups, Lie Algebras, and Their Representations, G.T.M. 102, Springer-Verlag, New York, 1984.
  * [23] J.A. Wolf, Harmonic Analysis on Commutative Spaces, Math. Surveys Monog. 142, American Mathematical Society, Providence, 2007.
  * [24] J.A. Wolf and Z. Chen, Weakly symmetric pseudo-Riemannian nilmanifolds, J. Differential Geom. 121 (3) (2022), 541-572.
  * [25] M. Xu and S. Deng, Rigidity of negatively curved geodesic orbit Finsler spaces, C. R. Acad. Sci. Paris, Ser. I 355 (2017), 987-990.
  * [26] M. Xu, Geodesic orbit spheres and constant curvature in Finsler geometry, Differential Geom. Appl. 61 (2018), 197-206.
  * [27] M. Xu, Geodesic Finsler spaces with $K\geq 0$ and the (FP) condition, Adv. Geom. 21 (4) (2021), 551-564.
  * [28] M. Xu, Left invariant spray structure on a Lie group, J. Lie Theory 32 (1) (2022), 121-138.
  * [29] M. Xu, Submersion and homogeneous spray geometry, J. Geom. Anal. 32 (2022), no. 172.
  * [30] M. Xu, Parallel translations for a left invariant spray, Bull. Iran. Math. Soc. 49 (2023) (2), no. 16.
  * [31] M. Xu and S. Deng, Rigidity of negatively curved geodesic orbit Finsler spaces, C. R. Acad. Sci. Paris, Ser. I 355 (2017), 987-990.
  * [32] O.S. Yakimova, Weakly symmetric Riemannian manifolds with a reductive isometry group, Sb. Math. 195 (3-4) (2004), 599-614.
  * [33] G. Yang, Some classes of sprays in projective spray geometry, Differential Geom. Appl. 29 (4), 606-614.
  * [34] Z. Yan and S. Deng, Finsler spaces whose geodesics are orbits, Differential Geom. Appl., 36 (2014), 1-23.
  * [35] W. Ziller, Weakly symmetric spaces, in: Topics in Geometry, editted by S. Gindikin, Progress in Nonlinear Differential Equations and Their Application 20 (1996), 355-368.
  * [36] L. Zhang and M. Xu, Standard homogeneous $(\alpha_{1},\alpha_{2})$-metrics and geodesic orbit property, Math. N. 295 (7) (2022), 1443-1453.


Hybrid systems theorem proving provides strong correctness guarantees about the interacting discrete and continuous dynamics of cyber-physical systems.
The trustworthiness of proofs rests on the soundness of the proof calculus and its correct implementation in a theorem prover.
Correctness is easier to achieve with a soundness-critical core that is stripped to the bare minimum, but, as a consequence, proof convenience has to be regained outside the soundness-critical core with proof management techniques.
We present modeling and proof management techniques that are built on top of the soundness-critical core of to enable expanding definitions, parametric proofs, lemmas, and other useful proof techniques in hybrid systems proofs.
Our techniques steer the uniform substitution implementation of the differential dynamic logic proof calculus in to allow users choose when and how in a proof abstract formulas, terms, or programs become expanded to their concrete definitions, and when and how lemmas and sub-proofs are combined to a full proof.
The same techniques are exploited in implicit sub-proofs (without making such sub-proofs explicit to the user) to provide proof features, such as temporarily hiding formulas, which are notoriously difficult to get right when implemented in the prover core, but become trustworthy as proof management techniques outside the core.
We illustrate our approach with several useful proof techniques and discuss their presentation on the user interface.

§ INTRODUCTION

Hybrid systems theorem proving provides strong correctness guarantees about the interacting discrete and continuous dynamics of cyber-physical systems.
Theorem proving is most valuable early in the design of a system, since it is not merely a technique to prove the correctness of an already correct system, but also shines when analyzing a system in all its subtleties to discover unknown or only partially known properties of the system.
The trustworthiness of proofs and analysis results, however, rests on the soundness of the proof calculus and its correct implementation in a theorem prover.
Typical theorem prover implementations often opt for directly representing the rules of a proof calculus in the theorem prover, for instance, with axiom schemata in <cit.>, or with trusted implementations of rules (e.g., KeYmaeraD <cit.>) or decision procedures (e.g., invariant computation <cit.> in the HHL prover <cit.>).
The downside of such an approach is not only that implementations of rules and their side conditions become soundness-critical, but also that additional features often result in increasing the size of the soundness-critical code base of the theorem prover.
Correctness is easier to achieve with an LCF-style approach that strips the soundness-critical core to the bare minimum, but, as a consequence, proof convenience has to be regained outside the soundness-critical core with proof management techniques.
The  <cit.> theorem prover for hybrid systems takes an LCF-style approach; previous techniques expanded the capabilities of primarily by providing tactics <cit.>, e.g., for certifying solutions of differential equations <cit.>, for certifying safety and liveness properties of differential equations <cit.>, for stability proofs <cit.>, for code synthesis <cit.>, for component-based modeling and verification <cit.>, and for monitor synthesis <cit.>.

In this paper, we present modeling and proof management techniques that are built on top of the soundness-critical core of to enable structuring and modularizing models with definitions and modularizing proofs with lemmas.
These modeling and proof management techniques were developed primarily with interactive proofs in mind, but may also be beneficial for automation (e.g., hierarchical definitions may serve as proof hints).
Useful proof techniques for explicit proof management include expanding definitions of the model during a proof, parametric proofs to make progress in proofs despite unknown system properties (e.g., loop invariants), and creating and applying lemmas.
Our techniques steer the uniform substitution implementation of the differential dynamic logic proof calculus in to allow users choose when in a proof and how abstract formulas, terms, or programs become expanded to their concrete definitions, and when and how lemmas and sub-proofs are combined to a full proof.
The same techniques are exploited in implicit sub-proofs (without making such sub-proofs explicit to the user) to hide technicalities of the prover implementation whose details are irrelevant to the user, or to provide proof features, such as temporarily hiding formulas, which are notoriously difficult to get right when implemented in the prover core, but become trustworthy as proof management techniques outside the core.
On the user interface, we attempt to make such proof features available as part of the usual user interactions: for example, when a tactic asks for input (e.g., a loop invariant), users start a parametric proof simply by using uninterpreted function and predicate symbols as tactic inputs, which then appear like elements of the input model whose concrete interpretations can be defined and expanded at a later point in the proof.
That way, users can focus on exploring and understanding a system by way of formal proof to provide insight to the theorem prover when it becomes available during the proof.

The remainder of this paper is structured as follows:
sec:preliminaries introduces differential dynamic logic and the relevant core and user interface features of .
sec:proofmanagementexample gives an example proof that combines and illustrates several of the desired proof management techniques, sec:lemmas and sec:prooftechniques discuss the underlying lemma application and proof techniques and their appearance on the user interface, and sec:conclusion concludes the paper with a discussion of related and future work.

§ PRELIMINARIES

Differential Dynamic Logic by Example

Differential dynamic logic  <cit.> is a specification language and verification calculus for hybrid systems written as hybrid programs.
The syntax of hybrid programs (HP) is described by the following grammar where $\asprg,\bsprg$ are hybrid programs, $x$ is a variable and $\astrm,\genDE{x}$ are terms, $\ivr$ is a logical formula:

\begin{equation*}
\asprg,\bsprg ~\bebecomes~
\pupdate{\pumod{x}{\astrm}}
\alternative
\ptest{\ivr}
\alternative
\pevolvein{\D{x}=\genDE{x}}{\ivr}
\alternative
\pchoice{\asprg}{\bsprg}
\alternative
\asprg;\bsprg
\alternative
\prepeat{\asprg}
\end{equation*}

Assignments \(\pupdate{\pumod{x}{\astrm}}\) and tests \(\ptest{\ivr}\) (to abort execution and discard the run if $\ivr$ is not true) are as usual.
Differential equations \(\pevolvein{\D{x}=\genDE{x}}{\ivr}\) are followed along a solution of \(\D{x}=\genDE{x}\) for any duration as long as the evolution domain constraint $\ivr$ is true at every moment along the solution.
Nondeterministic choice \(\pchoice{\asprg}{\bsprg}\) runs either $\asprg$ or $\bsprg$, sequential composition \(\asprg;\bsprg\) first runs $\asprg$ and then $\bsprg$ on the resulting states of $\asprg$, and nondeterministic repetition \(\prepeat{\asprg}\) runs $\asprg$ any natural number of times.
For example, the hybrid program below

\[
\prepeat{\bigl(\underbrace{\text{if}~(x<1) \{\humod{y}{-x}\}~\text{else}~\{\humod{y}{*};\ptest{y>2}\}}_\textit{ctrl};~\underbrace{\pevolve{\D{x}=-xy}}_\textit{ode}\bigr)}
\]

repeats program $\textit{ctrl}$ followed by differential equation $\textit{ode}$ arbitrarily often; program $\textit{ctrl}$ is a choice between setting $y$ to the value of $-x$ when $x<1$ or else picking any $y>2$.
The combined effect of $\textit{ctrl}$ and $\textit{ode}$ is an exponential increase/decay of $x$ with a rate depending on the choice of $y$.
When programs become more complicated, it is useful to literally modularize hybrid programs into $\textit{ctrl}$, $\textit{ode}$ etc. using program symbols and use definitions as a structuring mechanism for models.

The formulas of describe properties of hybrid programs, summarized by the following grammar
where $\asfml,\bsfml$ are formulas, $\astrm,\bstrm$ are terms, $x$ is a variable and $\asprg$ is a hybrid program:

\begin{equation*}
\asfml,\bsfml ~\bebecomes~
\astrm\geq\bstrm \alternative
\lnot \asfml \alternative
\asfml \land \bsfml \alternative
\asfml \lor \bsfml \alternative
\asfml \limply \bsfml \alternative
\asfml \lbisubjunct \bsfml \alternative
\lforall{x}{\asfml} \alternative
\lexists{x}{\asfml} \alternative
\dbox{\asprg}{\asfml}
\alternative \ddiamond{\asprg}{\asfml}
\end{equation*}

The operators of first-order real arithmetic are as usual with quantifiers ranging over the reals.
Formula \(\dbox{\asprg}{\asfml}\) is true in a state iff formula $\asfml$ is true after all ways of running hybrid program $\asprg$, which is useful for expressing safety properties.
Dually, liveness properties are expressed with \(\ddiamond{\asprg}{\asfml}\), which is true in a state iff $\asfml$ is true after at least one run of $\asprg$.

Proofs in the Core

Γ_1Δ_1 (subgoal_1)
!…!Γ_nΔ_n (subgoal_n)

ΓΔ (conclusion)

A  representing proof state in the core

[anchor=east] at ($(ui.north west)+(0,-0.6)$) Tactics menu A;
[anchor=east] at ($(ui.west)+(0,0.3)$) Deduction B;
[anchor=east] at ($(ui.south west)+(0,0.8)$) Explanation C;
[anchor=west] at ($(ui.north west)+(0.2,-1.6)$) D;

User interface displays the open subgoals of a proof.
Tactics menu $\tiny\circled{\bf A}$ lists proof tactics and automation, deduction view $\tiny\circled{\bf B}$ lists the open subgoals (one tab per subgoal), explanation $\tiny\circled{\bf C}$ illustrates the last applied proof step and lists the recorded proof history as a tactic.
Subgoal 1 is selected $\tiny\circled{D}$ and its sequent $\lsequent{p,q \land r}{p}$ is displayed.

Proof state data structure and rendering on the user interface

The prover core represents proof state as derived rules called , which list the conclusion to prove and the open subgoals, as illustrated in fig:proofstate-provable.
Conclusion and subgoals are each represented with a sequent of the form $\lsequent{\Gamma}{\Delta}$: assumptions are in $\Gamma$, $\Delta$ lists the alternatives to prove.
The meaning of sequent $\lsequent{\Gamma}{\Delta}$ is that of formula $\bigwedge_{p \in \Gamma}p \limply \bigvee_{q\in\Delta}q$.
Validity of the subgoals justifies validity of the conclusion; a proof is closed when there are no more open subgoals.
The user interface of in fig:proofstate-ui displays proof state in its deduction view $\tiny\circled{\bf B}$, provides automation and tactics $\tiny\circled{\bf A}$ to progress in the proof, and lists proof step explanations $\tiny\circled{\bf C}$ as well as a tactic summarizing the recorded proof history.
Proofs can be started from an initial conjecture, as well as from a (partial) tactic that advances the proof state according to the tactic steps and displays the remaining proof goals (further manual steps are then recorded and extend the provided tactic).
The deduction view strives for close mnemonic similarity to text books <cit.> while maximizing screen estate use (it displays open subgoals in tabs to utilize the full screen width for each subgoal).
In principle, the user interface could use typesetting libraries such as MathJax, to resemble textbook appearance even more closely, but such attempts were abandoned for rendering performance reasons.

The core is stateless, it does not keep track of proof state.
Instead, tactics and proof management outside the core keep track of  and instruct the core to apply operations on  to transform proof state, see <cit.> for a description of how tactics combine axioms and a comparison to alternative implementation approaches.
Major core operations are to

* create a , which is allowed only from a small number of sources, the most important ones are \(\begin{aligned}\linfer
\linfer[qear]
\linfer
(from left to right: starting a proof by justifying the conjecture from itself, real arithmetic facts, and axioms);

* apply another , whose conjecture matches a subgoal syntactically to replace the existing subgoal with the subgoals of the other , which we exploit for applying lemmas;

* apply uniform substitution to replace predicate symbols with formulas, function symbols with terms, and program symbols with hybrid programs, which is useful to support definitions.

A simple proof instructing the core to create a new , apply rule $\irref{implyr}$ in step $\tiny\bcircled{1}$, and apply $\irref{qear}$ in step $\tiny\bcircled{2}$, which obtains a  from a trusted solver and applies it to the remaining subgoal to close the proof.

[draw,dashed] (implyr)

[below=-0.7cm of ui,draw,dashed] (qe)

[anchor=east] at ($(ui.west)+(0,0)$) Step implyr 1;
[draw,circle,very thick] (qehint) at ($(implyr.north east)+(-1.8,-2)$) ;
[-latex] (qehint) – node[right,pos=0.75,fill=white,xshift=0.5cm] apply hint $\irref{qear}~\bcircled{2}$ (qe);
[anchor=east] at ($(qe.west)+(0,-0.3)$) ASCII  A;
[anchor=east] at ($(qe.west)+(0,-1.6)$) Tactic B;

Presentation of step $\irref{implyr}~\tiny\bcircled{1}$ on the user interface as a sequent proof.
The final  is printed directly from the core in ASCII syntax, the tactic below lists the steps to reproduce the proof from the conjecture.

Steps in a proof in the core vs. presentation on the user interface

A typical proof, illustrated in fig:coreproof-internal, retrieves an initial  from the core and then proceeds by handing back the  to the core together with a proof rule to retrieve a follow-up .
This process is repeated until all subgoals are either reduced to axioms or valid formulas in real arithmetic, so no more subgoals remain.
At any point in this process can proof state be stored and used later as a lemma (even in other proofs).
This entire process is hidden from the user, who instead is presented the sequent proof in fig:coreproof-ui.

proofs appeal to uniform substitution from axioms <cit.>: for example, the test axiom $\dibox{\ptest{q}}p \lbisubjunct (q \limply p)$, which is an ordinary formula, together with uniform substitution $\sigma=\usubstlist{\usubstmod{q}{x>0},\usubstmod{p}{\dbox{\pevolve{\D{x}=-x}}x\geq 0}}$ can be used to obtain a concrete instance of this axiom during a proof as follows:

\[
\linfer[US]
{\dbox{\ptest{q}}p \lbisubjunct (q \limply p)}
{\dbox{\ptest{x>0}}\dbox{\pevolve{\D{x}=-x}}x\geq 0 \lbisubjunct (x>0 \limply \dbox{\pevolve{\D{x}=-x}}x\geq 0)} \enspace .
\]

Uniform substitution is mainly used as a mechanism to instantiate axioms soundly, but through <cit.> it is also useful to replace symbols in entire  soundly, as illustrated in fig:provablesubst.

[text width=4cm,draw,dashed] (conjecture)

p abq

[right=1.3cm of conjecture,text width=10cm,draw,dashed] (substituted)

x>0 x=-x(xx/2)x>0

[-latex,solid,black] (conjecture) – node[above] US 1 (substituted);

Uniform substitution $\sigma=\usubstlist{\usubstmod{p}{x>0},\usubstmod{a}{\pevolve{\D{x}=-x}},\usubstmod{b}{\prepeat{(\humod{x}{\frac{x}{2}})}},\usubstmod{q}{x>0}}$ on an entire  has uniform effect across subgoals and conclusion <cit.>.

In this paper, we are going to exploit its application to entire  in order to implement proof features such as expanding definitions during a proof and an extended lemma mechanism that is able to bridge syntactic differences between the lemma conclusion and its application target.

§ IMPLICIT AND EXPLICIT PROOF MANAGEMENT BY EXAMPLE

Bool A(Real x) <-> x=2;
Bool S(Real x) <-> x>=0;
HP ctrl ::=  if (S(x)) x:=2*x; ; /* ?S(x);x:=2*x; ++ ?!S(x);?true; */
HP ode  ::=  x'=-x ;

ProgramVariables Real x; End.

Problem  A(x) -> [ctrl;ode;*]S(x) End.

Definitions in the input syntax

Definitions menu

Predicate and program definitions in

The main motivation for proof management is to allow users expand definitions and structure proofs at their discretion, as well as to enable future automated definition expansion and contraction <cit.>.
For example, consider the input file in fig:defs-inputfile that uses predicate definitions $A(x) \equiv x=2$ to capture assumptions about initial values of $x$ and $S(x) \equiv x \geq 0$ to describe the desired safety property, as well as program definitions $\textit{ctrl}$, which doubles the value of any non-negative $x$, and the differential equation $\textit{ode}$, which models exponential decay.
The definitions populate the “Defs” menu in that allows users to expand definitions collectively () or selectively (e.g., ) during a proof, see fig:defs-menu.
The menu automatically adjusts to the symbols of the currently selected subgoal (in the background in fig:defs-menu).

As a safety question example, we want to answer whether repeated execution of $\textit{ctrl};\textit{ode}$ keeps the value of $x$ non-negative when started at $x=2$.
In the proof, we want control over when to expand definitions, and we want to structure the proof into a main theorem and supporting lemmas.
fig:expanddefs illustrates the proof steps.

ids|id using S(x)

x ≥0x=-xx ≥0

x ≥0x=-xx ≥0

Exponential decay lemma

S(x) S(x)P

Unsatisfied control guard lemma

Induction step lemma, appeals to exponential decay lemma and unsatisfied guard lemma

x=2x ≥0

A(x) (ctrl;ode)S(x)

Main theorem proves loop induction base case and use case, appeals to fig:expanddefs-step for the induction step.

The substitutions collected during step  and step  are $\sigma=\usubstlist{\usubstmod{A(\cdot)}{\cdot=2},\usubstmod{S(\cdot)}{\cdot \geq 0},\usubstmod{ctrl}{\pchoice{\ptest{S(x)}}{\ptest{\neg S(x)}}},\usubstmod{ode}{\pevolve{\D{x}=-x}},\usubstmod{P}{\dibox{ode}S(x)}}$, so the proof shows validity of the concrete formula $x=2 \limply \dibox{\prepeat{\bigl((\pchoice{\ptest{x \geq 0}}{\ptest{\neg x \geq 0}});\{\D{x}=-x\}\bigr)}}x \geq 0$.

The proof proceeds from the initial conjecture $\lsequent{A(x)}{\dibox{\prepeat{(\textit{ctrl};\textit{ode})}}S(x)}$ bottom-to-top, with proof step justifications annotated to the left of the horizontal bars.
Validity transfers top-to-bottom, so validity of the sequents (subgoals) above a horizontal bar justifies validity of the conclusion below the horizontal bar.
The first step implyr makes the left-hand side of the implication available as assumptions $A(x)$.
Next, step loop induction splits the proof into three subgoals: the base case $\lsequent{A(x)}{S(x)}$, which closes by real arithmetic qear after expanding the definitions, the use case $\lsequent{S(x)}{S(x)}$ that is trivially true by step id, and the induction step.
The induction step in fig:expanddefs-step first addresses the sequential composition with step composeb to isolate $\textit{ctrl}$ from $\textit{ode}$, then expands $\textit{ctrl}$ to split into its two cases:

* on the left branch, the condition of $\text{if}~(S(x))$ is true (represented with $\ptest{S(x)}$) and preserved by the program $\ptest{S(x)};\humod{x}{2}$ as witnessed by a monotonicity step MR and, thus, the exponential decay lemma applies;

* on the right branch with its leading test $\ptest{\neg S(x)}$ the unsatisfied control guard lemma applies.

The main proof management features used in the proof are step expand to expand definitions, step by to apply a lemma, and  to temporarily restrict reasoning to certain formulas.
To users, the proof in fig:expanddefs appears as if they were working on a single  and the proof steps were combined immediately.
Doing so, however, would require extensive changes to the soundness-critical core and violate the local nature of its reasoning.
Behind the scenes, this proof therefore requires a shift from operating on a single  to keeping track of loosely connected sub-proofs outside the prover core; these sub-proofs fit together only after applying the substitutions collected during the proof.
In the following sections, we provide details on explicit proof management that structures proofs into lemmas and implicit proof management that delays merging  and applying uniform substitutions.

§ EXPLICIT PROOF MANAGEMENT WITH LEMMAS

The input format allows explicit proof management in the input format for users to structure their problem descriptions into lemmas that are shared between proofs, and theorems, which appeal to lemmas to show some of their subgoals.
For example, the “Exponential decay” and “Unsatisfied control guard” lemmas from fig:expanddefs-decaylemma and fig:expanddefs-lemma are expressed in the ASCII input syntax below, recorded from the steps of the interactive proofs in fig:expanddefs-decaylemma and fig:expanddefs-lemma.
Optional “/” in lemma names structure the lemmas into folders on both the user interface and the file system.
Lemma "FIDE21/Exponential decay"
ProgramVariables Real x; End.
Problem x>=0 -> [x'=-x]x>=0 End.
Tactic "Recorded" implyR('R=="x>=0 -> [x'=-x]x>=0"); ODE('R=="[x'=-x]x>=0") End.
Tactic "Automated proof" autoClose End.
Lemma "FIDE21/Unsatisfied control guard"
Definitions		 /* constants, functions, properties, programs */
Bool S(Real x);
Bool P(Real x);
ProgramVariables Real x; End.       /* variables */
Problem	S(x) -> [?!S(x);]P(x) End.  /* specification in dL */
Tactic "Interactive proof"
implyR('R=="S(x) -> [?!S(x);]P(x)");
implyR('R=="!S(x) -> P(x)");
id using "S(x)"
Tactic "Automated proof" autoClose End.

The “Induction step” lemma below uses the earlier two lemmas in its proof.
It follows the steps in fig:expanddefs-step largely verbatim, but the specific lemma application steps are worth noting.
Applying the “Exponential decay” lemma is straightforward by auto, since it uses $S(x)$ and $\textit{ode}$ in their expanded form as the only difference between the subgoal and the lemma conclusion.
The “Unsatisfied control guard” lemma, however, introduces a new predicate symbol $P(x)$, which is neither present in the induction step nor in the original conjecture.
We, therefore, use substitution $\sigma=\usubstlist{\usubstmod{P(x)}{\dbox{\humod{x}{x}}\dbox{\ptest{\ltrue}}\dbox{\pevolve{\D{x}=-x}}S(x)}}$ to tell the lemma application mechanism how to resolve $P(x)$.[The leading self-assignment $\humod{x}{x}$ is a necessary technicality to make variable $x$ must-bound because the differential equation $\D{x}=-x$ may run for duration $0$.]
Lemma "FIDE21/Induction step"
Bool S(Real x) <-> x>=0;
HP ctrl ::=  if (S(x))  x:=2*x;  ;
HP ode ::=  x'=-x ;
ProgramVariables Real x; End.
Problem S(x) -> [ctrl;ode;]S(x) End.
Tactic "Proof induction step"
expand "ctrl";
andR('R=="[?S(x);x:=2*x;][ode;]S(x)     [?!S(x);?true;][ode;]S(x)"); <(
MR("S(x)", 'R=="[?S(x);x:=2*x;][ode;]S(x)"); <(
"Use Q->P": expand "S"; autoClose,
"Show [a]Q": useLemma("FIDE21/Exponential decay", "US(`S(x) >x>=0 :: ode; >x'=-x :: nil`);unfold;id")
useLemma("FIDE21/Unsatisfied control guard", "US(`P(x) >[x:=x;][?true;][x'=-x]S(x) :: nil`);unfold;id")

The main theorem of fig:expanddefs-main is expressed in ASCII syntax below.
Its proof uses the “Induction step” lemma in a straightforward way.
Theorem "FIDE21/Combine lemmas"
Bool A(Real x) <-> x=2;
Bool S(Real x) <-> x>=0;
HP ctrl ::=  if (S(x))  x:=2*x;  ;
HP ode ::=  x'=-x ;
ProgramVariables Real x; End.
Problem A(x) -> [ctrl;ode;*]S(x) End.
Tactic "Interactive proof"
loop("S(x)", 'R=="[ctrl;ode;*]S(x)"); <(
"Init": expandAllDefs; QE,
"Post": id,
"Step": expandAllDefs; useLemma("FIDE21/Induction step", "prop")

Structuring proofs into lemmas and theorems need not necessarily be done when creating the input file.
As an alternative, the user interface allows users to start lemmas from any proof state; lemma proofs remain linked from the tabs representing open subgoals in the main proof until finished.
Other pre-existing lemmas can be searched and applied from the user interface as in fig:applylemma.
Techniques for implicit proof management and delayed substitution (used in the proofs above) are discussed next.

Applying a lemma from the lemma search dialog in

§ IMPLICIT PROOF MANAGEMENT WITH DELAYED SUBSTITUTION

In this section, we discuss the fundamental proof management technique of delayed proof composition and delayed uniform substitution, and then devise several applications of it for enabling parametric proofs and delayed modeling, and for temporary sub-proofs focusing on some select aspects of a subgoal.

§.§ Delayed Proof Composition and Delayed Uniform Substitution

As illustrated in sec:preliminaries, the core creates and modifies proof state without keeping track of the steps of the proof.
records proof steps outside the core with a separate  per proof step.
This trace of  not only is the basis for rendering and navigating the sequent calculus proof on the user interface, but also gives us freedom to choose when to combine .
Instead of combining provables and applying uniform substitutions immediately at every step in the proof, those separate  are combined to a single proof once all the steps are finished.
The advantage of delayed merging is that we can postpone the uniform effect <cit.> of uniform substitution across subgoals of a .
Without delayed merging, symbols that are expanded on one branch would immediately be expanded uniformly across all other branches of the proof, even if those other branches would prefer to continue using symbols in their unexpanded form.
The different points of expanding symbols are then reconciled in the final proof checking pass that combines : uniform substitutions that originate from explicit user interactions (e.g., from expanding definitions) are combined with substitutions found through unification.

§.§ Parametric Proofs and Delayed Modeling

Theorem proving is not merely a tool to just obtain a correctness proof about an already correct system; it is a tool to explore and understand a system in all its subtleties and with all its corner cases thoroughly, to discover properties of the system that are not or only partially known, and to discover and fix correctness bugs in the process.
We, therefore, frequently want to make progress in a proof without yet committing to specific inputs or even without supplying a finished model and/or conjecture.
For example, we may want to analyze a loop, but do not yet know a concrete loop invariant that we could use in the proof.
An obvious technique is to use loop unrolling to debug the behavior of the loop body in an attempt to manually identify a loop invariant candidate.
However, this is usually not a suitable technique to prove safety of a loop, and  so requires duplicate proof effort once a loop invariant candidate is identified through debugging (and perhaps several rounds of alternating debugging and proof attempts).

Parametric Proofs A powerful alternative technique are parametric proofs <cit.> to advance in a proof without committing to concrete inputs early in a proof.

x=2x ≥1

x ≥11+x-1/2 ≥1

x ≥1x ≥-1

J(x)x ≥-1

x=2(x1+x-1/2)x ≥-1

Parametric sequent proof

(start) ;
[draw,dashed,text width=0.8cm,minimum height=.5cm] at (-5,2.9) (menuanchor) ;
[below left=0cm and -1.8cm of start.west,anchor=east,draw,dashed] (menu)

[-,dashed] (menuanchor.south west) – (menu.north west);
[-,dashed] (menuanchor.south east) – (menu.north east);

Starting a parametric proof in by using an uninterpreted predicate symbol as tactic input; the proof parameter is then definable from a text field in the “Defs” menu.

Parametric loop induction with abstract invariant $J(x)$.
The substitution $\sigma=\{J(\cdot)\mapsto \cdot \geq 1\}$ supplies a concrete loop invariant to close all three branches of the proof, but any other substitution $\sigma=\{J(\cdot)\mapsto \cdot \sim y\}$ with $\sim\, \in \{\geq,>\}$ and $y \in [-1,1]$ would work as well.

Parametric proofs allow users to proceed with abstract terms or formulas whose concrete shape is discovered later during the proof.
Delayed merging of  and delayed uniform substitution allow users to supply concrete terms, formulas, and programs for function symbols, predicate symbols, and program symbols at any point in the proof, which then get automatically applied to all prior proof steps upon composition of the final .

In fig:parametricloopproof, step loop uses an uninterpreted predicate symbol $J(x)$ instead of a concrete formula as a loop invariant.
That way, we can advance the proof on all three branches until we find that $J(x)$ simultaneously has to fit $\lsequent{x=2}{J(x)}$ in the induction base case, $\lsequent{J(x)}{J(1+\frac{x-1}{2})}$ in the induction step, and $\lsequent{J(x)}{x \geq -1}$ in the induction use case.
At this point, we can experiment with different choices of $J(x)$ and, ultimately, settle for $\sigma=\usubstlist{\usubstmod{J(\cdot)}{\cdot \geq 1}}$.
Uniformly substituting this choice into the entire  concludes the proof by qear on all branches.

Delayed Modeling
Delayed merging of  and delayed substitution are also helpful to address a common nuisance in proofs: missing assumptions about model parameters (e.g., to avoid division by zero) are easily forgotten and their absence becomes apparent often only rather late in a proof.
Using an arity 0 predicate symbol in the model allows users to supply missing assumptions during a proof as they are discovered, without requiring to redo the proof.
For example, the proof in fig:delayedassumptions uses an arity 0 predicate symbol $p_\text{\faShoppingCart}$ that can be used to collect missing assumptions as they become apparent in the proof.
The effect of collecting assumptions during the proof is achieved by simply augmenting the concrete assumption with another fresh $p_{\text{\faShoppingCart}i}$.

x ≥0, y ≠0x/y^2 ≥0

x ≥0, p_x/y^2 ≥0
x ≥0, p_xx/y^2x ≥0

Predicate $p_\text{\faShoppingCart}$ to supply assumptions during the proof.
The substitution $\sigma=\{p_\text{\faShoppingCart}\mapsto y\neq0\}$ results in the proof showing validity of the sequent $\lsequent{x\geq 0,y\neq 0}{\dibox{\prepeat{(\humod{x}{\frac{x}{y^2}})}}x\geq0}$.

[below left=1.5cm and 1.8cm of sequent.north,anchor=north west,draw,dashed] (menu)

[below right=0.8cm and 1.7cm of sequent.north west,text width=0.8cm,minimum height=0.5cm,draw,dashed] (menuanchor) ;
[-,dashed] (menuanchor.south west) – (menu.north west);
[-,dashed] (menuanchor.south east) – (menu.north east);

Providing assumptions with the “Defs” menu

Delayed modeling by using uninterpreted predicate symbols in the input

Note that a proof parameter $J(x)$ cannot be used to introduce the missing assumption $y \neq 0$ because that fact was not even available in the original conjecture and therefore would not be provable in the base case of the induction proof.
We use $p_\text{\faShoppingCart}$ to allow limited fixing of model mistakes during the proof; in the proof in fig:delayedassumptions it is important that $p_\text{\faShoppingCart}$ is an arity 0 predicate symbol whose free variables do not overlap with the variables bound in the loop, so that it stays available in the induction step of the proof.
The conjecture of fig:delayedassumptions is expressed below in ASCII input syntax.
Problem A__0() -> x>=0 -> [x:=x/y()2;]x>=0 End.

§.§ Temporary Implicit Sub-Proofs with Select Formulas

Applying tactics, axioms, and proof rules has permanent effect on the proof state.
For example, weakening assumptions permanently removes formulas from the proof state; if weakening is done for convenience to focus on specific aspects of the proof, we cannot undo the effect of weakening when the hidden formulas become useful again later in the proof.
Not focusing, however, is not an option either, because the mere presence of additional assumptions and formulas may result in duplicate proof effort or intractable proofs (e.g., when applying real arithmetic decision procedures with non-trivial complexity).

We want to keep temporary operations separate from the soundness-critical prover core, because their effect is not compatible with its local isolated reasoning principles.
It would be unsound to temporarily exclude formulas so that they are not affected by tactic applications.
fig:temphide-ok illustrates an example with the wanted effect of temporarily hiding formulas, but fig:temphide-assignunsound shows that care needs to be taken to not unsoundly exclude formulas temporarily from being affected by, e.g., the assignment axiom.
In order to fix fig:temphide-assignunsound, the prover core would need to know which axiom or rule can soundly ignore temporarily hidden facts under what conditions.
With an implicit sub-proof as in fig:temphide-assignok we can temporarily focus tactic application on some proof aspects without extending the core or sacrificing soundness.
As an additional benefit, the abbreviations $P_\text{\faEyeSlash}(x)$ have simpler structure than the fully expanded formulas, which makes tactic applications less expensive even if they have to operate on $P_\text{\faEyeSlash}(x)$.

x<0 x=0,y=xxy ≤y^2

x<0 x=0,y>0xy ≤y^2

x<0 x=0,y>0xy ≤y^2

x<0 x=0,y=x y>0xy ≤y^2
x<0 x=0,y=x y>0xy ≤y^2

Wanted effect of temporarily hiding a formula: ignore for some proof steps, re-introduce when needed

Unsoundly ignoring temporarily hidden formula

Sub-proof with substitution $\sigma=\{P_\text{\faEyeSlash}(\cdot)\mapsto \cdot=0\}$

Hiding formulas temporarily on the user interface

Sub-proof allows hiding explicit formula structure to temporarily focus tactic application on relevant formulas without sacrificing soundness.

In tactics, temporarily focusing on a subset of the sequent formulas is supported with the notation .
For example, the proof of fig:temphide-ok is expressed as follows:

(orL('L)*; <(QE, skip)) using "y=x|y>0 :: x*y<=y^2 :: nil"; QE

This script advances the proof fully on the left branch, but postpones the final qear () step of the right branch using  until after the  block.

§ CONCLUSION

Uniform substitution in hybrid systems is a powerful technique for implementing hybrid systems theorem provers in an LCF-style approach, but it comes at the expense of proof convenience when sticking exclusively to core operations.
We illustrated how proof convenience can be regained with proof management features that are implemented on top of uniform substitution outside the soundness-critical core of a theorem prover, and we complement those features with modeling conventions and corresponding treatment in the user interface.

This approach of using modeling conventions and making proof steps implicit through other user interactions sits somewhat between auto-active verifiers and full interactive theorem proving.
Auto-active verifiers, such as Dafny <cit.> and AutoProof <cit.> hide verification and interaction with the verification tool entirely behind annotations in the analyzed code.
Interactive theorem provers, such as Coq <cit.> and Isabelle/HOL <cit.>, primarily interact with users through scripts, such as structured proofs in Isabelle/Isar <cit.> and  hide only little of the proof complexity behind other means of presentation even in advanced editors <cit.> or when proofs are found automatically, e.g., with Sledgehammer <cit.>.
Many (hybrid systems) theorem provers (e.g., <cit.>) opt for implementing their proof calculus using axiom schemata or with trusted rules, which renders the features presented here soundness-critical.
Our proof management techniques, in contrast, provide proof convenience without sacrificing soundness.

For future work, we plan to automate unification steps in applying lemmas to bridge the syntactic differences between lemma conclusion and target subgoal, and seek to exploit uniform substitution for further proof techniques.


# On Data-Driven Drawdown Control
with Restart Mechanism in Trading

Chung-Han Hsieh  Department of Quantitative Finance,
National Tsing Hua University, Hsinchu 30044, Taiwan R.O.C.
(e-mail: ch.hsieh@mx.nthu.edu.tw).

###### Abstract

This paper extends the existing drawdown modulation control policy to include
a novel restart mechanism for trading. It is known that the drawdown
modulation policy guarantees the maximum percentage drawdown no larger than a
prespecified drawdown limit for all time with probability one. However, when
the prespecified limit is approaching in practice, such a modulation policy
becomes a stop-loss order, which may miss the profitable follow-up
opportunities, if any. Motivated by this, we add a data-driven restart
mechanism into the drawdown modulation trading system to auto-tune the
performance. We find that with the restart mechanism, our policy may achieve a
superior trading performance to that without the restart, even with a nonzero
transaction costs setting. To support our findings, some empirical studies
using equity ETF and cryptocurrency with historical price data are provided.

###### keywords:

Control applications, stochastic systems, algorithmic trading, financial
engineering, drawdown control.

††thanks: This paper was supported in part by Ministry of Science and
Technology, R.O.C. Taiwan, under Grant: MOST 111–2221–E–007–124– .

##  1 Introduction

Starting from the pioneering work by Markowitz (1952, 1959), the portfolio
optimization problem is often solved by the mean-variance approach. That is,
the trader seeks an optimal trade-off between payoff and risk measured by the
portfolio returns’ mean and variance. While the variance is widely used as a
standard risk metric in finance, it is more to the dispersion risk, which
treats both positive and negative deviation from the mean as equally risky;
see Fabozzi et al. (2007) for a good introduction to this topic.

###  1.1 Downside Risks

To remedy the equal riskiness on the dispersion risks, many surrogate risk
measures are proposed to pay attention to the downside risks. This includes
Value at Risk (VaR); see Jorion (2000), Conditional Value at Risk (CVaR); see
Rockafellar and Uryasev (2000), absolute drawdown; see Magdon-Ismail and Atiya
(2004); Hayes (2006), conditional expected drawdown (CED), the tail mean of
maximum drawdown distributions, see Goldberg and Mahmoud (2017), and the more
general coherent risk that axiomatize the risk measures; see Luenberger
(2013); Shapiro et al. (2021). See also Korn et al. (2022) for an empirical
study of comparing various drawdown-based risk metrics. In this paper, we
focus on a more practical drawdown measure, the maximum percentage drawdown,
the maximum percentage drops in wealth over time, as the risk measure.

###  1.2 Control of Drawdown

Different types of drawdown and methodologies are studied extensively in the
existing literature. For example, optimal drawdown control problem in a
continuous-time setting are studied in Grossman and Zhou (1993); Cvitanic and
Karatzas (1994); Chekhlov et al. (2005); Malekpour and Barmish (2012, 2013).
See also Boyd et al. (2017) for a study on multiperiod portfolio optimization
problems involving drawdown as a constraint in a discrete-time setting. A
recent study that uses deep reinforcement learning to address practical
drawdown issues can be found in Wu et al. (2022).

Among all the existing papers, the prior works in Hsieh and Barmish (2017a, b)
are the most closely related papers, where the key result, the so-called
drawdown modulation lemma, is proved. Roughly speaking, it shows a necessary
and sufficient conditions for a broad class of control policies that
guarantees an almost sure maximum percentage drawdown protection for all time.
However, Hsieh and Barmish (2017a) indicate that, in practice, when the
prespecified drawdown limit is approaching, the trading policy may behave like
a stop-loss order, and the trading may be stopped; see also Hsieh (2022a) for
a study on a class of affine policies with a stop-loss order. To this end, we
extend the drawdown modulation policy with a novel restart mechanism to remedy
the stop-loss phenomenon.

###  1.3 Contributions of the Paper

This paper extends the existing drawdown modulation policy with a novel
restart mechanism. The preliminaries are provided in Section 2. We formulate
an optimal drawdown control problem for a two-asset portfolio with one risky
and one riskless asset. Then we extend the existing drawdown modulation theory
so that the riskless asset is explicitly involved; see Lemma 3.1. The
necessary and sufficient conditions for a broad class of control policy which
we call the drawdown modulation policy are provided. Then, the modulation
policy with a restart mechanism is discussed in Section 3. The idea of the
restart is simple: When the percentage drawdown up-to-date is close to the
prespecified drawdown limit, we restart the trades with an updated policy. We
also provide numerical examples involving ETF and cryptocurrency historical
price data to support our findings; see Section 4.

##  2 Preliminaries

We now provide some useful preliminaries for the sections to follow.

###  2.1 Asset Trading Formulation

Fix an integer $N>0.$ For stage $k=0,1,\dots,N$, we let $S(k)>0$ denote the
prices of the underlying financial asset at stage $k$. The associated per-
period returns are given by $X(k):=\frac{S(k+1)-S(k)}{S(k)}$ and the returns
are assumed to be bounded, i.e., $X_{\min}\leq X(k)\leq X_{\max}$ with
$X_{\min}$ and $X_{\max}$ being points in the support, denoted by
$\mathcal{X}$, and satisfying $-1<X_{\min}<0<X_{\max}.$ For the money market
asset, e.g., bond or bank account, we use $r_{f}(k)$ to denote the interest
rate at stage $k$.

###### Remark 2.1

Note that the returns considered here are not necessarily independent and can
have an arbitrary but bounded distribution with the bounds $X_{\min}$ and
$X_{\max}$.

###  2.2 Account Value Dynamics

Beginning at some initial account value $V(0)>0$, consider a portfolio
consisting of two assets, with one being risky and the other being a riskless
asset with interest rate $r_{f}(k)\in[0,X_{\max}]$ for all $k$ almost surely.
For stage $k=0,1,\dots$, we let $V(k)$ denote the account value at stage $k$.
Then the evolution of the account value dynamics is described by the
stochastic recursion

$\displaystyle V(k+1)=V(k)+u(k)X(k)+(V(k)-u(k))r_{f}(k).$

Given a prespecified drawdown limit $d_{\max}\in(0,1)$, we focus on conditions
on selecting a policy $u(k)$ under which satisfaction of the constraint
$d(k)\leq d_{\max}$ is assured for all $k$ with probability one where $d(k)$
is the percentage drawdown up to date $k$, which is defined below.

######  Definition 2.1 (Maximum Percentage Drawdown)

For $k=0,1,\dots,N$, the percentage drawdown up to date $k$, denoted by
$d(k)$, is defined as

$d(k):=\frac{V_{\max}(k)-V(k)}{V_{\max}(k)}$

where $V_{\max}(k):=\max_{0\leq i\leq k}V(i).$ The maximum percentage
drawdown, call it $d^{*}$, is then defined as

$d^{*}:=\max_{0\leq k\leq N}d(k).$

###### Remark 2.2

It is readily seen that the percentage drawdown satisfies $d(k)\in[0,1]$ for
all $k$ with probability one.

##  3 Drawdown Modulation with Restart

According to Hsieh and Barmish (2017a), it states a necessary and sufficient
condition on any trading policy $u(k)$ that guarantees the percentage drawdown
up to date $d(k)$ is no greater than a given level $d_{\max}$ for all $k$ with
probability one. Below, we extend the result to include a riskless asset.

######  Lemma 3.1 (Drawdown Modulation)

Let $d_{\max}\in(0,1)$ be given. An trading policy $u(\cdot)$ guarantees
prespecified drawdown limit satisfying $d(k)\leq d_{\max}$ for all $k$ with
probability one if and only if for all $k$, the condition

$-\frac{M(k)+r_{f}(k)}{X_{\max}-r_{f}(k)}V(k)\leq
u(k)\leq\frac{M(k)+r_{f}(k)}{|X_{\min}|+r_{f}(k)}V(k)$

is satisfied along all sample paths where

$M(k):=\frac{d_{\max}-d(k)}{1-d(k)}.$

Proof. The idea of the proof is similar to that of Hsieh and Barmish (2017a).
However, for the sake of completeness, we provide full proof here. To prove
necessity, assuming that $d(k)\leq d_{\max}$ for all $k$ and all sequences of
returns, we must show the condition on $u(k)$ holds along all sequences of
returns. Fix $k$. Since both $d(k)\leq d_{\max}$ and $d(k+1)\leq d_{\max}$ for
all sequences of returns, we claim this forces the required inequalities on
$u(k)$. Without loss of generality, we prove the right-hand inequality for the
case $u(k)\geq 0$ and note that an almost identical proof also works for
$u(k)<0$. To establish the condition on $u(k)$ for all sequences of returns,
it suffices to consider the path with the worst loss $|X_{\min}|u(k)$. In this
case, we have $V_{\max}(k+1)=V_{\max}(k)$. Hence,

$\displaystyle d(k+1)$
$\displaystyle=\frac{V_{\max}(k+1)-V(k+1)}{V_{\max}(k+1)}$
$\displaystyle=\frac{V_{\max}(k)-V(k+1)}{V_{\max}(k)}$
$\displaystyle=\frac{V_{\max}(k)-V(k)+u(k)|X_{\min}|-(V(k)-u(k))r_{f}(k)}{V_{\max}(k)}$
$\displaystyle=d(k)+\frac{u(k)|X_{\min}|-(V(k)-u(k))r_{f}(k)}{V_{\max}(k)}\leq
d_{\max}$

We now substitute ${V_{\max}}(k)=\frac{{V(k)}}{{1-d(k)}}>0$ into the
inequality above and obtain

$|X_{\min}|u(k)-(V(k)-u(k))r_{f}(k)\leq M(k)V(k),$

where $M(k)=\frac{d_{\max}-d(k)}{1-d(k)}$. This implies that

$(|X_{\min}|+r_{f}(k))u(k)\leq\left(M(k)+r_{f}(k)\right)V(k).$

Or equivalently,

$u(k)\leq\frac{M(k)+r_{f}(k)}{|X_{\min}|+r_{f}(k)}V(k).$

To prove sufficiency, assuming that the stated bounds on $u(k)$ hold along all
sequences of returns, we must show $d(k)\leq d_{\max}$ for all $k$ and all
sequences of returns. Proceeding by induction, for $k=0$, we trivially have
$d(0)=0\leq d_{\max}$. To complete the inductive argument, we assume that
$d(k)\leq d_{\max}$ for all sequences of returns, and must show $d(k+1)\leq
d_{\max}$ for all sequences of returns. Without loss of generality, we again
provide a proof for the case $u(k)\geq 0$ and note that a nearly identical
proof is used for $u(k)<0$. Indeed, by noting that

$\displaystyle d(k+1)$ $\displaystyle=1-\frac{{V(k+1)}}{{{V_{\max}}(k+1)}},$

and $V_{\max}(k)\leq V_{\max}(k+1)$ for all sequences of returns, we split the
argument into two cases: If $V_{\max}(k)<V_{\max}(k+1)$, then
$V_{\max}(k+1)=V(k+1)$ and we have $d(k+1)=0\leq d_{\max}.$ On the other hand,
if $V_{\max}(k)=V_{\max}(k+1)$, with the aid of the dynamics of account value,
we have

$\displaystyle d(k+1)$
$\displaystyle=1-\frac{V(k)+u(k)X(k)+(V(k)-u(k))r_{f}(k)}{V_{\max}(k)}$
$\displaystyle\leq
1+\frac{-V(k)(1+r_{f}(k))+u(k)(|X_{\min}|+r_{f}(k))}{V_{\max}(k)}.$

Using the upper bound on $u(k)$; i.e.,

$u(k)\leq\frac{M(k)+r_{f}(k)}{|X_{\min}|+r_{f}(k)}V(k)$

and ${V_{\max}}(k)=\frac{{V(k)}}{{1-d(k)}},$ we obtain

$\displaystyle d(k+1)$ $\displaystyle\leq 1+(-1+M(k))(1-d(k))$
$\displaystyle=d(k)+M(k)(1-d(k)).$

Using the definition of $M(k)=\frac{d_{\max}-d(k)}{1-d(k)}$, it follows that
$d(k+1)\leq d_{\max},$ and the proof is complete. ∎

###  3.1 Drawdown Modulation Policy

Consistent with Hsieh and Barmish (2017a), fix the prespecified drawdown limit
$d_{\max}\in(0,1)$. With the aid of Lemma 3.1, one can readily obtain a class
of policy functions $u(k)$ expressed as a linear time-varying feedback
controller parameterized by a gain $\gamma$, leading to the satisfaction of
the drawdown specification. Specifically, we express $u(k)$ in the feedback
form

$\displaystyle u(k):=K(k)V(k)$ (1)

with $K(k):=\gamma M(k)$ and

$\gamma\in\Gamma:=\left[\frac{-1}{X_{\max}-\max_{k}r_{f}(k)},\,\frac{1}{|X_{\min}|+\max_{k}r_{f}(k)}\right].$

Equation (1) is called the drawdown modulation policy, which is parameterized
by the two parameters $(\gamma,d_{\max})$.

###### Remark 3.1

$(i)$ It is readily verified that the drawdown modulation policy (1) satisfies
Lemma 3.1. $(ii)$ To link back to finance concepts, the special case of buy-
and-hold is obtained when $K(k)\equiv 1$. Note that $u(k)<0$ stands for short
selling.111Short selling a stock means that a trader borrows the stocks from
someone who owns it and selling it with the hope that the prices of the stock
will drop in the near future; see Luenberger (2013). $(iii)$ Instead of using
a fixed feasible set $\Gamma$, it is also possible to allow a time-varying
feasible set, say $\Gamma_{k}$, to reflect the time dependency of the returns.

######  Corollary 3.1 (Maximum Drawdown Protection)

With the drawdown modulation policy (1), the maximum percentage drawdown
satisfies $d^{*}\leq d_{\max}$.

Proof. Since the drawdown modulation policy satisfies Lemma 3.1, it assures
$d(k)\leq d_{\max}$ for all $k$ with probability one. Therefore, it follows
that

$d^{*}=\max_{0\leq k\leq N}d(k)\leq d_{\max}.\qed$

###  3.2 Optimal Drawdown Control Problem

Having obtained the drawdown modulation policy (1), a natural question arises
of how to select an “optimal” $\gamma.$ To this end, we define the total
return up to terminal stage $N$ as a ratio

$R_{\gamma}(N):=\frac{V(N)}{V(0)}$

where the subscript of $R_{\gamma}(\cdot)$ is used to emphasize the dependence
on the gain $\gamma$. Define $J(\gamma):=\mathbb{E}[R_{\gamma}(N)]$. Then, we
consider a multiperiod drawdown-based stochastic optimization problem

$\displaystyle J^{*}:=\max_{\gamma\in\Gamma}J(\gamma)$

subject to

$\displaystyle V(k+1)$ $\displaystyle=V(k)+u(k)X(k)+(V(k)-u(k))r_{f}(k)$
$\displaystyle=[1+r_{f}(k)+\gamma M(k)(X(k)-r_{f}(k))]V(k).$

It is readily verified that

$\frac{V(N)}{V(0)}=\prod_{k=0}^{N-1}[1+r_{f}(k)+\gamma M(k)(X(k)-r_{f}(k))].$

Therefore, we rewrite the problem as the following equivalent form

$\displaystyle\max_{\gamma\in\Gamma}\mathbb{E}[R_{\gamma}(N)]$
$\displaystyle=\max_{\gamma\in\Gamma}\mathbb{E}\left[\prod_{k=0}^{N-1}[1+r_{f}(k)+\gamma
M(k)(X(k)-r_{f}(k))]\right].$ (2)

In the sequel, we shall use $\gamma^{*}$ to denote a maximizer of the
optimization problem above. In practice, if one view that the optimum
$\gamma^{*}$ obtained may be too aggressive, a practical but arguably
suboptimal way is to introduce an additional fraction, call it $\alpha$, that
is used to shrink the investment size; see Maclean et al. (2010) for a similar
idea. That is, instead of working with $\gamma^{*}$, one may work with
$\alpha\gamma^{*}$ where $\alpha\in(0,1]$.

######  Remark 3.2 (Non-Convexity)

It is important to note that solving Problem (3.2) is challenging since the
modulation function $M(k)$ depends on $\gamma$ and the history of
$X(0),\dots,X(k-1)$, which in general yields a nonconvex problem; e.g., see
Figure 4 in Section 4 for an illustration of non-convexity nature. Therefore,
Monte-Carlo simulations are often needed to obtain the optimum.

###  3.3 Modulation with Restart

As mentioned in Section 1, while the derived drawdown modulation policy
provides almost sure drawdown protection, it may incur a stop-loss behavior.
To remedy this, we now introduce a restart mechanism into the modulation
policy. Specifically, let $\varepsilon\in(0,d_{\max})$ be a prespecified
threshold parameter. Then we set the threshold for restarting the trade by

$\displaystyle d(k)+\varepsilon>d_{\max}$ (3)

If, at some stage $k=k_{0}$, Inequality (3) is satisfied, the trading is
restarted by re-initializing $d(k_{0}):=0$ and reset the time-varying gain
function $K(k)$ of the modulation policy $u(k)=K(k)V(k)$ at that stage
$k=k_{0}$ as

$\displaystyle K(k_{0}):=\gamma^{*}\alpha e^{-k_{0}/N}M(k_{0})$ (4)

where $\alpha e^{-k_{0}/N}$ represents a forgetting factor with fraction
$\alpha\in(0,1]$ mentioned previously. Then we continue the trade until the
next restart stage or to the terminal stage $N$.

###### Remark 3.3

$(i)$ The forgetting factor in Equation (4) reflects the idea that the trading
size should be shrunk after the restart. Said another way, if the trades are
approaching the prespecified drawdown limit $d_{\max}$, the follow-up trades
should be more conservative after the restart. $(ii)$ Note that after the
restart, the control policy satisfies $|u(k_{0})|\leq|\gamma^{*}|\alpha
d_{\max}$ since $M(k)\leq d_{\max}$ for all $k$ with probability one. $(iii)$
While it does not consider in this paper, we should note that the optimal
$\gamma^{*}$ in Equation (4) can also be re-calculated at each restart time by
using the previous $k_{0}-m$ stages information for some integer $m>1$; see
also Wang and Hsieh (2022) for a similar idea for obtaining a data-driven log-
optimal portfolio via a sliding-window approach.

##  4 Illustrative Examples

In this section, two trading examples are proposed to support our theory. The
first example is trading with ETF and riskless asset. The second example is
trading with Bitcoin and a riskless asset. For the sake of simplicity, we take
a constant daily interest rate $r_{f}(k):=0.01/365$ for all $k$, which
corresponds to a $1\%$ annual rate. While our theory allows leveraging, in the
sequel, we impose an additional cash-financing condition by imposing that
$|u(k)|\leq V(k)$ for all $k$, which corresponds to $|K^{*}(k)|\leq 1.$

###  4.1 Trading with ETF and Riskless Asset

Consider the Vanguard Total World Stock Index Fund ETF (Ticker: VT)222VT
invests in both foreign and U.S. stocks; hence it can be viewed as a good
representative of the global stock market to be the risky asset covering a
one-year in-sample period for optimization from January 02, 2019 to January
02, 2020, and the out-of-sample period from January 02, 2020 to September 20,
2022, which contains a total of $N=684$ trading days; see Figure 2 where the
cyan colored trajectory is used for in-sample optimization and the blue
colored trajectory is used for the out-of-sample trading test. It should be
noted that due to the COVID-19 pandemic, the considered prices covering the
2020 stock market crash from February 20, 2020 to April 7, 2020, and a
recovery period after the crash. Thus, we view this dataset as an excellent
back-testing case for our proposed drawdown modulation policy with the
restart.

Figure 1: Stock Prices of VT

Without loss of generality, consider the initial account value to be
$V(0):=\$1$. To implement the drawdown modulation policy with restart, we set
$d_{\max}:=0.1$ and restart threshold $\varepsilon:=d_{\max}/10$. With the
data collected in the in-sample period, the corresponding feasible set is
$\Gamma\approx[-30.79,\;34.9]$. Then we numerically solve the optimization
problem (3.2) via Monte-Carlo simulations. It follows that any
$\gamma\in(8.5,34.9)$ share an almost identical optimal value when the cash-
financing condition is imposed. For the sake of risk-averseness, we pick the
infimum of the candidates, i.e., $\gamma^{*}:=8.5$. Using this $\gamma$, we
obtain the drawdown modulation policy $u^{*}(k)=\gamma^{*}M(k)V(k).$

The corresponding trading performance is shown in Figure 2, where the green
dots indicate that the trade is restarted. In the same figure, we also compare
it with the standard buy-and-hold strategy333Here, we mean buy and hold on the
risky asset VT with $K(k)=1$. and the modulation policy without restart. We
see clearly that the modulation policy with restart leads to superior
performance. Some key performance metrics, including maximum drawdown and
cumulative rate returns, and $N$-period Sharpe ratio444The per-period Sharpe
ratio is $SR:=\frac{\mu-r_{f}}{\sigma}$ where $\mu$ is the per-period sample
mean return, $\sigma$ is the per-period sample standard deviation, and $r_{f}$
is the per-period riskless return. are reported in Table 1.

Figure 2: Drawdown Modulation with/without Restart (Green Dots Indicate a
Restart) Table 1: Performance Metrics for Trading VT and Riskless Asset
Trading Performance with $d_{\max}=0.1$ and $\varepsilon=d_{\max}/10$
---
Trading Policy | Buy and Hold | Modulation without Restart | Modulation with Restart
Maximum percentage drawdown $d^{*}$ | $34.24\%$ | $10.00\%$ | $\textbf{10.00}\%$
Cumulative rate of return $\frac{V(N)-V(0)}{V(0)}$ | $10.64\%$ | $-8.422\%$ | $\textbf{20.97}\%$
$N$-period Sharpe ratio $\sqrt{N}\cdot SR$ | $0.4082$ | $-1.3375$ | 1.0462

###  4.2 Trading with Cryptocurrency and Riskless Asset

As a second example, we consider a portfolio consisting of cryptocurrency BTC-
USD and a riskless asset. The BTC-USD asset covers the same in-sample and out-
of-sample periods described in Example 4.1. From January 02, 2020 to September
20, 2022, it has a total of $N=993$ trading days555It is worth noting that the
cryptocurrency is typically traded at 24 hours a day, seven days a week.
Therefore, it has longer tradings days than that trades with VT in Section
4.1.; see Figure 3. The corresponding feasible set for $\gamma$ is
$\Gamma=[-5.761,\;7.083]$.

Figure 3: Prices of BTC-USD (In-Sample and Out-of-Sample)

Take $d_{\max}:=0.2$ and restart threshold $\varepsilon:=d_{\max}/10$. By
solving the optimal drawdown control problem (3.2), we obtain
$\gamma^{*}\approx 5.138$; see Figure 4 for $J(\gamma)$ versus
$\gamma\in\Gamma$. Note that the $J(\gamma)$ is clearly not concave for
$\gamma\in\Gamma$. To consider the volatile nature of cryptocurrency and
unforeseen estimation error, we consider using a fractional $\gamma^{*}$ by
$\alpha\gamma^{*}$ with $\alpha=1/2$. That is, $u^{*}(k)=K^{*}(k)V(k)$ with
$K^{*}(k)=\frac{\gamma^{*}}{2}M(k)V(k)$. The trading performances using
drawdown modulation policy with and without restart, and buy-and-hold strategy
are shown in Figure 5, where the green dots indicate that the trades were
restarted. Some performance metrics are summarized in Table 2 where we see
that the modulation with restart provides the highest Sharpe ratio among all
the other strategies.

Figure 4: Seeking the Optimum: $J(\gamma)$ Versus $\gamma\in\Gamma$ Figure 5:
Trading Performance of BTC-USD with $d_{\max}:=0.2$ and
$\varepsilon:=d_{\max}/10$. Table 2: Performance Metrics for Trading BTC-USD
and Riskless Asset Trading Performance with $d_{\max}=0.2$ and
$\varepsilon=d_{\max}/10$
---
Trading Policy | Buy and Hold | Modulation without Restart | Modulation with Restart
Maximum percentage drawdown $d^{*}$ | $72.12\%$ | $20.00\%$ | $\textbf{20.18}\%$
Cumulative rate of return $\frac{V(N)-V(0)}{V(0)}$ | $170.43\%$ | $17.41\%$ | $\textbf{101.82}\%$
$N$-period Sharpe ratio $\sqrt{N}\cdot SR$ | $1.4424$ | $0.6970$ | 2.1363

####  4.2.1 Transaction Costs Considerations.

Traditionally, with cryptocurrency as the underlying asset, most exchanges
typically charge transaction fees from $0\%$ to $1\%$, depending on the
trading volumes. While we are not developing the drawdown modulation theory
involving the transaction costs, in this example, we perform backtests to see
the effects with percentage costs of $0.1\%$ per trade.666 This cost level is
typical in common cryptocurrency exchanges such as Binance; see Hsieh (2022b).
Take $d_{\max}=0.2$, $\varepsilon=d_{\max}/10$ and $\gamma^{*}=2.69$, the
trading performances are shown in Figure 6. From the figure, we see that, even
with transaction costs, the proposed modulation policy with a restart
mechanism is still superior to that without a restart. The corresponding
Sharpe ratio is about $1.521$ compared with that without restart, where the
Sharpe ratio is down to $-0.043$.

Figure 6: Trading Performance with and without Transaction Costs

##  5 Concluding Remarks

This paper extended the existing drawdown modulation policy with a novel data-
driven restart mechanism. We first derived a drawdown modulation policy by
proving a lemma for a two-asset portfolio involving one risky and riskless
asset. Then we modified the derived modulation policy by adding the restart
mechanism. Subsequently, we showed an auto-tuned trading performance using
historical price data for an ETF and cryptocurrency within a duration where
the prices are volatile. Overall, our modulation policy with restart
dynamically controls the drawdown and maintains the profits level.

Some possible future research directions might include the multi-asset
problem, which will be considered in the subsequent journal version of this
paper. The other possibility is to consider the consumption-investment
problem; i.e.,

$\sup_{\gamma}\mathbb{E}\left[\sum_{k=0}^{T-1}U_{1}(c(k))+U_{2}(V(N))\right]$

where $U_{1}$ and $U_{2}$ are two utility functions with $c(k)$ being the
amount consumed at time $k$. See Cvitanic and Zapatero (2004). Lastly, one
might consider a more general portfolio optimization problem that seeks
$\gamma$ maximizing $\sup_{\gamma}\mathbb{E}\left[U(V_{\gamma}(N))\right]$
where $U:\mathbb{R}\to\mathbb{R}$ is a strictly increasing and concave utility
function. One example is to consider a general hyperbolic absolute risk
aversion (HARA) class of utilities; i.e.,

$U(x)=\frac{1-\theta}{\theta}\left(\frac{ax}{1-\theta}+b\right)^{\theta}$

for $a,b>0$ and $\theta<1$. The HARA utility functions include the quadratic,
exponential, and the isoelastic utility function as special cases.

## Acknowledgment

The author thanks Chia-Yin Lee for coding and running some preliminary
numerical examples on the early draft of this paper.

## References

  * Boyd et al. (2017) Boyd, S., Busseti, E., Diamond, S., Kahn, R.N., Koh, K., Nystrup, P., Speth, J., et al. (2017).  Multi-Period Trading via Convex Optimization.  _Foundations and Trends® in Optimization_ , 3(1), 1–76.
  * Chekhlov et al. (2005) Chekhlov, A., Uryasev, S., and Zabarankin, M. (2005).  Drawdown Measure in Portfolio Optimization.  _International Journal of Theoretical and Applied Finance_ , 8(1), 13–58.
  * Cvitanic and Karatzas (1994) Cvitanic, J. and Karatzas, I. (1994).  On Portfolio Optimization Under “Drawdown” Constraints.  _IMA Volumes in Mathematics and its Applications_ , 65, 35–46.
  * Cvitanic and Zapatero (2004) Cvitanic, J. and Zapatero, F. (2004).  _Introduction to the Economics and Mathematics of Financial Markets_.  MIT press.
  * Fabozzi et al. (2007) Fabozzi, F.J., Focardi, S.M., Kolm, P.N., and Pachamanova, D.A. (2007).  _Robust Portfolio Optimization and Management_.  John Wiley & Sons.
  * Goldberg and Mahmoud (2017) Goldberg, L.R. and Mahmoud, O. (2017).  Drawdown: From Practice to Theory and Back Again.  _Mathematics and Financial Economics_ , 11(3), 275–297.
  * Grossman and Zhou (1993) Grossman, S.J. and Zhou, Z. (1993).  Optimal Investment Strategies for Controlling Drawdowns.  _Mathematical Finance_ , 3(3), 241–276.
  * Hayes (2006) Hayes, B.T. (2006).  Maximum Drawdowns of Hedge Funds with Serial Correlation.  _The Journal of Alternative Investments_ , 8(4), 26–38.
  * Hsieh (2022a) Hsieh, C.H. (2022a).  Generalization of Affine Feedback Stock Trading Results to Include Stop-Loss Orders.  _Automatica_ , 136, 110051.
  * Hsieh (2022b) Hsieh, C.H. (2022b).  On Robustness of Double Linear Trading with Transaction Costs.  _To appear in the IEEE Control Systems Letters_.
  * Hsieh and Barmish (2017a) Hsieh, C.H. and Barmish, B.R. (2017a).  On Drawdown-Modulated Feedback Control in Stock Trading.  _IFAC-PapersOnLine_ , 50(1), 952–958.
  * Hsieh and Barmish (2017b) Hsieh, C.H. and Barmish, B.R. (2017b).  On Inefficiency of Markowitz-Style Investment Strategies when Drawdown is Important.  In _Proceedings of the IEEE Conference on Decision and Control (CDC)_ , 3075–3080.
  * Jorion (2000) Jorion, P. (2000).  Value at Risk.
  * Korn et al. (2022) Korn, O., Möller, P.M., and Schwehm, C. (2022).  Drawdown Measures: Are They All the Same?  _The Journal of Portfolio Management_ , 48(5), 104–120.
  * Luenberger (2013) Luenberger, D.G. (2013).  _Investment Science_.  Oxford University Press.
  * Maclean et al. (2010) Maclean, L.C., Thorp, E.O., and Ziemba, W.T. (2010).  Long-Term Capital Growth: the Good and Bad Properties of the Kelly and Fractional Kelly Capital Growth Criteria.  _Quantitative Finance_ , 10(7), 681–687.
  * Magdon-Ismail and Atiya (2004) Magdon-Ismail, M. and Atiya, A.F. (2004).  Maximum Drawdown.  _Risk Magazine_ , 17(10), 99–102.
  * Malekpour and Barmish (2012) Malekpour, S. and Barmish, B.R. (2012).  How Useful Are Mean-Variance Considerations in Stock Trading via Feedback Control?  In _Proceedings of the IEEE Conference on Decision and Control (CDC)_ , 2110–2115.
  * Malekpour and Barmish (2013) Malekpour, S. and Barmish, B.R. (2013).  A Drawdown Formula for Stock Trading via Linear Feedback in a Market Governed by Brownian Motion.  In _Proceedings of the European Control Conference (ECC)_ , 87–92.
  * Markowitz (1952) Markowitz, H.M. (1952).  Portfolio Selection.  _The Journal of Finance_ , 7, 77–91.
  * Markowitz (1959) Markowitz, H.M. (1959).  _Portfolio Selection: Efficient Diversification of Investments_ , volume 16.  John Wiley New York.
  * Rockafellar and Uryasev (2000) Rockafellar, R.T. and Uryasev, S. (2000).  Optimization of Conditional Value-at-Risk.  _Journal of Risk_ , 2, 21–42.
  * Shapiro et al. (2021) Shapiro, A., Dentcheva, D., and Ruszczynski, A. (2021).  _Lectures on Stochastic Programming: Modeling and Theory_.  SIAM.
  * Wang and Hsieh (2022) Wang, P.T. and Hsieh, C.H. (2022).  On Data-Driven Log-Optimal Portfolio: A Sliding Window Approach.  _To appear in the IFAC-PapersOnline_.
  * Wu et al. (2022) Wu, J.M.T., Lin, S.H., Syu, J.H., and Wu, M.E. (2022).  Embedded Draw-Down Constraint Reward Function for Deep Reinforcement Learning.  _Applied Soft Computing_ , 125, 109150.