TITLE: Factorising the supersymmetric oscillator Hamiltonian: what (anti)commutes?
QUESTION [4 upvotes]: In this paper on supersymmetry, the Hamiltonian for the supersymmetric oscillator is given:
$$H = \frac12 p^2 + \frac12 \omega^2 x^2 + \omega\bar\psi\psi.$$
Furthermore, its factorisation is given as
$$H = \omega(a_B^{\dagger}a_B + a_F^{\dagger}a_F)$$
where the creation/annihilation operators have been defined as follows:
$$a_B^{\dagger}=\frac{1}{\sqrt{2\omega}}(-ip+\omega x),\quad a_B=\frac{1}{\sqrt{2\omega}}(ip+\omega x),\quad a_F^{\dagger}=\bar\psi,\quad a_F=\psi.$$
Questions:

In order for this factorisation to work, surely $x$ and $p$ must commute? So I assume $x$, $p$ are just commuting bosonic variables (not operators) and $\psi$, $\bar\psi$ are just anti-commuting fermionic (Grassmann) variables?
Later in the paper it states that $\{Q,\bar Q\}=H/\omega$, this being the anti-commutator between the operators $Q=a_B^{\dagger}a_F$ and $\bar Q=a_F^{\dagger}a_B$. But this can't be true if $x$, $p$ (or $\psi$, $\bar\psi$) commute (or anti-commute). So have they been promoted to operators at this point?
If so and they obey the relations $[x,p]=i$ and $\{\psi,\bar\psi\}=1$, then I find that $\{Q,\bar Q\}\ne H/\omega$. Am I missing something?

REPLY [2 votes]: No. It's like just rewriting of classical Hamiltonan.
Yes. At this point you need consider fields as operators.
Be more accurate. You formulas for commutators are true. I done this calculation and obtained true result.

Details (about operators ambiguities in QM see Operator Ordering Ambiguities, I choosen hermitean hamiltonian):
\begin{equation}
\hat{H}_B = \frac{\omega}{2}(\hat{a}_B^\dagger \hat{a}_B + \hat{a}_B \hat{a}_B^\dagger)
= \omega (\hat{a}_B^\dagger \hat{a}_B +\frac{1}{2})
\end{equation}
\begin{equation}
\hat{H}_F = \frac{\omega}{2} (\hat{a}^\dagger_F \hat{a}_F - \hat{a}_F \hat{a}^\dagger_F )
=
\omega(\hat{a}^\dagger_F \hat{a}_F - \frac{1}{2})
\end{equation}
\begin{equation}
\hat{H} = \hat{H}_B+\hat{H}_F = \omega (\hat{a}_B^\dagger \hat{a}_B + \hat{a}^\dagger_F \hat{a}_F)
\end{equation}
\begin{equation}
\{\hat{Q},\hat{Q}^\dagger \}
=
\{\hat{a}^\dagger_B\hat{a}_F\;,\hat{a}^\dagger_F\hat{a}_B \}
=
\hat{a}^\dagger_B\underbrace{\hat{a}_F \hat{a}^\dagger_F}_{-\hat{a}^\dagger_F \hat{a}_F - 1}\hat{a}_B
+
\hat{a}^\dagger_F\underbrace{\hat{a}_B\hat{a}^\dagger_B}_{\hat{a}^\dagger_B\hat{a}_B + 1}\hat{a}_F
=
 (\hat{a}_B^\dagger \hat{a}_B + \hat{a}^\dagger_F \hat{a}_F)
= \frac{\hat{H}}{\omega}
\end{equation}


text:
\begin{document}
\title{Neostability-properties of Fra\"{\i}ss\'e limits of 2-nilpotent groups of exponent $p> 2$}
\author{Andreas Baudisch}
\date{\today}
\maketitle

\begin{abstract}
\noindent Let $L(n)$ be the language of group theory with $n$ additional new constant symbols $c_1,\ldots,c_n$. In $L(n)$ we consider the class ${\mathbb K}(n)$ of all finite groups $G$ of exponent $p > 2$, where  $G'\subseteq\langle c_1^G,\ldots,c_n^G\rangle \subseteq Z(G)$ and $c_1^G,\ldots,c_n^G$ are linearly independent. Using amalgamation we show the existence of   Fra\"{\i}ss\'e limits $D(n)$ of  ${\mathbb K}(n)$. $D(1)$ is Felgner's extra special $p$-group. The elementary theories of the $D(n)$ are superstable of SU-rank 1. They have the independence property.
\end{abstract}

\section{Introduction}

We consider the variety ${\mathbb G}_{2,p}$ of nilpotent groups of class 2 of exponent $p>2$ in the language $L$ of group theory. To get the Amalgamation Property (AP) in \cite{Bau} an additional predicate $P(G)$ for $G\in{\mathbb G}_{2,p}$ with $G'\subseteq P(G)\subseteq Z(G)$ is  introduced. Let ${\mathbb G}_{2,p}^P$ be the category of this groups in the extended language $L_P$ where the morphisms are embeddings. Using the class ${\mathbb K}_{2,p}^P$ of finite structures in ${\mathbb G}_{2,p}^P$ we get a Fra\"{\i}ss\'e limit $D$. If we build $D$ by amalgamation then $P(a)$ says that $a$ will become an element of the commutator subgroup $D'$ of $D$ in that process. In \cite{Bau} it is shown that ${\rm Th}(D)$ is not simple. Here we point out that $D$ has the tree property of the second kind (TP$_2$). This is easily seen.
\medskip

Let $L(n)$ be the language of group theory with $n$ additional new constant symbols $c_1,\ldots,c_n$. In $L(n)$ we consider the class ${\mathbb G}(n)$ of all groups $G\in {\mathbb G}_{2,p}$, where  $G'\subseteq\langle c_1^G,\ldots,c_n^G\rangle \subseteq Z(G)$ and $c_1^G,\ldots,c_n^G$ are linearly independent. We use linear independence, since we can consider an abelian group of expoent p as a vector space over ${\mathbb F}_p$.  $\langle X \rangle$ denotes the substructure generated by $X$. Hence   $\langle c_1^G,\ldots,c_n^G\rangle = \langle \emptyset \rangle$. ${\mathbb G}(n)$ is uniformly locally finite. Let ${\mathbb K}(n)$ be the class of finite structures in ${\mathbb G}(n)$. ${\mathbb K}(n)$ has the Hereditary Property (HP), the Joint Embedding Property (JEP) and the Amalgamation Property (AP). Hence the Fra\"{\i}ss\'e limit $D(n)$ of the class ${\mathbb K}(n)$ exists. Note that $D(1)$ is the extra special $p$-group considered by U.~Felgner in \cite{Fe}. In \cite{MacSt} the corresponding bilinear alternating map is obtained as an ultraproduct of finite structures.
It is a well-known example of a supersimple theory of SU-rank 1.
\medskip

We show that the theories of all Fra\"{\i}ss\'e limits $D(n)$ are supersimple of SU-rank 1. To prove this we check the properties of non-forking that characterize simple theories \cite{KP}. Before we show that each group $G$ in ${\mathbb G}(n)$ where $G/Z(G)$ is infinite has the Independence Property especially all $D(n)$.

\section{TP{\boldmath$_2$} of {\boldmath${\rm Th}(D)$}}\label{s1}

\begin{prop}\label{p2.1}
In ${\rm Th}(D)$ the formulae $[x,y_1]=[y_2,y_3]$ has the tree property of the second kind.
\end{prop}

{\em Proof\/}. Since $D$ is the Fra\"{\i}ss\'e limit of ${\mathbb K}_{2,p}^P$ there is an embedding of an infinite free group of $G_{2,p}$ in $D$. Assume that $\{b_\alpha:\alpha<\omega\}\cup\{c_{\alpha,i},d_{\alpha,i}:\alpha<\omega, i<\omega\}$ are free generators of  such an infinite free subgroup. We consider the array
\[
 \ol{a}_{\alpha,i}=\{(b_{\alpha,i}, c_{\alpha,i},d_{\alpha,i}):\alpha<\omega, i<\omega\}
\]
where $b_{\alpha,i}=b_\alpha$ for all $\alpha$ and $i$:
\[
\mbox{Then }\; D\vDash\neg\exists x([x,b_\alpha]=[c_{\alpha,i},d_{\alpha,i}]\wedge[x,b_\alpha]  = [c_{\alpha,j},d_{\alpha,j}])
\]
for fixed $\alpha$ and $i\ne j$. Now let $f$ be any map of $\omega$ into $\omega$. Then the set
\[
 \{[x,b_\alpha]=[c_{\alpha,f(\alpha)},d_{\alpha,f(\alpha)}]:\alpha<\omega\}
\]
is consistent, since $D$ is a Fra\"{\i}ss\'e limit.\hfill$\Box$

\section{The amalgamation property for {\boldmath${\mathbb K}(n)$}}\label{s3}

Let $G$ be a group in ${\mathbb G}(n)$ with the elements $c_1^G,\ldots,c_n^G$ short $c_1,\ldots,c_n$. Let $P(G)$ be the subgroup generated by $c_1,\ldots,c_n$. In the language $L(n)$ \, $P(G)$ is the $L(n)$-substructure generated by the empty set. By definition $G'\subseteq P(G)\subseteq Z(G)$ and the linear dimension ${\rm ldim}(P(G))$ of $P(G)$ is $n$.
\medskip

In \cite{Bau} a functor $F$ from ${\mathbb G}_{2,p}^P$ into the category ${\mathbb B}^P$ of bilinear alternating maps $(V,W,\beta)$ is defined where $V$ and $W$ are ${\mathbb F}_p$-vector spaces and $\beta$ is a bilinear alternating map from $V$ into $W$. Morphisms of ${\mathbb B}^P$ from $(V_1,W_1,\beta_1)$ to $(V_2,W_2,\beta_2)$ consists of vector space embeddings $f:V_1$ into $V_2$ and $g:W_1$ into $W_2$ that commute with the bilinear maps $\beta_i$.
\[
\begin{xy}
\xymatrix{
V_1\ar[d]^{\textstyle f}&\times&V_1\ar[d]^{\textstyle f}\ar[r]^{\textstyle\beta_1} &W_1\ar[d]^{\textstyle g, }\\
V_2&\times&V_2 \ar[r]^{\textstyle\beta_2}&W_2
}
\end{xy}
\]
$F$ is defined in the following way: $F(G)$ is $(V,W,\beta)$ where $V=G/P(G)$, $W= P(G)$ and $\beta$ is induced by $[\;,\;]$. If $f: G\to H$ then $F(f)=(\ol{f}, f\restriction P)$ where $\ol{f}:G/P(G)\to H/P(H)$ is induced by $f$.
$F$ is a bijection on the level of objects up to isomorphisms.
\medskip

If we consider the category ${\mathbb G}(n)$, then the morphisms $f:G\to H$ send $c_i^G$ to $c_i^H$. Hence $f$ induces an isomorphism of $P(G)$ onto $P(H)$. We call ${\mathbb B}(n)$ the corresponding category of bilinear alternating maps $(V,P,\beta)$ where $P=\langle c_1,\ldots,c_n\rangle$ is fixed. The morphisms have the form $(g,{\rm id})$. We define the functor $F$ from ${\mathbb G}(n)$ to ${\mathbb B}(n)$ as above and obtain as in \cite{Bau2}:

\begin{lemma}\label{l3.1}
\begin{enumerate}
 \item[{\rm i)}] $F$ is a functor of ${\mathbb G}(n)$ onto ${\mathbb B}(n)$ that is a bijection for the objects of the categories up to isomorphisms.

\item[{\rm ii}] If $G_0 \in {\mathbb G}(n)$ and $(g,id)$ is ann embedding of $F(G_0)$ into some $(V,P,\beta)$, then there are some $G \in {\mathbb G}(n)$ and some embedding $f$ of $G_0$ into $G$, such that $F(G) = (V,P, \beta)$ and $F(f) = (g,id)$.

\item[{\rm iii)}] In ${\mathbb G}(n)$ we consider $e_0:G_0\to G$, $e_1:H_0\to H$ where $f_0$ is an isomorphism of $G_0$ onto $H_0$. In ${\mathbb B}(n)$ we assume that there is $g$ such that
\[
\begin{xy}
\xymatrix{
F(G_0)\ar[d]^{F(f_0)}\ar[r]^{F(e_0)} &F(G)\ar[d]^{(g,{\rm id})}\\
F(H_0) \ar[r]^{F(e_1)}&F(H)\;\;.
}
\end{xy}
\]
\end{enumerate}
Then there is an embedding $f$ of $G$ into $H$ such that $F(f)=(g,{\rm id})$ and
\[
\begin{xy}
\xymatrix{
G_0\ar[d]^{f_0}\ar[r]^{e_0} &G\ar[d]^{f}\\
H_0 \ar[r]^{e_1}&H\;\;.
}
\end{xy}
\]
\end{lemma}

Lemma~\ref{l3.1} shows that AP for ${\mathbb B}(n)$ implies AP for ${\mathbb G}(n)$ as in \cite{Bau}. To show AP for ${\mathbb B}(n)$ we cannot use the free amalgam as in \cite{Bau}.
\smallskip

Assume
\begin{eqnarray*}
(f_A,{\rm id}):&&(V_B,P,\beta_B)\longrightarrow(V_A,P,\beta_A),\\
(f_C,{\rm id}):&&(V_B,P,\beta_B)\longrightarrow(V_C,P,\beta_C).
\end{eqnarray*}
W.l.o.g. $V_B$ is a common subspace of $V_A$ and $V_C$. Let $V_D$ be the vector space amalgam
$V_C\bigoplus\limits_{V_B} V_A$  with respect to $f_A$ and $f_C$. We get the desired amalgam $\langle V_D,P,\beta_D\rangle$ if
\[
\beta_D=\beta_A\;\mbox{ on }\; V_A \quad\mbox{ and } \quad \beta_D=\beta_C\;\mbox{ on }\;V_C
\]
and the rest is obtained in the following way:
If $X$ is a basis of $V_A$ over $V_B$ and $Y$ is a basis of $V_C$ over $V_B$ then we can choose for each pair $x\in X$ and $y\in Y$ \, $\beta_0(x,y)$ in $P$ as we want.
\medskip

In our context AP implies JEP.

\begin{theorem}\label{t3.1}
${\mathbb K}(n)$ has HP, JEP and AP. Hence the Fra\"{\i}ss\'e limit $D(n)$ exists. It is $\aleph_0$-categorical. ${\rm Th}(D(n))$ has the elimination of quantifiers.
\end{theorem}
The theorem uses the known theory. See \cite{Ho}. Uniform local finiteness and finite signature for ${\mathbb K}(n)$ imply $\aleph_0$-categoricity and elimination of quantifiers. ${\rm Th}(D(n))$ can be axiomatized by the following sentences: Let $M$ be a model of ${\rm Th}(D(n))$.
\begin{enumerate}
 \item[$\Sigma\,1)$] $M$ is a nilpotent group of class 2 with exponent $p$.
\item[$\Sigma\,2)$] $M'=Z(M)=\langle c_1,\ldots,c_n\rangle$ is of linear dimension $n$.
\item[$\Sigma\,3)$] For $B\subseteq A$ in ${\mathbb K}(n)$ it holds: If $B'\subseteq M$ and $B'\cong B$, then this embedding of $B$ into $M$ can be extended to $A$.
\end{enumerate}

In the case $n=1$ these axioms imply that $M$ is infinite and $M'=Z(M)$ is cyclic.
By U.~Felgner \cite{Fe} $D(1)$ is the extra special $p$-group, since his axiomatization is $\Sigma\,1)$ $M'=Z(M)$ is cyclic and infiniteness.
\bigskip

{\bf Question} \, Is there an easier axiomatization of ${\rm Th}(D(n))$ for $n\ge 2$?

\section{Independence property in {\boldmath${\mathbb G}(n)$}}\label{s4}

Assume $M\vDash {\rm Th}(D(1))$ and $M$ is countable. We write $c$ instead of $c_1$. By \cite{Fe} $M$ is a central product over $\langle c\rangle$:
\[
 M=\bigodot\limits_{\stackrel{\scriptstyle\langle c\rangle}{i<\omega}}\langle c,a_ib_i\rangle
\]
where $c$ is a generator of the cyclic subgroup $M'=Z(M)$ and $[b_i,a_i]=c$.
\smallskip

By the elimination of quantifiers of ${\rm Th}(D(1))$ \, $a_0\hat{\;}b_0,a_1\hat{\;}b_1\ldots,a_n\hat{\;}b_n,\ldots$ is an indiscernible sequence in $M$. Then
$a_1\hat{\;}b_1,a_2\hat{\;}(b_2\circ b_0),a_3\hat{\;}b_3,a_4\hat{\;}(b_4\circ b_0),\ldots$ and $b_1,b_2\circ b_0,b_3,b_4\circ b_0,\ldots$ are indiscernible sequences in $M$.
We have $M\vDash[b_{2i+1},a_0]=1$ for $i<\omega$ and $M\vDash[b_{2i}\circ b_0,a_0]=c$ for $i\le i<\omega$.
\medskip

We have shown  (see \cite{A}):

\begin{lemma}\label{l4.1}
The formula $[y,x]=1$ has the independence property in ${\rm Th}(D(1))$.
\end{lemma}

Let $G$ be in ${\mathbb G}(n)$ with $G/Z(G)$ is infinite. For $a\in G\setminus Z(G)$ choose a maximal linearly independent subset $\{e_1,\ldots,e_m\}=X_a$ of $P(G)$ such that for every $1\le i\le m\le n$ there is some $b_i\in G$ with $[a,b_i]=e_i$. Let $E_a$ be $\{b_1,\ldots,b_m\}$. If $[a,b]=t\ne 1\in P(G)$, then $t=\sum\limits_{1\le i\le m} e_i^{r_i}$ and $[a,b\cdot b_1^{p-r_1}\cdot\ldots\cdot b_m^{p-r_m}]=1$. Hence every element $a\in G$ has a centralizer $C(a)$ of index $\le n$ and $G=\langle a,E_a\rangle\circ C(a)$.
\medskip

Now we start again with $d_0\in G\setminus Z(G)$. Then $X_{d_0}\ne \emptyset$ and $E_0=E_{d_0}\ne\emptyset$ and we choose $e_0\in E_0$ with $[d_0,e_0]\ne 1$.
Since $C(\langle d_0,E_0\rangle)$ has finite index in $G$ there is some
\[
 d_1\in C(\langle d_0,E_0\rangle)\quad\mbox{ with }\; d_1\not\in Z(G).
\]
We get $E_1=E_{d_1}\ne\emptyset$ and choose $b_1\in E_1$.
We can repeat this argument and get
\[
 d_2\in C(\langle d_0,e_0,E_0,E_1\rangle), \quad d_2\not\in Z(G).
\]
Finally we have $d_0,e_0, d_1,e_1,\ldots$ with $[d_i,e_i]\ne 1$ and $[d_i,d_j]=1$, $[d_i,e_j]=1$ and $[e_i,e_j]=1$ for $i\ne j$.
We can select a subsequence with $[d_i,e_i]=c\ne 1$ for some $c\in P(G)$. Assume w.l.o.g. $[d_i,e_i]=c$ for all $i<\omega$. We have shown that $D(1)$ is a subgroup of $G$. Since the independence property of $D(1)$ is given by a quantifier formula we get

\begin{theorem}\label{t4.2}
For every $G\in{\mathbb G}(n)$ with $G/Z(G)$ infinite we have:
\begin{enumerate}
 \item[{\rm i)}] There is an embedding of $D(1)$ in $G$.
\item[{\rm ii)}] $G$ has the independence property.
\end{enumerate}
\end{theorem}

\begin{corollary}\label{c4.3}
The Fra\"{\i}ss\'e limits $D(n)$ of ${\mathbb K}(n)$ have the independence property.
\end{corollary}

\section{Superstability of {\boldmath$Th(D(n))$}}\label{s5}

Let ${\mathbb C}(n)$ be a monster model of $Th(D(n))$. We define
\[
A\ind\limits_B{}\!\!^0 C, \mbox{ if }\;  \langle A\rangle\cap\langle C\rangle=\langle B\rangle.
\]
Note that all substructures as $\langle A\rangle$ contain $P({\mathbb C}(n))$.
\smallskip

We have to check that $\ind^0$ fulfils the conditions of B.~Kim and A.~Pillay \cite{KP} that characterize Non-forking. Working in the vector space ${\mathbb C}(n)/P({\mathbb C}(n))$ Monotonicity, Transitivity, Symmetry, Finite Character, and Local Character are easily shown.
\medskip

{\bf Existence:} $\ol{a},B\subseteq A$ are considered in ${\mathbb C}(n)$. Then there is some $\ol{d}$ in ${\mathbb C}(n)$ with ${\rm tp}(\ol{a}/B)={\rm tp}(\ol{d}/B)$ and $\ol{d}\ind\limits_B{}\!\!^0A$.
\medskip

W.l.o.g. $B$ and $A$ are $L(n)$-substructures. Since $P\subseteq B$ we can assume that $\ol{a}$ is linearly independent over $B$. Choose $X_B$ and $X_A$ such that the images of $X_B$ and $X_BX_A$ are vector space bases of $B/P$ and $A/P$, respectively.
Let $\beta((X_BX_A)^2)$ be the set of all $\beta(b_1,b_2)=[b_1,b_2]$ where $b_1,b_2\in X_BX_A$. Then $A$ is uniquely determined by $X_BX_A$ and $\beta((X_BX_A)^2)$.
\smallskip

Now we define an extension $G$ of $A$. Let $\ol{e}$ linearly independent over $A$. $\ol{e}X_BX_A$ is linearly independent over $P$. $\beta((\ol{e}\,\hat{\;}X_BX_A)^2)$ is chosen as any extension of $\beta((X_BX_A)^2)$ and $\beta((\ol{e}X_B)^2)$, where the last set is obtained from $\beta((\ol{a}X_B)^2)$ by replacing $a_i$ in $\ol{a}$ by $e_i$ in $\ol{e}$.  $G=\langle\ol{e}A\rangle$ is a structure in ${\mathbb K}(n)$. By the axioms $\Sigma\,3)$ of ${\rm Th}(D(n))$ there is an embedding of $\ol{e}$ onto $\ol{d}$ over $A$ in ${\mathbb C}(n)$ . By quantifier elimination ${\rm tp}(\ol{d}/B)={\rm tp}(\ol{a}/B)$. Furthermore $\ol{d}\ind\limits_B{}\!\!^0A$ by construction.
\medskip

Finally we have to show:

\subsubsection*{Independence over Models}

Let $M\preceq {\mathbb C}(n)$, ${\rm tp}(\ol{a}{}^0/M)={\rm tp}(\ol{a} {}^1/M)$
\[
\ol{b}{}^0\ind\limits_M{}\!\!^0\;\ol{b}{}^1,\qquad \ol{a}{}^0\ind\limits_M{}\!\!^0\;\ol{b}{}^0,\qquad
\ol{a}{}^1\ind\limits_M{}\!\!^0\;\ol{b}{}^1.
\]
Then there is some $\ol{e}$ with
\[
 {\rm tp}(\ol{e}/M\ol{b}{}^0)={\rm tp}(\ol{a}_0/M\ol{b}{}^0),\qquad {\rm tp}(\ol{e}/M\ol{b}{}^1)={\rm tp}(\ol{a}_1/M\ol{b}{}^1),
\]
and
\[
 \ol{e}\ind\limits_M{}\!\!^0\;\ol{b}{}^0\ol{b}{}^1.
\]
Let $X_M$ be a set in $M$ such that its image is a vector space basis of $M/P$. By assumption we can assume that w.l.o.g.  $\ol{b}{}^0\ol{b}{}^1$ is linearly independent over $M$ modulo~$P$. We choose $\ol{d}$ linearly independent over $\ol{b}{}^0\ol{b}{}^1X_M$ modulo~$P$. Now we extend $\langle \ol{b}{}^0,\ol{b}{}^1,X_M\rangle$ to a group $G$ in ${\mathbb G}(n)$ defined on $\ol{d}\,\ol{b}{}^0\ol{b}{}^1X_M$. We extend $\beta((\ol{b}{}^0\ol{b}{}^1X_M)^2)$ to $\beta((\ol{d}\,\ol{b}{}^0\ol{b}{}^1X_M)^2)$ by the following:
\begin{eqnarray*}
\beta(d_i,m)&&\mbox{for }\:d_i\in\ol{d}\;\mbox{ and }\; m\in X_M\;\mbox{ is given by }\;\beta(a_i^0,m)=\beta(a_i^1,m),\\
\beta(d_i,b_j^0)&&\mbox{is given by }\;\beta(a_i^0,b_j^0), \mbox{ and}\\
\beta(d_i,b_j^1)&&\mbox{is given by }\; \beta(a_i^1,b_j^1).
\end{eqnarray*}
Now we find an image $\ol{e}$ of $\ol{d}$ in ${\mathbb C}(n)$ over $\langle\ol{b}{}^0,\ol{b}{}^1,M\rangle$ by axioms $\Sigma\,3)$ that defines an embedding. By elimination of quantifiers and the consltruction $\ol{e}$ has the desired properties.

\begin {theorem}\label{t5.1}
$\ind^0$ is non-forking for $D(n)$. $D(n)$ is supersimple of SU-rank $1$. It is not stable.
\end {theorem}

{\em Proof\/}. As shown above $\ind^0$ is non-forking and $D(n)$ is simple. Any type ${\rm tp}(\ol{a}/A)$ does not fork on a finite subset of $A$. By the description of non-forking we have SU-rank 1. In Chapter~4 it is shown that $D(n)$ has the independence property.

config: arxiv


TITLE: Generate roof from a 2D polygon
QUESTION [1 upvotes]: Let's say we have a 2D Polygon ( it can be concaved or convex), and on top of this polygon we are required to build a house roof. What is the algorithm that one can use for this?
The conditions:

The roof cannot be $0^o$ or $90^o$.
The created roof piece must be as smooth as possible ( smooth is defined as first order differentiable), meaning the slope of the roof must not change unnecessarily.

I'm sorry if the conditions sound vague. If you get lost, just think about this: you have a house, how do you generate the roof profile?
Note: The roof plan must be uniformly sloping, so no circle, or bump can be used.

REPLY [3 votes]: Here is an image I happen to have prepared for a book.  It shows the medial-axis polyhedron over a convex polygon, which coincides with the straight skeleton as in lhf's answer, and also with the offset-procedure in alQpr's answer. Sides slope at $45^\circ$.


TITLE: Contradiction between me and my professor solution in normal app. to binomial
QUESTION [1 upvotes]: %$20$ of people smoke , if we choose a sample space consisting of $225$ people , what is the probability that more than $40$ people are smokers

This is an probability question given by my professor.As you see ,it can be solved by normal approximation to binomial distribution.However , there is problem here. The problem is the limits of z value. Me and my professor have different solutions , i want you guys decide which of us is right..
My professors'approach: If it is wanted more than $40$ , then find $P(x=41)+P(x=42)+...+P(x=225)$ , so make use of normal approach such that $P(X >39.5)$
My approach : If it is wanted more than $40$ , then find $P(x=41)+P(x=42)+...+P(x=225)$ , so make use of normal approach such that $P(X >40.5)$
The rest is classical solution and not our problem here.. I thought that it must be $P(X >40.5)$ instead of $P(X >39.5)$ , because $P(X >39.5)$ include the probability of $P(x=40)$.However , he continues to solve other problems in this way. For example , another binomial question asked for $P(10<x<18)$ and he solved it such that $P(9.5<x<18.5)$ , but i think that because of it is binomial ,i.e discrete, it must be $P(11 \leq x \leq 17)$ ,so $P(10.5<X<17.5)$
When you look at these $2$ example , which of us right ? Thanks in advance..
NOTE = He gives this course in many years  , if i am missing something please explain clearly

REPLY [1 votes]: When using continuity correction (see the link below) when estimating $P(X \leq 40)$ where $X\sim \text{Binomial}(n,p)$ , you use the probability $P(Y \leq 40.5)$ where $Y \sim N(np,\sqrt{np(1-p)})$. Hence for estimating $P(X > 40)$ you would naturally have to use $P(Y>40.5)$. So this would mean your approach is correct.
However, your professor might be taking into account that for certain values of $p$ and $n$, the Normal approximation underestimates the Binomial distribution and hence choosing to correct for this by looking at $P(X > 39.5)$ instead. I am not an expert on this topic so I won't comment on whether or not this is reasonable or not. I just wanted to point out that this could be an explanation.
As a final remark, note that $P(X > 39.5) \approx P(X > 40.5)$ as long as $np$ is not too close to 40. Hence in a some situations it does not matter which approach you use (as you are using approximations anyway).

Sources:
Continuity correction: https://en.wikipedia.org/wiki/Continuity_correction

Edit: It just occured to me that your professor might intepret it as greater or equal to 40 in which case the probability of interest is $P(X \geq 40)=P(X>39)$. Then you would both agree and pick $39.5$.


TITLE: Dividing Cuboid into Equal Cubes
QUESTION [0 upvotes]: What is the formula to divide a large cuboid into equal cubes given a starting Length, Width, Height and known quantity of cubes so that the combined volume of the cubes equals the total volume of the cuboid?
For instance, if I had a cuboid that was 24.4in X 11.6in X 8in and wanted to get 500 smaller cubes of the exact same size.
When I tried to guess at the formula, I divided each side by 500, to get 0.0488, 0.0232, 0.0160 L,W,H respectively. The volume of this cube is 0.000018 inches$^3$ while the volume of the cuboid is 2264.32 inches$^3$. Then if I multiply $0.000018*500$ I only get 0.009 which doesn't match 2264.32.
What am I missing?

REPLY [0 votes]: When you divide the length by $m$, the width by $n$, and the height by $p$ you get $mnp$ little cuboids.  If you want to divide the large one into $500$ you need to find three numbers whose product is $500$.  One choice would be $4,5,25$ so you could make the length $\frac {24.4}{25}=0.976$ and compute the others the same way.  The small pieces will not be cubical, but they will be cuboids.


TITLE: Show that $X-Y\mid X \sim \exp(\lambda)$
QUESTION [0 upvotes]: I'm clueless with this one:
Let $X$ and $Y$ be the minimum and the maximum of two independent exponentially distributed random variables with parameter $\lambda>0$. Show that $Y-X\mid X \sim \exp(\lambda)$.
I will appreciate any hint.

REPLY [1 votes]: Let the original variables be $X_1$ and $X_2$. Then
\begin{eqnarray*}
P(Y-X\gt a\mid X=x)
&=&
P(X_1-X_2\gt a\mid X_2=x,X_1\ge X_2)\quad\quad\;\text{(by symmetry)}
\\
&=&
P(X_1-x\gt a\mid X_1\ge x)\\
&=&
P(X_1\gt x+a\mid X_1\ge x)\\
&=&
P(X_1\gt a)\;.\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\text{(by memorylessness)}
\end{eqnarray*}
Thus $Y-X\mid X$ is distributed as $X_1$, and thus $\sim\exp(\lambda)$.


text:
{\bf Problem.} The graph of the rational function $\frac{p(x)}{q(x)}$ is shown below, with a horizontal asymptote of $y = 0$ and a vertical asymptote of $ x=-1 $. If $q(x)$ is quadratic, $p(2)=1$, and $q(2) = 3$, find $p(x) + q(x).$
[asy]
size(8cm);
import graph;

Label f;
f.p=fontsize(6);

real f(real x) {return (x-1)/((x-1)*(x+1));}

int gridsize = 5;
draw((-gridsize,0)--(gridsize,0), black+1bp, Arrows(8));
draw((0,-gridsize)--(0, gridsize), black+1bp, Arrows(8));
label("$x$", (gridsize, 0), E);
label("$y$", (0, gridsize), N);
label("$0$", (0,0),SE, p=fontsize(8pt));
for (int i=-gridsize+1; i<0; ++i){
    label("$"+string(i)+"$",(i,0),S, p=fontsize(8pt));
    label("$"+string(i)+"$",(0,i),E, p=fontsize(8pt));}
for (int i=1; i<=gridsize-1; ++i){
    label("$"+string(i)+"$",(i,0),S, p=fontsize(8pt));
    label("$"+string(i)+"$",(0,i),E, p=fontsize(8pt));}

draw(graph(f,-5,-1.2));
draw(graph(f,-.8,0.85));
draw(graph(f,1.15,5));
draw((-1,-5)--(-1,5), dashed);
draw(circle((1,.5),.15));

[/asy]
{\bf Level.} Level 5
{\bf Type.} Intermediate Algebra
{\bf Solution.} Since $q(x)$ is a quadratic, and we have a horizontal asymptote at $y=0,$ we know that $p(x)$ must be linear.

Since we have a hole at $x=1,$ there must be a factor of $x-1$ in both $p(x)$ and $q(x).$ Additionally, since there is a vertical asymptote at $x=-1,$ the denominator $q(x)$ must have a factor of $x+1.$ Then, $p(x) = a(x-1)$ and $q(x) = b(x+1)(x-1),$ for some constants $a$ and $b.$

Since $p(2) = 1$, we have $a(2-1) = 1$ and hence $a=1$. Since $q(2) = 3$, we have $b(2+1)(2-1) = 3$ and hence $b=1$.

So $p(x) = x - 1$ and $q(x) = (x + 1)(x - 1) = x^2 - 1,$ so $p(x) + q(x) = \boxed{x^2 + x - 2}.$

set_name: MATH


text:
Here we compare the behavior of the stochastic model described in Section~\ref{sec:stoch} to that of the limiting system of conservation laws~\eqref{PDEs}.
We do so by comparing direct numerical simulation of the stochastic model with a finite-difference scheme for~\eqref{PDEs} given by the mesoscopic model in~\eqref{rhoA2}.

\subsection{Simulations with Uniform Initial Density}
\label{sec:numsumu}

In the first set of simulations, we consider uniform initial densities on non-overlapping squares. In particular,
we consider two groups of agents moving toward each other on a $200 \times 200$ lattice with
initial conditions for the two groups given by
\[
	\sigma^A_{j,k} = \begin{cases} 1, & 81 \leq j \leq 100 \text{ and } 81 \leq k \leq 100,\\
				0, & \text{otherwise}, \end{cases}
\]
\[
	\sigma^B_{j,k} = \begin{cases} 1, & 101 \leq j \leq 120 \text{ and } 101 \leq k \leq 120,\\
				0, & \text{otherwise}. \end{cases}
\]
We take the velocity potentials to be
\[
	\psi^A(j,k) = (180 - j)^2 + (180 - k)^2 {\rm ~~and~~}
	\psi^B(j,k) = (21 - j)^2 + (21 - k)^2.
\]
Computing the gradients of these potentials and then normalizing in $\ell^{1}$ yields the floor velocity fields for the two groups of agents:
\begin{align*}
	\phi^A(j,k) &= \left( \frac{180 - j}{|180 - j| + |180 - k|},  \frac{180 - k}{|180 - j| + |180 - k|}\right),
\\
	\phi^B(j,k) &= \left( \frac{21 - j}{|21 - j| + |21 - k|},  \frac{21 - k}{|21 - j| + |21 - k|}\right).
\end{align*}
Group $A$ moves toward the point $(180,180)$, while the target point for group $B$ is $(21,21)$.
Consequently, the two groups pass through each other in order to reach their corresponding target points.
We set the velocity scaling parameter $c_0 = 1$ and consider two cases of differing slowdown interaction strengths: $\alpha = 2,4$ in~\eqref{vel}.

We simulate the microscopic model with timestep $\Delta t =.05$ and average over 1000 simulations to obtain a Monte Carlo approximation for the evolution of the group densities, $\rho^A$ and $\rho^B$.
We then compare these results to those produced by numerically solving the mesoscopic model using a Runge-Kutta fourth-order method with variable timestep.
A comparison of the evolutions of $\rho^A$ and $\rho^B$ for the microscopic and mesoscopic models is depicted in Figures~\ref{fig1alpha2},\ref{fig3alpha2} and Figures~\ref{fig1alpha4},\ref{fig3alpha4} for $\alpha=2$ and $\alpha=4$, respectively.
Two-dimensional density plots are presented in Figures \ref{fig1alpha2} and \ref{fig1alpha4}.
To examine the fine details of the group interactions, we illustrate the evolution of the density $\rho^A$ along the diagonal $j = k$ in
Figures~\ref{fig3alpha2} and~\ref{fig3alpha4}.

In Figure~\ref{fig1alpha2}, the two groups almost completely overlap in space at time $t=35$.
At $t=105$, the groups still overlap significantly, but approximately 15\% of the agents from each group have passed through the complementary group.
The groups have nearly passed through one another at time $t=175$, and have completely done so by time $t=245$.
When assessing how well the deterministic model approximates the stochastic dynamics, times $t=175$ and $t=245$ provide the most demanding test.
Figures~\ref{fig1alpha2} and~\ref{fig3alpha2} demonstrate that the deterministic model is in excellent agreement with the results of the stochastic simulations.
At time $t=175$, the deterministic model accurately captures the effect of the slowdown mechanism, a mechanism that results in complex profiles for the densities of the moving agents.
Importantly, the deterministic model captures not only the overall shapes of the densities, but also the magnitudes of the peaks, as well as the leading and trailing fronts.

In the stronger slowdown interaction regime ($\alpha = 4$), the deterministic model once again accurately captures the behavior of the stochastic model, except for discrepancies in the trailing fronts (these fronts occur after the groups have passed through one another).
These results are depicted in Figures~\ref{fig1alpha4} and~\ref{fig3alpha4}.
Analyzing the simulations in detail, we note that due to the stronger slowdown interaction strength (i.e. $\alpha=4$ vs $\alpha=2$), it takes the two groups much longer to pass through one another.
This results in longer numerical simulations for both the deterministic and stochastic models.
Consequently, small discrepancies between the two have more time to grow when $\alpha=4$ than when $\alpha = 2$.
Nevertheless, we observe good agreement between the deterministic and stochastic models for times $t=50$, $150$, and $250$.
At time $t=150$, the positions of the peaks, as well as the leading and trailing fronts, are accurately captured by the deterministic model.

For $t=250$, the density of agents that have already passed through the other group is slightly higher in the deterministic case (see $110 \lessapprox k \lessapprox 170$ in the bottom left subplot of Figure~\ref{fig3alpha4}).
This small overestimation of the density by the deterministic model
accumulates over time (from $t=250$ to $t=350$), and results in the two groups passing through one another earlier (at $t \approx 320$ for the deterministic model versus $t=360$ for the stochastic model).
Consequently, the trailing fronts have slightly separated by time $t=350$ (bottom right subplot of Figure~\ref{fig3alpha4}).

Summarizing our results when the initial group densities are uniform, we find excellent quantitative agreement between the macroscopic system of conservation laws~\eqref{PDEs} and the microscopic stochastic model.
Even when the slowdown interactions are strong ($\alpha = 4$), we see excellent agreement modulo small differences between the group pass-through times and trailing fronts.

\begin{figure}[t]
\centering
\includegraphics[width=68mm]{./alpha2/stochCon35.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha2/odeCon35.pdf}\\
\includegraphics[width=68mm]{./alpha2/stochCon105.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha2/odeCon105.pdf}\\
\includegraphics[width=68mm]{./alpha2/stochCon175.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha2/odeCon175.pdf}\\
\includegraphics[width=68mm]{./alpha2/stochCon245.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha2/odeCon245.pdf}
\caption{Two group densities, initially distributed uniformly over disjoint squares, pass through one another under mild slowdown interaction strength.
A finite-difference simulation of the macroscopic PDEs~\eqref{PDEs} (right column) closely matches an average of 1000 realizations of the microscopic stochastic model (left column).
Slowdown strength: $\alpha=2$.
Times: 35, 105, 175, 245.}
\label{fig1alpha2}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=70mm]{./alpha2/compLinea35.pdf}
\hspace{0.5em}
\includegraphics[width=70mm]{./alpha2/compLinea105.pdf}\\
\vspace{1ex}
\includegraphics[width=70mm]{./alpha2/compLinea175.pdf}
\hspace{0.5em}
\includegraphics[width=70mm]{./alpha2/compLinea245.pdf}
\caption{Evolution of group A density along the diagonal $j=k$ of the lattice.
Setup is as in Figure~\ref{fig1alpha2}.
Blue: Macroscopic model~\eqref{PDEs}.
Red: Microscopic stochastic model.
Slowdown strength: $\alpha=2$.
Times (left to right): 35, 105, 175, 245.}
\label{fig3alpha2}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=68mm]{./alpha4/stochCon50.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha4/odeCon50.pdf}\\
\includegraphics[width=68mm]{./alpha4/stochCon150.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha4/odeCon150.pdf}\\
\includegraphics[width=68mm]{./alpha4/stochCon250.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha4/odeCon250.pdf}\\
\includegraphics[width=68mm]{./alpha4/stochCon350.pdf}
\hspace{1em}
\includegraphics[width=68mm]{./alpha4/odeCon350.pdf}
\caption{Two group densities, initially distributed uniformly over disjoint squares, pass through one another under strong slowdown interaction strength.
The macroscopic model~\eqref{PDEs} (right column) quantitatively agrees with the microscopic stochastic model (left column), except for differences in the trailing fronts at $t=350$.
Slowdown strength: $\alpha=4$.
Times: 50, 150, 250, 350.}
\label{fig1alpha4}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=70mm]{./alpha4/compLinea50.pdf}
\hspace{0.5em}
\includegraphics[width=70mm]{./alpha4/compLinea150.pdf}\\
\vspace{1ex}
\includegraphics[width=70mm]{./alpha4/compLinea250.pdf}
\hspace{0.5em}
\includegraphics[width=70mm]{./alpha4/compLinea350.pdf}
\caption{Evolution of group A density along the diagonal $j=k$ of the lattice.
Setup is as in Figure~\ref{fig1alpha4}.
Blue: Macroscopic model~\eqref{PDEs}.
Red: Microscopic stochastic model.
Slowdown strength: $\alpha=4$.
Times (left to right): 50, 150, 250, 350.}
\label{fig3alpha4}
\end{figure}

\subsection{Simulations with Non-Uniform Initial Density}
\label{sec:numsumnonu}

In the second set of simulations, we analyze the performance of the macroscopic model when the initial agent densities vary in space.
The stochastic model is more diffusive by nature than our derived deterministic models that approximate it.
We believe that conservation law system~\eqref{PDEs} can produce and propagate sharp gradients in the solution, while such sharp gradients are typically `smoothed out' rather quickly in stochastic simulations.
Further, as pointed out in~\cite{ckpt14,goatin}, conservation laws which are conditionally hyperbolic can potentially
develop high-frequency, non-physical oscillations in the non-hyperbolic regime.
Therefore, this set of simulations is designed to test how well the macroscopic model performs in the non-hyperbolic regime with large initial gradients.

We consider a $100 \times 100$ lattice $\mathcal{L}$ and initial conditions for the deterministic model given by
\begin{equation}
	\rho^A_{j,k,0} = \begin{cases} \frac{1}{4}\left\lceil 2\left(1+\cos{\left(\frac{4\pi}{19}(j+k-62)\right)}\right)\right\rceil, & 31 \leq j \leq 50 \text{ and } 31 \leq k \leq 50,\\
			0, & \text{otherwise}, \end{cases}
\end{equation}
and
\begin{equation}
	\rho^B_{j,k,0} = \begin{cases} \frac{1}{4}\left\lceil 2\left(1+\cos{\left(\frac{4\pi}{19}(j+k-102)\right)}\right)\right\rceil, & 51 \leq j \leq 70 \text{ and } 51 \leq k \leq 70,\\
				0, & \text{otherwise}. \end{cases}
\end{equation}

To replicate this initial configuration in the stochastic model, we average over 20000 realizations,
where we sample $1$ in each lattice cell with probabilities given by the expressions above.
Therefore, the expected value of the solution at time zero in stochastic simulations
is given by the expressions above.

We specify floor velocity fields for the two groups using the potential functions
$\psi^A(j,k)$ and $\psi^B(j,k)$ on $\mathcal{L}$ defined by
\[
	\psi^A(j,k) = (80-j)^2 + (80-k)^{2}, \qquad
	\psi^B(j,k) = (21-j)^2 + (21-k)^{2},
\]
respectively. We obtain the floor velocity fields by computing the $\ell^{1}$-normalized gradients of the potentials:
\[
	\phi^A(j,k) =
\left( \frac{80 - j}{|80 - j| + |80 - k|},  \frac{80 - k}{|80 - j| + |80 - k|}\right)
\]
and
\[
	\phi^B(j,k) =
\left(\frac{21 - j}{|21 - j| + |21 - k|},  \frac{21 - k}{|21 - j| + |21 - k|}\right).
\]
Under these floor fields, agents from group $A$ move toward the point $(80,80)$, while agents from group $B$ move toward $(21,21)$.

Here we examine the mildly-strong slowdown interaction regime $\alpha = 2$ for the sake of brevity.
Since the two groups interact only for a short period of time in this regime, we expect the deterministic model to accurately capture the stochastic dynamics, and this does indeed happen.
That said, we will more closely examine how the nonuniformity in the initial data propagates forward.
We therefore concentrate on the early stages of the group-group interaction, as the system quickly loses memory of the initial nonuniformity.

We compare the behavior of the deterministic and stochastic systems in Figures~\ref{fig:levelf21},~\ref{fig:levelf22}, and~\ref{fig:levelf23}.
As with the first set of simulations, the two systems quantitatively agree over short time intervals (Figure~\ref{fig:levelf21}).
Figure~\ref{fig:levelf21} also illustrates that memory of the nonuniformity in the initial densities is quickly lost, with regions of high density and low density quickly equilibrating.
However, before the nonuniformity is lost due to equilibration, density fluctuations are sharper and persist longer in the deterministic case (Figures~\ref{fig:levelf22} and~\ref{fig:levelf23}).
This indicates that the stochastic model is more diffusive than the macroscopic conservation law approximation, as was also the case in~\cite{ckpt14}.
We will address this problem in Section~\ref{sec:diff} by deriving a diffusive correction to~\eqref{PDEs}.

\begin{figure}[t]
\centering
\includegraphics[width=2.5in]{./level/stochCon4.pdf}
\hspace{1em}
\includegraphics[width=2.5in]{./level/odeCon4.pdf}\\
\includegraphics[width=2.5in]{./level/stochCon8.pdf}
\hspace{1em}
\includegraphics[width=2.5in]{./level/odeCon8.pdf}\\
\includegraphics[width=2.5in]{./level/stochCon12.pdf}
\hspace{1em}
\includegraphics[width=2.5in]{./level/odeCon12.pdf}\\
\includegraphics[width=2.5in]{./level/stochCon16.pdf}
\hspace{1em}
\includegraphics[width=2.5in]{./level/odeCon16.pdf}
\caption{Two group densities, initially distributed {\itshape nonuniformly} over disjoint squares, pass through one another under mild slowdown interaction strength.
We observe excellent agreement between the microscopic stochastic model (left column) and the approximating conservation laws~\eqref{PDEs} (right column).
Initial nonuniformity in the densities is quickly lost.
Slowdown strength: $\alpha = 2$.
Times: $4,8,12,16$ (top to bottom).}
\label{fig:levelf21}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=2.5in]{./leveld/compLinea4.pdf}
\hspace{0.5em}
\includegraphics[width=2.5in]{./leveld/compLinea8.pdf}\\
\vspace{1ex}
\includegraphics[width=2.5in]{./leveld/compLinea12.pdf}
\hspace{0.5em}
\includegraphics[width=2.5in]{./leveld/compLinea16.pdf}
\caption{Time evolution of the diagonal of the group A density, $\rho^A_{j,j,t}$, for the simulation illustrated in Figure~\ref{fig:levelf21}.
Density fluctuations are sharper and persist longer for the approximating conservation laws~\eqref{PDEs} (blue curves) than for the microscopic stochastic dynamics (red curves).
Times: $4,8,12,16$ (left to right).}
\label{fig:levelf22}
\end{figure}

\begin{figure}[t]
\centering
\includegraphics[width=2.5in]{./heat/stochHeatZoom.pdf}
\hspace{1em}
\includegraphics[width=2.5in]{./heat/odeHeatZoom.pdf}
\caption{Time evolution (top to bottom) of the diagonal of the group A density, $\rho^A_{j,j,t}$, for the simulation illustrated in Figure~\ref{fig:levelf21}.
Density fluctuations are sharper and persist longer for the approximating conservation laws~\eqref{PDEs} (right column) than for the microscopic stochastic dynamics (left column).}
\label{fig:levelf23}
\end{figure}


text:
\section{Generalization Guarantees for Multi-pass SGD}
\label{sec:MultipassSGD}

One important implication of our stability bounds
is that they provide non-trivial generalization error guarantees for multi-pass SGD on nonsmooth losses. Multi-pass SGD is one of the most extensively used settings of SGD in practice, where SGD is run for $K$ passes (epochs) over the dataset (namely, the number of iterations $T=K n$). To the best of our knowledge, aside from the dimension-dependent bounds based on uniform convergence \citep{ShwartzSSS10}, no generalization error guarantees are known for the multi-pass setting on general nonsmooth convex losses. Given our uniform stability upper bounds, we can prove the following generalization error guarantees for the multi-pass setting of sampling-with-replacement SGD. Analogous results can be obtained for fixed-permutation SGD \iffull. \else (using our stability bounds for the latter in Sec.~3 of the supplementary material).\fi

\begin{thm} \label{thm:gen_bds_replSGD}
Running Algorithm \ref{alg:repl_SGD} for $K$ passes (i.e., for $T=K n$ iterations) with constant stepsize $\eta_t=\eta>0$ yields the following generalization error guarantees:
$$ |\EE_{\A_{\sf rSGD}} [\generr(\A_{\sf rSGD})]| \leq 4L^2 \eta\left( \sqrt{Kn}  + K\right), $$

and there exists $c>0$, such that for any $0<\theta<1$, with probability~$\geq 1-\theta-\exp(-n/2)$,
$$ |\generr(\A_{\sf rSGD})|
\leq c ~\Bigg( L^2 \eta\left(\sqrt{K n}+ K \right) \log(n) \log(n/\theta) +LR\sqrt{\frac{\log(1/\theta)}{n}}~\Bigg). $$
\end{thm}

\begin{proof}

First, by the expectation guarantee on UAS given in Theorem~\iffull\ref{thm:UB_repl_SGD} \else \ref{thm:sharp_repl_SGD} \fi together with the fact that the losses are $L$-Lipschitz, it follows that Algorithm~\ref{alg:repl_SGD} (when run for $K$ passes with constant stepsize $\eta$) is $\gamma$-uniformly stable, where $\gamma = 4L^2\left(\eta \sqrt{Kn}  +\eta K\right)$. Then, by \cite[Thm.~2.2]{HardtRS16}, we have
$$ |\EE_{\A_{\sf rSGD}}[\generr(\A_{\sf rSGD})]| \leq \gamma. $$
For the high-probability bound, we combine the high-probability guarantee on UAS given in Theorem~\iffull\ref{thm:UB_repl_SGD} \else \ref{thm:sharp_repl_SGD} \fi with Theorem~\ref{thm:stab-to-gen} to get the claimed bound.

\end{proof}

These bounds on generalization error can be used to obtain excess risk bounds using the standard risk decomposition (see \eqref{eqn:risk_decomp}). In practical scenarios where one can certify small optimization error for multi-pass SGD, Thm.~\ref{thm:gen_bds_replSGD} can be used to readily estimate the excess risk. In Section~6.2 \iffull \else of the supplementary material \fi we provide worst-case analysis showing that multi-pass SGD is guaranteed to attain the optimal excess risk of $\approx LR/\sqrt n$ within $n$ passes (with appropriately chosen constant stepsize).


TITLE: Occlusion of light with very fast objects
QUESTION [0 upvotes]: Take this graphic:

On the left there is a light emitter, which can fire light on command, towards the right. There are also two receptors, A and B, both $1$ light second away from the emitter. receptor B is in the path of the light, and receptor A is not. receptor B also has a velocity of $0.9c$ to the right.
Imagine that at time $0$, light is emitted from the box marked emitter. (before that time no light was emitted) If I understand the speed of light correctly, it will contact receptor B after $1$ second, even though it is moving at $0.9c$ away from the emitter.
Now imagine this. At time $0.5$, you receptor A down so that it would come in contact with the path of the light. Would receptor A be hit by the light after $1$ second? If so, would that prevent receptor B from being hit by the light?

REPLY [0 votes]: Yes the light that is emitted from the emitter, would reach receptor "A" after a time period of 1 second, which means the distance that the light traveled is 299,792.458 km's.
However, during the time that the light has departed from the emitter, and is moving toward receptor "A", receptor "B" is rapidly moving off to the right. By the time that the light reaches the receptor "A" position, receptor "B" has already traveled 269,813.212 km's away from that position, and there will be even  further movement off to the right before the light reaches this receptor "B".
Overall, if receptor "A" was left in its original position and thus does not block the line of sight leading to receptor "B", the light would reach receptor "B" after 4.359 seconds. Thus receptor "B" has traveled  (269,813.212 km's * 4.359) = 1,176,088.526 km's during this time period.
Now if the emitter and receptor "B" were mounted on a common frame, here too we would measure a time period of 1 second for the light to move across this 299,792.458 km's distance between the emitter and the receptor. If we then accelerated this common frame up to 0.9c off to the right, external viewers, who have not accelerated, would see that it takes 4.359 seconds for the light to leave the emitter and reach the receptor.
However, due to time dilation, clocks on board the moving frame would only measure 1.9 seconds ( 4.359 sec * 0.436 ). But it also is to be noted that a clock located at receptor "B" would be lagging behind a clock  located the emitter, by 0.9 of a second. Thus if it was agreed that the light would be emitted from the emitter at t=0 sec, the clock located at receptor "B" would therefore indicate t=1 sec ( 1.9 sec - 0.9 sec = 1 sec ) when the light finally reaches this receptor end.
Thus from the moving frames point of view, they will still measure the speed of the light as being 299,792.458 km/s. Yes, due to length contraction, the length of the frame has contracted from 299,792.458 km's, to 130,676.503 km's, but for those on board the moving frame, they are totally unaware of this contraction and thus to them the frame is still 299,792.458 km's long.
Thus 299,792.458 km's * 1 sec = the speed of light.


TITLE: Which of the statements is/are TRUE?
QUESTION [1 upvotes]: Let $K = \big [k_{i,j} \big ]_{i,j = 1}^{\infty}$ be an infinite matrix over $\Bbb C$ (the set of all complex numbers) such that
$(\text {i})$ for each $i \in \Bbb N$ (the set of all natural numbers), the $i^{\text {th}}$ row $(k_{i,1},k_{i,2}, \cdots )$ of $K$ is in $\ell^{\infty}$ and
$(\text {ii})$ for every $x = (x_1,x_2, \cdots) \in \ell^{1},$ $\sum\limits_{j = 1}^{\infty} k_{i,j}\ x_j$ is summable for all $i \in \Bbb N,$ and $(y_1,y_2, \cdots ) \in \ell^{1}$ where $y_i = \sum\limits_{j = 1}^{\infty} k_{i,j}\ x_j.$
Let the set of all rows of $K$ be denoted by $E.$ Consider the following statements $:$
$\text {P}\ :\ $ $E$ is a bounded set in $\ell^{\infty}.$
$\text {Q}\ :\ $ $E$ is a dense set in $\ell^{\infty}.$
$$\begin{align*} \left (\ell^{1}  = \left \{ \left (x_1,x_2, \cdots \right )\ :\ x_i \in \Bbb C, \sum\limits_{i=1}^{\infty} \left |x_i \right | < \infty \right \} \right ) \\ \left ( \ell^{\infty}  = \left \{ \left (x_1,x_2, \cdots \right )\ :\ x_i \in \Bbb C, \sup\limits_{i \in \Bbb N} \left |x_i \right | < \infty \right \} \right   ) \end{align*}$$
Which of the above statements is/are TRUE $?$
$(\text A)$ Both $\text P$ and $\text Q.$
$(\text B)$ $\text P$ only.
$(\text C)$ $\text Q$ only.
$(\text D)$ Neither $\text P$ nor $\text Q.$

How do I solve this problem? Any help will be highly appreciated.
Thank you very much.
EDIT $:$ What I can see is that the column vectors of $K$ are in $\ell^{1}.$ Can it help anyway? I think $E$ is bounded but for that we need only to show that the sequence $\bigg \{ \sup\limits_{j \in \Bbb N} \left |k_{i,j} \right | \bigg \}_{i=1}^{\infty}$ of real numbers is bounded. How do I show that?
Suppose the sequence $\bigg \{ \sup\limits_{j \in \Bbb N} \left |k_{i,j} \right | \bigg \}_{i=1}^{\infty}$ of real numbers is unbounded then we can find a strictly increasing sequence $\big \{i_r \big \}_{r=1}^{\infty}$ of natural numbers such that $$\sup\limits_{j \in \Bbb N} \left |k_{i_r,j} \right | > r,\ \text {for each}\ r \in \Bbb N.$$ So $\exists$ another sequence $\big \{j_r \big \}_{r = 1}^{\infty}$ of natural numbers such that $$\left |k_{i_r,j_r} \right | > r,\ \text {for each}\ r \in \Bbb N.$$ Now this would yield a sequence $\bigg \{\left |k_{i_r,j_r} \right | \bigg \}_{r = 1}^{\infty}$ of real numbers such that $$\left |k_{i_r,j_r} \right | > r,\ \text {for each}\ r \in \Bbb N.\ \ \ \ \ \ (1)$$
Now how do I proceed? I think that I have to somehow use condition $(\text {ii} )$ here. Since the column vectors of $K$ are in $\ell^1$ we have for any fixed $j \in \Bbb N$ $$\lim\limits_{r \to \infty} \left |k_{i_r,j} \right | = 0.$$
So in particular if we take $j=j_r$ then we have $$\lim\limits_{r \to \infty} \left | k_{i_r,j_r} \right | = 0$$ which contradicts $(1).$ Is it correct what I have argued? Please verify it.
I don't think the last argument is true. The matrix $K$ may be such that for each $r \in \Bbb N,$ $j_r$'s could have been distinct and $k_{i_r,j_r}$ is the last non-zero entry in the $j_r^{\text {th}}$ column and $\left |k_{i_r,j_r} \right | = r + 1 > r.$ That's why I get stuck and can't able to proceed further.

REPLY [1 votes]: $E$ is countable and thus never dense in the non-separable space $\ell^\infty$.
Asumption (ii) says that $T:\ell^1\to \ell^1$, $T(x)=\left(\sum\limits_{j=1}^\infty k_{i,j}x_j\right)_{i\in\mathbb N}$ is a well-defined map which is obviously linear. Show that its graph is closed (because it is continuous with respect to the weaker topology of coordinate-wise convergence on the range) to conclude its continuity. This gives you a uniform bound
$$
c=\sup\{\sum_{i=1}^\infty\left|\sum_{j=1}^\infty k_{i,j}x_j\right|: x\in\ell^1,\|x\|_1\le 1\}<\infty.
$$
For fixed $i_0,j_0$ plug in the sequence $x$ which has only $0$ entries but at the $j_0$-th spot where the entry is the sign of $k_{i_0,j_0}$ (in the complex case, the sign of $z\in\mathbb C\setminus\{0\}$ is $|z|/z$). This gives $|k_{i_0,j_0}|\le c$ for all $(i_0,j_0)$ and hence the boundedness of the set of rows in $\ell^\infty$.

Instead of the closed graph theorem it is also possible to use the uniform boundedness principle for the maps $T_i(x)=\sum\limits_{j=1}^\infty k_{i,j}x_j$. This would require an assumption  weaker than (ii).


TITLE: Limit of Gamma functions
QUESTION [1 upvotes]: I need to prove:
$$\lim_{p \to\infty}\frac{\Gamma \left ({\dfrac{p+1}{2}} \right )}{\Gamma(p/2)\sqrt{p\pi}}= \frac{1}{\sqrt{2\pi}}.$$
Where $\Gamma (x)$ represents the gamma function.
To provide some context, I need to find the limiting distribution of a student's t distribution , which should converge to the normal distribution. The key part of the proof translates to solving the above limit.

REPLY [1 votes]: As $p\to +\infty$ the Gamma function has the asymptotic approximation:
$$\Gamma\left(\frac{p+1}{2}\right) \sim \large e^{\frac{p}{2}\left(1 - \ln(2) - \ln\left(\frac{1}{p}\right)\right)}\left(\sqrt{2\pi} - \frac{1}{6p}\sqrt{\frac{\pi}{2}} + \mathcal{O}\left(\frac{1}{p}\right)^{3/2}\right)$$
and
$$\Gamma\left(\frac{p}{2}\right) \sim \large e^{\frac{p}{2}\left(1 - \ln(2) - \ln\left(\frac{1}{p}\right)\right)}\left(2\sqrt{\pi}\frac{1}{\sqrt{p}} + \mathcal{O}\left(\frac{1}{p}\right)^{3/2}\right)$$
Hence substituting into the limit:
$$\frac{e^{\frac{p}{2}\left(1 - \ln(2) - \ln\left(\frac{1}{p}\right)\right)}\left(\sqrt{2\pi} - \frac{1}{6p}\sqrt{\frac{\pi}{2}} + \mathcal{O}\left(\frac{1}{p}\right)^{3/2}\right)}{e^{\frac{p}{2}\left(1 - \ln(2) - \ln\left(\frac{1}{p}\right)\right)}\left(2\sqrt{\pi}\frac{1}{\sqrt{p}} + \mathcal{O}\left(\frac{1}{p}\right)^{3/2}\right)\cdot \sqrt{p\pi}} = \frac{\left(\sqrt{2\pi} - \frac{1}{6p}\sqrt{\frac{\pi}{2}} + \mathcal{O}\left(\frac{1}{p}\right)^{3/2}\right)}{\left(2\sqrt{\pi}\frac{1}{\sqrt{p}} + \mathcal{O}\left(\frac{1}{p}\right)^{3/2}\right)\sqrt{p\pi}}$$
Which, as $p \to +\infty$ goes to
$$\frac{\sqrt{2\pi}}{2\pi} = \color{red}{\frac{1}{\sqrt{2\pi}}}$$
As wanted.


text:
(*  Title:       Safe OCL
    Author:      Denis Nikiforov, March 2019
    Maintainer:  Denis Nikiforov <denis.nikif at gmail.com>
    License:     LGPL
*)
chapter \<open>Basic Types\<close>
theory OCL_Basic_Types
  imports Main "HOL-Library.FSet" "HOL-Library.Phantom_Type"
begin

(*** Definition *************************************************************)

section \<open>Definition\<close>

text \<open>
  Basic types are parameterized over classes.\<close>

type_synonym 'a enum = "('a, String.literal) phantom"
type_synonym elit = String.literal

datatype ('a :: order) basic_type =
  OclAny
| OclVoid
| Boolean
| Real
| Integer
| UnlimitedNatural
| String
| ObjectType 'a ("\<langle>_\<rangle>\<^sub>\<T>" [0] 1000)
| Enum "'a enum"

inductive basic_subtype (infix "\<sqsubset>\<^sub>B" 65) where
  "OclVoid \<sqsubset>\<^sub>B Boolean"
| "OclVoid \<sqsubset>\<^sub>B UnlimitedNatural"
| "OclVoid \<sqsubset>\<^sub>B String"
| "OclVoid \<sqsubset>\<^sub>B \<langle>\<C>\<rangle>\<^sub>\<T>"
| "OclVoid \<sqsubset>\<^sub>B Enum \<E>"

| "UnlimitedNatural \<sqsubset>\<^sub>B Integer"
| "Integer \<sqsubset>\<^sub>B Real"
| "\<C> < \<D> \<Longrightarrow> \<langle>\<C>\<rangle>\<^sub>\<T> \<sqsubset>\<^sub>B \<langle>\<D>\<rangle>\<^sub>\<T>"

| "Boolean \<sqsubset>\<^sub>B OclAny"
| "Real \<sqsubset>\<^sub>B OclAny"
| "String \<sqsubset>\<^sub>B OclAny"
| "\<langle>\<C>\<rangle>\<^sub>\<T> \<sqsubset>\<^sub>B OclAny"
| "Enum \<E> \<sqsubset>\<^sub>B OclAny"

declare basic_subtype.intros [intro!]

inductive_cases basic_subtype_x_OclAny [elim!]: "\<tau> \<sqsubset>\<^sub>B OclAny"
inductive_cases basic_subtype_x_OclVoid [elim!]: "\<tau> \<sqsubset>\<^sub>B OclVoid"
inductive_cases basic_subtype_x_Boolean [elim!]: "\<tau> \<sqsubset>\<^sub>B Boolean"
inductive_cases basic_subtype_x_Real [elim!]: "\<tau> \<sqsubset>\<^sub>B Real"
inductive_cases basic_subtype_x_Integer [elim!]: "\<tau> \<sqsubset>\<^sub>B Integer"
inductive_cases basic_subtype_x_UnlimitedNatural [elim!]: "\<tau> \<sqsubset>\<^sub>B UnlimitedNatural"
inductive_cases basic_subtype_x_String [elim!]: "\<tau> \<sqsubset>\<^sub>B String"
inductive_cases basic_subtype_x_ObjectType [elim!]: "\<tau> \<sqsubset>\<^sub>B \<langle>\<C>\<rangle>\<^sub>\<T>"
inductive_cases basic_subtype_x_Enum [elim!]: "\<tau> \<sqsubset>\<^sub>B Enum \<E>"

inductive_cases basic_subtype_OclAny_x [elim!]: "OclAny \<sqsubset>\<^sub>B \<sigma>"
inductive_cases basic_subtype_ObjectType_x [elim!]: "\<langle>\<C>\<rangle>\<^sub>\<T> \<sqsubset>\<^sub>B \<sigma>"

lemma basic_subtype_asym:
  "\<tau> \<sqsubset>\<^sub>B \<sigma> \<Longrightarrow> \<sigma> \<sqsubset>\<^sub>B \<tau> \<Longrightarrow> False"
  by (induct rule: basic_subtype.induct, auto)

(*** Partial Order of Basic Types *******************************************)

section \<open>Partial Order of Basic Types\<close>

instantiation basic_type :: (order) order
begin

definition "(<) \<equiv> basic_subtype\<^sup>+\<^sup>+"
definition "(\<le>) \<equiv> basic_subtype\<^sup>*\<^sup>*"

(*** Strict Introduction Rules **********************************************)

subsection \<open>Strict Introduction Rules\<close>

lemma type_less_x_OclAny_intro [intro]:
  "\<tau> \<noteq> OclAny \<Longrightarrow> \<tau> < OclAny"
proof -
  have "basic_subtype\<^sup>+\<^sup>+ OclVoid OclAny"
    by (rule_tac ?b="Boolean" in tranclp.trancl_into_trancl; auto)
  moreover have "basic_subtype\<^sup>+\<^sup>+ Integer OclAny"
    by (rule_tac ?b="Real" in tranclp.trancl_into_trancl; auto)
  moreover hence "basic_subtype\<^sup>+\<^sup>+ UnlimitedNatural OclAny"
    by (rule_tac ?b="Integer" in tranclp_into_tranclp2; auto)
  ultimately show "\<tau> \<noteq> OclAny \<Longrightarrow> \<tau> < OclAny"
    unfolding less_basic_type_def
    by (induct \<tau>, auto)
qed

lemma type_less_OclVoid_x_intro [intro]:
  "\<tau> \<noteq> OclVoid \<Longrightarrow> OclVoid < \<tau>"
proof -
  have "basic_subtype\<^sup>+\<^sup>+ OclVoid OclAny"
    by (rule_tac ?b="Boolean" in tranclp.trancl_into_trancl; auto)
  moreover have "basic_subtype\<^sup>+\<^sup>+ OclVoid Integer"
    by (rule_tac ?b="UnlimitedNatural" in tranclp.trancl_into_trancl; auto)
  moreover hence "basic_subtype\<^sup>+\<^sup>+ OclVoid Real"
    by (rule_tac ?b="Integer" in tranclp.trancl_into_trancl; auto)
  ultimately show "\<tau> \<noteq> OclVoid \<Longrightarrow> OclVoid < \<tau>"
    unfolding less_basic_type_def
    by (induct \<tau>; auto)
qed

lemma type_less_x_Real_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> < Real"
  "\<tau> = Integer \<Longrightarrow> \<tau> < Real"
  unfolding less_basic_type_def
  by (rule rtranclp_into_tranclp2, auto)

lemma type_less_x_Integer_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> < Integer"
  unfolding less_basic_type_def
  by (rule rtranclp_into_tranclp2, auto)

lemma type_less_x_ObjectType_intro [intro]:
  "\<tau> = \<langle>\<C>\<rangle>\<^sub>\<T> \<Longrightarrow> \<C> < \<D> \<Longrightarrow> \<tau> < \<langle>\<D>\<rangle>\<^sub>\<T>"
  unfolding less_basic_type_def
  using dual_order.order_iff_strict by blast

(*** Strict Elimination Rules ***********************************************)

subsection \<open>Strict Elimination Rules\<close>

lemma type_less_x_OclAny [elim!]:
  "\<tau> < OclAny \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Boolean \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Integer \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Real \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = String \<Longrightarrow> P) \<Longrightarrow>
   (\<And>\<E>. \<tau> = Enum \<E> \<Longrightarrow> P) \<Longrightarrow>
   (\<And>\<C>. \<tau> = \<langle>\<C>\<rangle>\<^sub>\<T> \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_OclVoid [elim!]:
  "\<tau> < OclVoid \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_Boolean [elim!]:
  "\<tau> < Boolean \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_Real [elim!]:
  "\<tau> < Real \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Integer \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_Integer [elim!]:
  "\<tau> < Integer \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_UnlimitedNatural [elim!]:
  "\<tau> < UnlimitedNatural \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_String [elim!]:
  "\<tau> < String \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

lemma type_less_x_ObjectType [elim!]:
  "\<tau> < \<langle>\<D>\<rangle>\<^sub>\<T> \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<And>\<C>. \<tau> = \<langle>\<C>\<rangle>\<^sub>\<T> \<Longrightarrow> \<C> < \<D> \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  apply (induct rule: converse_tranclp_induct)
  apply auto[1]
  using less_trans by auto

lemma type_less_x_Enum [elim!]:
  "\<tau> < Enum \<E> \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow> P"
  unfolding less_basic_type_def
  by (induct rule: converse_tranclp_induct; auto)

(*** Properties *************************************************************)

subsection \<open>Properties\<close>

lemma basic_subtype_irrefl:
  "\<tau> < \<tau> \<Longrightarrow> False"
  for \<tau> :: "'a basic_type"
  by (cases \<tau>; auto)

lemma tranclp_less_basic_type:
  "(\<tau>, \<sigma>) \<in> {(\<tau>, \<sigma>). \<tau> \<sqsubset>\<^sub>B \<sigma>}\<^sup>+ \<longleftrightarrow> \<tau> < \<sigma>"
  by (simp add: tranclp_unfold less_basic_type_def)

lemma basic_subtype_acyclic:
  "acyclicP basic_subtype"
  apply (rule acyclicI)
  using OCL_Basic_Types.basic_subtype_irrefl
    OCL_Basic_Types.tranclp_less_basic_type by auto

lemma less_le_not_le_basic_type:
  "\<tau> < \<sigma> \<longleftrightarrow> \<tau> \<le> \<sigma> \<and> \<not> \<sigma> \<le> \<tau>"
  for \<tau> \<sigma> :: "'a basic_type"
  unfolding less_basic_type_def less_eq_basic_type_def
  apply (rule iffI; auto)
  apply (metis (mono_tags) basic_subtype_irrefl
      less_basic_type_def tranclp_rtranclp_tranclp)
  by (drule rtranclpD; auto)

lemma antisym_basic_type:
  "\<tau> \<le> \<sigma> \<Longrightarrow> \<sigma> \<le> \<tau> \<Longrightarrow> \<tau> = \<sigma>"
  for \<tau> \<sigma> :: "'a basic_type"
  unfolding less_eq_basic_type_def less_basic_type_def
  by (metis (mono_tags, lifting) less_eq_basic_type_def
      less_le_not_le_basic_type less_basic_type_def rtranclpD)

lemma order_refl_basic_type [iff]:
  "\<tau> \<le> \<tau>"
  for \<tau> :: "'a basic_type"
  by (simp add: less_eq_basic_type_def)

instance
  by standard (auto simp add: less_eq_basic_type_def
        less_le_not_le_basic_type antisym_basic_type)

end

(*** Non-Strict Introduction Rules ******************************************)

subsection \<open>Non-Strict Introduction Rules\<close>

lemma type_less_eq_x_OclAny_intro [intro]:
  "\<tau> \<le> OclAny"
  using order.order_iff_strict by auto

lemma type_less_eq_OclVoid_x_intro [intro]:
  "OclVoid \<le> \<tau>"
  using order.order_iff_strict by auto

lemma type_less_eq_x_Real_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Real"
  "\<tau> = Integer \<Longrightarrow> \<tau> \<le> Real"
  using order.order_iff_strict by auto

lemma type_less_eq_x_Integer_intro [intro]:
  "\<tau> = UnlimitedNatural \<Longrightarrow> \<tau> \<le> Integer"
  using order.order_iff_strict by auto

lemma type_less_eq_x_ObjectType_intro [intro]:
  "\<tau> = \<langle>\<C>\<rangle>\<^sub>\<T> \<Longrightarrow> \<C> \<le> \<D> \<Longrightarrow> \<tau> \<le> \<langle>\<D>\<rangle>\<^sub>\<T>"
  using order.order_iff_strict by fastforce

(*** Non-Strict Elimination Rules *******************************************)

subsection \<open>Non-Strict Elimination Rules\<close>

lemma type_less_eq_x_OclAny [elim!]:
  "\<tau> \<le> OclAny \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = OclAny \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Boolean \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Integer \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Real \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = String \<Longrightarrow> P) \<Longrightarrow>
   (\<And>\<E>. \<tau> = Enum \<E> \<Longrightarrow> P) \<Longrightarrow>
   (\<And>\<C>. \<tau> = \<langle>\<C>\<rangle>\<^sub>\<T> \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_OclVoid [elim!]:
  "\<tau> \<le> OclVoid \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Boolean [elim!]:
  "\<tau> \<le> Boolean \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Boolean \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Real [elim!]:
  "\<tau> \<le> Real \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Integer \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Real \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Integer [elim!]:
  "\<tau> \<le> Integer \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Integer \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_UnlimitedNatural [elim!]:
  "\<tau> \<le> UnlimitedNatural \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = UnlimitedNatural \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_String [elim!]:
  "\<tau> \<le> String \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = String \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_ObjectType [elim!]:
  "\<tau> \<le> \<langle>\<D>\<rangle>\<^sub>\<T> \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<And>\<C>. \<tau> = \<langle>\<C>\<rangle>\<^sub>\<T> \<Longrightarrow> \<C> \<le> \<D> \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

lemma type_less_eq_x_Enum [elim!]:
  "\<tau> \<le> Enum \<E> \<Longrightarrow>
   (\<tau> = OclVoid \<Longrightarrow> P) \<Longrightarrow>
   (\<tau> = Enum \<E> \<Longrightarrow> P) \<Longrightarrow> P"
  by (drule le_imp_less_or_eq; auto)

(*** Simplification Rules ***************************************************)

subsection \<open>Simplification Rules\<close>

lemma basic_type_less_left_simps [simp]:
  "OclAny < \<sigma> = False"
  "OclVoid < \<sigma> = (\<sigma> \<noteq> OclVoid)"
  "Boolean < \<sigma> = (\<sigma> = OclAny)"
  "Real < \<sigma> = (\<sigma> = OclAny)"
  "Integer < \<sigma> = (\<sigma> = OclAny \<or> \<sigma> = Real)"
  "UnlimitedNatural < \<sigma> = (\<sigma> = OclAny \<or> \<sigma> = Real \<or> \<sigma> = Integer)"
  "String < \<sigma> = (\<sigma> = OclAny)"
  "ObjectType \<C> < \<sigma> = (\<exists>\<D>. \<sigma> = OclAny \<or> \<sigma> = ObjectType \<D> \<and> \<C> < \<D>)"
  "Enum \<E> < \<sigma> = (\<sigma> = OclAny)"
  by (induct \<sigma>, auto)

lemma basic_type_less_right_simps [simp]:
  "\<tau> < OclAny = (\<tau> \<noteq> OclAny)"
  "\<tau> < OclVoid = False"
  "\<tau> < Boolean = (\<tau> = OclVoid)"
  "\<tau> < Real = (\<tau> = Integer \<or> \<tau> = UnlimitedNatural \<or> \<tau> = OclVoid)"
  "\<tau> < Integer = (\<tau> = UnlimitedNatural \<or> \<tau> = OclVoid)"
  "\<tau> < UnlimitedNatural = (\<tau> = OclVoid)"
  "\<tau> < String = (\<tau> = OclVoid)"
  "\<tau> < ObjectType \<D> = (\<exists>\<C>. \<tau> = ObjectType \<C> \<and> \<C> < \<D> \<or> \<tau> = OclVoid)"
  "\<tau> < Enum \<E> = (\<tau> = OclVoid)"
  by auto

(*** Upper Semilattice of Basic Types ***************************************)

section \<open>Upper Semilattice of Basic Types\<close>

notation sup (infixl "\<squnion>" 65)

instantiation basic_type :: (semilattice_sup) semilattice_sup
begin

(* We use "case"-style because it works faster *)
fun sup_basic_type where
  "\<langle>\<C>\<rangle>\<^sub>\<T> \<squnion> \<sigma> = (case \<sigma> of OclVoid \<Rightarrow> \<langle>\<C>\<rangle>\<^sub>\<T> | \<langle>\<D>\<rangle>\<^sub>\<T> \<Rightarrow> \<langle>\<C> \<squnion> \<D>\<rangle>\<^sub>\<T> | _ \<Rightarrow> OclAny)"
| "\<tau> \<squnion> \<sigma> = (if \<tau> \<le> \<sigma> then \<sigma> else (if \<sigma> \<le> \<tau> then \<tau> else OclAny))"

lemma sup_ge1_ObjectType:
  "\<langle>\<C>\<rangle>\<^sub>\<T> \<le> \<langle>\<C>\<rangle>\<^sub>\<T> \<squnion> \<sigma>"
  apply (induct \<sigma>; simp add: basic_subtype.simps
        less_eq_basic_type_def r_into_rtranclp)
  by (metis Nitpick.rtranclp_unfold basic_subtype.intros(8)
        le_imp_less_or_eq r_into_rtranclp sup_ge1)

lemma sup_ge1_basic_type:
  "\<tau> \<le> \<tau> \<squnion> \<sigma>"
  for \<tau> \<sigma> :: "'a basic_type"
  apply (induct \<tau>, auto)
  using sup_ge1_ObjectType by auto

lemma sup_commut_basic_type:
  "\<tau> \<squnion> \<sigma> = \<sigma> \<squnion> \<tau>"
  for \<tau> \<sigma> :: "'a basic_type"
  by (induct \<tau>; induct \<sigma>; auto simp add: sup.commute)

lemma sup_least_basic_type:
  "\<tau> \<le> \<rho> \<Longrightarrow> \<sigma> \<le> \<rho> \<Longrightarrow> \<tau> \<squnion> \<sigma> \<le> \<rho>"
  for \<tau> \<sigma> \<rho> :: "'a basic_type"
  by (induct \<rho>; auto)

instance
  by standard (auto simp add: sup_ge1_basic_type
        sup_commut_basic_type sup_least_basic_type)

end

(*** Code Setup *************************************************************)

section \<open>Code Setup\<close>

code_pred basic_subtype .

fun basic_subtype_fun :: "'a::order basic_type \<Rightarrow> 'a basic_type \<Rightarrow> bool" where
  "basic_subtype_fun OclAny \<sigma> = False"
| "basic_subtype_fun OclVoid \<sigma> = (\<sigma> \<noteq> OclVoid)"
| "basic_subtype_fun Boolean \<sigma> = (\<sigma> = OclAny)"
| "basic_subtype_fun Real \<sigma> = (\<sigma> = OclAny)"
| "basic_subtype_fun Integer \<sigma> = (\<sigma> = Real \<or> \<sigma> = OclAny)"
| "basic_subtype_fun UnlimitedNatural \<sigma> = (\<sigma> = Integer \<or> \<sigma> = Real \<or> \<sigma> = OclAny)"
| "basic_subtype_fun String \<sigma> = (\<sigma> = OclAny)"
| "basic_subtype_fun \<langle>\<C>\<rangle>\<^sub>\<T> \<sigma> = (case \<sigma>
    of \<langle>\<D>\<rangle>\<^sub>\<T> \<Rightarrow> \<C> < \<D>
     | OclAny \<Rightarrow> True
     | _ \<Rightarrow> False)"
| "basic_subtype_fun (Enum _) \<sigma> = (\<sigma> = OclAny)"

lemma less_basic_type_code [code]:
  "(<) = basic_subtype_fun"
proof (intro ext iffI)
  fix \<tau> \<sigma> :: "'a basic_type"
  show "\<tau> < \<sigma> \<Longrightarrow> basic_subtype_fun \<tau> \<sigma>"
    apply (cases \<sigma>; auto)
    using basic_subtype_fun.elims(3) by fastforce
  show "basic_subtype_fun \<tau> \<sigma> \<Longrightarrow> \<tau> < \<sigma>"
    apply (erule basic_subtype_fun.elims, auto)
    by (cases \<sigma>, auto)
qed

lemma less_eq_basic_type_code [code]:
  "(\<le>) = (\<lambda>x y. basic_subtype_fun x y \<or> x = y)"
  unfolding dual_order.order_iff_strict less_basic_type_code
  by auto

end

subset_name: curated


TITLE: Convergence properties of $z^{z^{z^{...}}}$ and is it "chaotic"
QUESTION [8 upvotes]: $\DeclareMathOperator{\Arg}{Arg}$
Let $z \in \mathbb{C}.$  Let $b = W(-\ln z)$ where $W$ is the Lambert W Function.  Define the sequence $a_n$ by $a_0 = z$ and $a_{n+1} = {a_0}^{a_n}$ for $n \geq 1$, that is to say $a_n$ is the sequence $z, z^z, z^{z^z} ...$
I am trying to classify the sequence $a_n$ as convergent or divergent (i.e. not convergent) according to $|b|$.  My approach to this involves defining $2$ additional sequences: $b_n = \ln a_n$ and $c_n = b_n - b$.  Then $b_{n+1} =  \ln \left(z^{e^{b_n}}\right) = e^{b_n} \ln z$ and $c_{n+1} = e^{(b + c_n)} \ln z - b= (e^b \ln z) e^{c_n}  - b  = b e^{c_n}  - b = b (e^{c_n}  - 1)$.  Suppose $b_n \to b \implies c_n \to 0 \implies e^{c_n} - 1 \sim c_n \implies c_{n+1} \sim bc_n$.  From here there are $3$ cases to consider:
If $|b| > 1$ then $c_n$ is increasing without bound, so it clearly cannot converge except if $c_0 = 0$ which would imply $c_n = 0$ for every $n$ which is not the case because $b_0 =\ln z$ so $b_1 = e^{\ln z}\ln z \ne b_0$ so $c_1 \ne c_0$, a contradiction $\implies b_n$ is divergent $\implies a_n$ is divergent.
If $|b| < 1$ then $c_n$ is decreasing towards $0 \implies b_n$ is convergent $\implies a_n$ is convergent.
If $|b| = 1$ then $c_n \to c \ne 0 \implies b_n$ is divergent $\implies a_n$ is divergent.
I would like to give credit to user1952009.  The method involving the sequences $b_n$ and $c_n$ is due to them.
Edit 1: After reading Yiannis Galidakis's answer several times, I have decided it is mostly satisfactory.  Having said that, I feel I must clarify my position on chaotic sequences.  When I said the concept of a chaotic sequence was nonsense, that was an exaggeration.  What I meant to say was the definition given in the previous post didn't really make sense to me.  The one given here is detailed and precise enough that I can understand what it actually means.
However, I do not believe the statements "$a_n$ is chaotic" and "$a_n$ does not converge" are incompatible.  Setting aside the question of whether $a_n$ is chaotic or not, I feel I have given a plausibility argument (although not a rigorous proof) that $a_n$ is convergent if and only if $c_n \to 0$ which happens if and only if $|b| < 1$.
On a different note, I have been experimenting numerically with $a_n$ for at least $3$ years.  I believe (but cannot prove) that whenever $z$ is not purely real and $|b| = |W(-\ln z)| > 1$ the sequence $a_n$
actually has a $k$-cycle for some $k \in \mathbb{N}$.  It appears that $k = 3$ for all sufficiently large $|z|$ and that $k \to \infty$ as $|b| \to 1$.
Similarly, whenever the sequence "shoots off" too a neighborhood of $\infty$ I have found that $a_n \sim$ {$..., \infty, 0, 1, z, z^z ...$}  I will admit however that I cannot predict when the sequence will "shoot of" to $\infty$.
At this point I have $2$ main questions: is my convergence analysis correct?  Are there any values of $z$, not purely real, such that $a_n$ is unbounded, i.e, the sequence "blows up" to $\infty$ and never "comes back down."
Apologies for a somewhat lengthy post.
Edit 2: In Addendum 2 in Yiannis Galidakis's answer, it is stated that if $c \in \mathbb{C}$ and $|\Re(c)| > \exp(\exp(-1))$ and $\Arg{c}=2\pi\alpha$ with $\alpha\in\mathbb{R}\setminus\mathbb{Q}$ then the iterated exponential will be unbounded.  This is not quite correct.  The part about irrational rotation is fine, but it is not enough to have $|\Re(c)| > \exp(\exp(-1))$.  Consider $c = 2\exp(e\pi i/14) \approx 1.6393177+1.1457037i$.  Clearly $c$ satisfies both conditions. However $|W(-\ln c)| \approx .890512$.  Hence the iterated exponential is convergent, hence it is bounded.  A few other counterexamples are given by $c = k\exp(e\pi i/14)$ for $k \in \mathbb{R}$ and $1.76253 \le k \le 2.34896$

REPLY [5 votes]: This is an extended response to Yiannis Galidakis's question.
I have been experimenting with the value $c$ they gave in the previous post.  It is in case 3b since $|t| = |W(-\ln c)| = 1$ and there is no $n \in \mathbb{N}$ such that $t^n = 1$.  I have evaluated the sequence $a_n$ for $0 \leq n \leq 10^8$.  As in Gottfried Helm's analysis, I have found no evidence that the terms are contracting towards some limit.  In fact, it appears the sequence is frequently "slingshot" to a neighborhood of $\infty$, and that the terms are being "slingshot" progressively farther out as $n \to \infty$.  As an example, the largest such "slingshot" has $|a_n| = 17.1$ for $n \leq 10^6$.  For $n \leq 10^8$  this increases to about $25$.  In all such cases, I have observed that $a_n \sim$ {$...,\infty, 0, 1, z, z^z, ...$}.  For these reasons I believe $a_n$ is divergent (i.e. not convergent) in case 3b.
As to whether $a_n$ is chaotic or not, I am not completely sure.  This may be a bad analogy, but, the way I have come to think of it, when we say a sequence or other mathematical object/phenomenon is chaotic, what we're really saying is the condition number of some function is very high relative to some other function.  By this definition, I believe the sequence $a_n$ can be chaotic in all cases, but is especially chaotic in cases 3a and 3b.  For one thing, an arbitrarily small perturbation in $a_0 = z$ can leave the sequence in the same case or shift it into any of the others.  Also, using the formula $cond(f(x)) =  \frac{xf'(x)}{f(x)}$ we see that $a_n$ is very ill-conditioned when it is "slingshot" near $\infty$.
In spite of these issues, I do not lose much sleep over it.  As far as I know, there are $4$ ways to alleviate the difficulty of an ill-conditioned problem.

Supercomputers
Arbitrary precision calculators
A very sophisticated algorithm
A lot of time and effort

Of course there are some problems where even all $4$ of these are not enough.  As someone once said "Computers and calculators are not replacements for mathematical thought. They are just replacements for some kinds of mathematical labor, either numerical or symbolic. There are, and always will be, mathematical problems that can’t be solved by a calculator or computer, regardless of its size and speed."


TITLE: Why are Galois extensions mapped to themselves?
QUESTION [1 upvotes]: Let $L$ be the splitting field of a separable irreducible polynomial $f(x)\in\Bbb{Q}[x]$. Consider the Galois subfield $K\subset L$. Let $\sigma\in \text{Gal}(L/\Bbb{Q})$. As $K$ is a galois extension, $\sigma(K)=K$.

I don't understand why $K$ being a Galois extension implies $\sigma(K)=K$. Any help would be great.

REPLY [2 votes]: Since $K/F$ is a Galois extension, it is a normal extension, meaning that the minimal polynomial of any $a\in K$, $f_a$, splits over $K$.
Let $\sigma\in\mathrm{Gal}\left(L/F\right)$ and let $a\in K$. $\sigma\left(a\right)$ is a root of $f_a$, hence $\sigma\left(a\right)\in K$. This proves $\sigma\left(K\right)\subseteq K$, and thus $\sigma\left(K\right)=K$ (dimension or something similar).