text:
\begin{document}
\newtheorem{Proposition}{\quad Proposition}[section]
\newtheorem{Theorem}[Proposition]{\quad Theorem}
\newtheorem{Definition}[Proposition]{\quad Definition}
\newtheorem{Corollary}[Proposition]{\quad Corollary}
\newtheorem{Lemma}[Proposition]{\quad Lemma}
\newtheorem{Example}[Proposition]{\quad Example}
\newtheorem{Remark}[Proposition]{\quad Remark}

\maketitle \addtocounter{section}{-1}

\numberwithin{equation}{section}

\date{}

\begin {abstract} Universal enveloping algebras of braided
m-Lie algebras and PBW theorem are obtained by means of
combinatorics on words.

\vskip0.1cm 2000 Mathematics Subject Classification: 16W30, 16G10

keywords: Braided Lie algebra, Universal enveloping algebras.
\end {abstract}

\section{Introduction}\label {s0}

The theory of Lie superalgebras has been developed systematically,
which includes  the representation theory and classifications of
simple Lie superalgebras and their varieties \cite {Ka77} \cite
{BMZP92}.  In many physical applications or in pure mathematical
interest, one has to consider not only ${\bf Z}_2$- or ${\bf Z}$-
grading but also $G$-grading of Lie algebras, where $G$ is an
abelian group equipped with a skew symmetric bilinear form given by
a 2-cocycle. Lie algebras in symmetric and more general categories
were discussed in \cite {Gu86} and \cite {GRR95}. A sophisticated
multilinear version of the Lie bracket was considered in \cite
{Kh99} \cite {Pa98}. Various generalized Lie algebras have already
appeared  under different names, e.g. Lie color algebras, $\epsilon
$ Lie algebras \cite {Sc79}, quantum and braided Lie algebras,
generalized Lie algebras \cite {BFM96} and $H$-Lie algebras \cite
{BFM01}.

In  \cite {Ma94c}, Majid introduced braided Lie algebras from
geometrical point of view, which have attracted attention in
mathematics and mathematical physics (see e.g. \cite {Ma95b} and
references therein).

In paper \cite {ZZ04}, braided m-Lie algebras was introduced,  which
generalize Lie algebras, Lie color algebras and quantum Lie
algebras. Two classes of braided m-Lie algebras are given, which are
generalized matrix braided m-Lie algebras and braided m-Lie
subalgebras of $End _F M$, where $M$ is a Yetter-Drinfeld module
over $B$ with dim $B< \infty $ . In particular, generalized
classical braided m-Lie algebras $sl_{q, f}( GM_G(A),  F)$  and
$osp_{q, t} (GM_G(A), M, F)$  of generalized matrix algebra
$GM_G(A)$ are constructed  and their connection with special
generalized matrix Lie superalgebra $sl_{s, f}( GM_{{\bf Z}_2}(A^s),
F)$  and orthosymplectic generalized matrix Lie super algebra
$osp_{s, t} (GM_{{\bf Z}_2}(A^s), M^s, F)$  are established. The
relationship between representations of braided m-Lie algebras and
their  associated algebras are established. In this paper we follow
paper \cite {ZZ04} and obtain  universal enveloping algebras of
braided m-Lie algebras and PBW theorem by means of combinatorics on
words (see \cite {Lo83}).

Throughout, $ F$ is a field,

\section {Braided  m-Lie Algebras}

 We recalled two concepts.

\begin {Definition} \label {4'.1.1} (See \cite {ZZ04})
Let  $(L, [\ \ ])$ be an object in the braided tensor category $
({\cal C }, C)$ with morphism $[\ \ ] : L \otimes L \rightarrow L$.
If there exists an algebra $(A, m)$ in  $ ({\cal C }, C)$ and
monomorphism $\phi : L \rightarrow A$ such that   $\phi [\  \ ] = m
(\phi \otimes \phi ) - m (\phi \otimes \phi )  C_{L, L},$   then
$(L, [ \ \  ])$ is called a braided m-Lie algebra in $ ({\cal C },
C)$ induced by multiplication of $A$ through $\phi $. Algebra $(A,
m) $ is called an algebra  associated to $(L, [ \ \ ])$.

\end {Definition}
A Lie  algebra is a braided m-Lie algebra in the category of
ordinary vector spaces, a Lie color algebra is a braided  m-Lie
algebra
 in symmetric braided tensor category $ ({\cal M} ^{FG}, C^r)$ since the
 canonical map $\sigma: L \rightarrow U(L)$ is injective (see
\cite [Proposition 4.1]{Sc79}), a  quantum Lie  algebra is a braided
m-Lie algebra in the Yetter-Drinfeld category $ (^B_B{\cal YD}, C)$
by \cite [Definition 2.1 and Lemma 2.2]{GM03}), and a ``good"
braided Lie  algebra is a braided  m-Lie algebra
 in the Yetter-Drinfeld category $ (^B_B{\cal YD}, C)$ by
 \cite [Definition 3.6 and Lemma 3.7]{GM03}).
For  a cotriangular Hopf algebra $(H, r)$, the $(H,r)$-Lie algebra
defined in \cite [4.1] {BFM01} is a
 braided m-Lie  algebra in the braided
tensor category $({}^H{\cal M}, C^r)$.  Therefore, the braided m-Lie
algebras generalize most known generalized Lie algebras.

For an algebra $(A, m)$ in $({\cal C}, C)$, obviously $L = A$ is  a
braided m-Lie algebra under operation $ [\ \ ] = m  - m   C_{L, L}$,
which  is induced by $A$ through $id _A$. This  braided  m-Lie
algebra is written as $A^-$.

\begin {Definition}\label {1} (see \cite {Zh99})
Let H be a Hopf algebra,
 $(V, \alpha)$ and  $(V,  \delta )$ be  a left  $H$-module and  a left  $H$-comodule, respectively. If
\begin {eqnarray} \label {EYD}\delta(\alpha(h\otimes v))=\delta(h\cdot v)=\sum h_{(1)}v_{(-1)}S(h_{(3)})\otimes h_{(2)}.v_{0}\end {eqnarray}
$\forall v\in V$, $h\in G$,  then  $(V, \alpha, \delta )$ is called  a Yetter-Drinfeld module over $H$, or a $H$- {\rm YD} module in short. All of
$H$- {\rm YD} module construct a braided tensor category, called the Yetter-Drinfeld module category, denoted as $(^H_H {\cal YD}, C)$, where $C$ is the braiding.
\end {Definition}
If $H= FG$ is a group algebra and  $(V, \alpha, \delta)$ is an $FG$-
{\rm YD} module, then $V$ becomes a $G$-graded space  $V = \oplus
_{g\in G}V_g$ and the condition (\ref {EYD}) becomes
\begin {eqnarray} \label {EYDG}\delta(\alpha(h\otimes v))=\delta(h \cdot v)=\sum h gh^{-1}\otimes h \cdot v \end {eqnarray} for any $h, g \in G, $ $v\in V_g.$

Let $G$ be a group and $\chi $ a bicharacter of $G$, i.e. $\chi$ is
a map from $G \times G$ to $F$ satisfying  $\chi (ab, c) = \chi (a,
c)\chi (b, c)$, $\chi (a, bc) = \chi (a, b)\chi (a, c) $  and $\chi
(a, e) =1 = \chi (e, a)$ for any $a, b, c \in G$, where $e$ is the
unit element of $G$. The braiding of $FG$-{\rm YD} module $(V,
\alpha, \delta)$ is determined by bicharacter $\chi$ if  $h\cdot x =
\chi (h, g)x$ for any $h, g\in G,$ $x\in V_g.$ In this case,
 $C( x \otimes y)=\chi(g, h)y\otimes x$ for any
homogeneous elements $ x \in V _g, $ $y\in V_h$. Obviously, if the
braiding of $FG$-{\rm YD} module $(V,  \alpha, \delta)$ is
determined by bicharacter $\chi$, then the braiding of $(V,  \alpha,
\delta)$ is diagonal. Conversely, if the braiding of a braided
vector space  $V$ is diagonal, then $V$ can becomes an $F\mathbb
Z[I]$-{\rm YD} module, which braiding is determined by a bicharacter
(see \cite {He06}).  If $G$ is a finite abelian group and $V$ is a
$kG$-{\rm YD} module, then the braiding of $V$ is diagonal (see
\cite {ZZC04}). In this paper we only consider the braiding
determined by bicharacter $\chi.$

\section{Jacobi identity}

\begin {Lemma} (See \cite {Kh99}) If $L$ is braided
m-Lie algebra, then Jacobi identity holds:
 \begin{eqnarray}\label {Jacobi} [[a  b]  c]-[a  [b
c]]+\chi(a,b)b [a c]-\chi(b,c)[a c] b=0 \end {eqnarray} for any
homogeneous elements $a, b, c \in L$, where $\chi (a, b)$ denotes
$\chi (g, h)$ for $a\in V_g$, $b \in V_h.$
\end {Lemma}
{\bf Proof.}
\begin{eqnarray*}
 \mbox {the left side }&=& abc-\chi(a,b)bac-\chi(ab,c)cab+\chi(ab,c)\chi(a,b)cba\\
& &  -abc+\chi(b,c)acb+\chi(a,bc)bca-\chi(a,bc)\chi(b,c)cba \\
& &  +\chi(a,b)bac-\chi(a,b)\chi(a,c)bca-\chi(b,c)acb+\chi(b,c)\chi(a,c)cab\\
&=&  0. \Box
\end{eqnarray*}

\section{ Universal enveloping algebras of braided
m-Lie algebras and PBW theorem }

Let $E$ be a homogeneous  basis of braided  m-Lie algebra $L$ and
$B$ a set. Let $B^*$ denote the set of all words (see \cite {Lo83}) on $B$ and
 $\varphi$  a bijective map from $E$ to $B$. Define  $[bc]=\varphi([ef])$ for any
  $b = \varphi(e)$, $c = \varphi(f)$, $e, f \in E$.
  Let $\prec$ be an order of $B$ and $P = : \{b_{1}b_{2}\cdots  b_{n}\ | \  b_{i}\in B,
 b_n \prec b_{n-1} \prec \cdots \prec b_1, n \in \mathbb N \}$.

 For any $w\in B^*$, let $\nu (w)$ denote the number of  elements in
 set $\{ (r, s, t) \ | \ w=rasbt;  a,b \in B, r, s, t \in B^*, a\prec
 b,\}$ and $\nu(w)$ is called the index of $w$.
 Obviously, we have
\[
v(ubav)=v(uabv)-1
\] for any $a,b \in B, u, v  \in B^*, a\prec
 b$. We also have that $\nu (w)=0$ if and only if $w\in F$.

For any a set $X$, let $FX$ denote the vector space spanned by $X$
with basis  $X.$ It is clear that $FB^*$ is  the free algebra on
$B$. Meantime $FB^*$ also is the tensor algebra $T(FB)$ over $FB$.

\begin {Lemma} \label {3.1}
 There exists $\lambda : FB^* \rightarrow FP$ such that

{\rm (i)} $\lambda(f)= f,$ $f\in P$;

{\rm (ii)}
$\lambda(ubcv)=\chi(b,c)\lambda(ucbv)+\lambda(u[bc]v),u,v\in
B^{\ast},b,c\in B $;

{\rm (iii)}
$\lambda(uv)=\lambda(\lambda(u)v)=\lambda(u\lambda(v)),u,v\in FB^*$.
\end {Lemma}
{\bf Proof.} For $w \in B^*$, we define $\lambda (w)$ using an
induction first on the length and second on the index. If $w \in B$,
 define $\lambda (w) = w$. Let the length of  $w$ be larger than 1 and define
 $ \lambda (w) =: \chi(b,c)\lambda(ucbv)+\lambda(u[bc]v)$ for $w=ubcv$ with
  $b, c\in B$, $u, v \in B^*$. Now we show that the definition is well-defined. For
  $w=ubcv=u'b'c'v'$ with
  $b, c, b', c'\in B$, $u, v, u', v' \in B^*$, we only need  show that
   \begin {eqnarray} \label {e3.1}\chi(b,c)\lambda(ucbv)+\lambda(u[bc]v) =
 \chi(b',c')\lambda(u'c'b'v')+\lambda(u'[b'c']v'). \end {eqnarray}

We show this by following two  steps.

 ($1^\circ$) If  $|u| \le |u'|-2$, then $u'=ubct,v=tb'c'v',t\in B^{*}$.
 By induction hypothesis we have
\begin{eqnarray*}
\mbox {the left side  }  &=& \chi(b,c)\chi(b',c')\lambda(ucbtc'b'v')+\chi(b,c)\lambda(ucbt[b'c']v')\\
& &  +\chi(b',c')\lambda(u[bc]tc'b'v')+\lambda(u[bc]t[b'c']v')
\end{eqnarray*}
and
\begin{eqnarray*}
\mbox {the right side  }  &=& \chi(b,c)\chi(b',c')\lambda(ucbtc'b'v')+\chi(b,c)\lambda(ucbt[b'c']v')\\
& &  +\chi(b',c')\lambda(u[bc]tc'b'v')+\lambda(u[bc]t[b'c']v').
\end{eqnarray*}
Thus  (\ref {e3.1}) holds.

($2^\circ$) If $|u|=|u'|-1$£¬then $u'=ub,c=b',v=c'v'$. We only need
show $
\chi(a,b)\lambda(rbacs)+\lambda(r[ab]cs)=\chi(b,c)\lambda(racbs)+\lambda(ra[bc]s)
$. By induction hypothesis we have
\begin{eqnarray*}
\mbox {the left side  } &=&\chi(a,b)\{\chi(a,c)\lambda(rbcas)+\lambda(rb[ac]s)\}+\lambda(r[ab]cs)\\
&=&\chi(a,b)\chi(a,c)\lambda(rbcas)+\chi(a,b)\lambda(rb[ac]s)+\lambda(r[ab]cs)\\
&=&\chi(a,b)\chi(a,c)\{chi(b,c)\lambda(rcbas)+\lambda(r[bc]as)\}+\chi(a,b)\lambda(rb[ac]s)+\lambda(r[ab]cs)\\
&=&\chi(a,b)\chi(a,c)chi(b,c)\lambda(rcbas)+\chi(a,b)\chi(a,c)\lambda(r[bc]as)+\chi(a,b)\lambda(rb[ac]s)\\
& &+\lambda(r[ab]cs)
\end{eqnarray*} and
\begin{eqnarray*}
\mbox {the right side  } &=&\chi(b,c)\{\chi(a,c)\lambda(rcabs)+\lambda(r[ac]bs)\}+\lambda(ra[bc]s)\\
&=&\chi(b,c)\chi(a,c)\lambda(rcabs)+\chi(b,c)\lambda(r[ac]bs)+\lambda(ra[bc]s)\\
&=&\chi(b,c)\chi(a,c)\{\chi(a,b)\lambda(rcbas)+\lambda(rc[ab]s)\}+\chi(b,c)\lambda(r[ac]bs)+\lambda(ra[bc]s)\\
&=&\chi(b,c)\chi(a,c)\chi(a,b)\lambda(rcbas)+\chi(b,c)\chi(a,c)\lambda(rc[ab]s)+\chi(b,c)\lambda(r[ac]bs)\\
& &+\lambda(ra[bc]s).
\end{eqnarray*}
Thus
\begin{eqnarray*}
&&\mbox {the left side  } - \mbox {the right side  }\\
 &=&\{\chi(a,b)\chi(a,c)\lambda(r[bc]as)-\lambda(ra[bc]s)\}+\{\chi(a,b)\lambda(rb[ac]s)-\chi(b,c)\lambda(r[ac]bs)\}\\
& &+\{\lambda(r[ab]cs)-\chi(b,c)\chi(a,c)\lambda(rc[ab]s)\}\\
&=&-\lambda(r[a[bc]]s)+\lambda(\chi(a,b)rb[ac]s-\chi(b,c)r[ac]bs)+\lambda(r[[ab]c]s)\\
&=&0 \ \ \ \ { \mbox {(by Jacobi identity)}}.
\end{eqnarray*}

For (iii), we  use an induction first on the length and second on
the index.  Assume   $|w_1|\neq |w|$ and  $w=w_{1}w_{2}$. If
$w_{1}=ubct$, $b, c\in B$, $u, t \in B^*$, then
\begin{eqnarray*}
&\lambda(w)&=\chi(b,c)\lambda(ucbtw_{2})+\lambda(u[bc]tw_{2})\\
& &=\chi(b,c)\lambda(\lambda(ucbt)w_{2})+\lambda(\lambda(u[bc]t)w_{2})\\
& &=\lambda(\lambda(w_{1})w_{2})
\end{eqnarray*}
If $w_{1}=b$, $w_2 = cv$, $b, c \in B$, $v \in B^*$, then $\lambda
(w) = \lambda ( \lambda (w_1)w_2).$ $\Box$

\begin {Definition}
Suppose that ${L}$ is a braided  m-Lie algebra in $ ({\cal C }, C)$
and  $U$ is a algebra with Lie algebra homomorphism  $i :
L\rightarrow U^-$. $(U, i)$ is called the universal algebra of
braided m -Lie algebra $L$, if the following condition holds:  If
for any an algebra $W$ in  $({\cal C }, C)$ with a Lie algebra
homomorphism $\psi: L \rightarrow W^-$  in  $({\cal C }, C)$,  there
exists the unique algebra homomorphism  $\bar \psi : U \rightarrow
W$ in  $({\cal C }, C)$ such that   the following is commutative:
$$ \begin {array} {lcccr} {}&\varphi & {}\\
L& \longrightarrow &U \\
&  \psi  \searrow &  \downarrow   \bar \psi\\
 & & W &  . \end {array}.$$
\end {Definition}

 Obviously,
  $\varphi$ in section above is a Lie algebra monomorphism from $L$ to $FP$ in
$ ^{FG}_{FG} {\mathcal YD}$.

Let $U(L)=: FP$. Define the multiplication of $U(L)$ as follows: $u
* v=\lambda(uv) $ for any $ u, v \in P.$
 By Lemma \ref {3.1} (iii), $U(L)$ is an associative algebra:
$u\ast(v\ast
w)=\lambda(u\lambda(vw))=\lambda(uvw)=\lambda(\lambda(uv)w)=(u\ast
v)\ast w$ for any $u, v, w \in P.$ Obviously, $\lambda $ is an
algebra homomorphism.

\begin {Lemma} \label {3.4''} If $(V, \alpha, \delta )$ is an $FG$-{\rm YD} module, then
tensor algebra $T(V)$ over $V$ is an $FG$-{\rm YD} module.
\end {Lemma}
{\bf Proof.} By the universal property of tensor algebra, we can construct the module operation $\alpha ^{(T(V))}$ and comodule operation $\delta ^{(T(V))}$of $T(V)$ as follows:

 i) $$ \begin {array} {lcccr} {}&\delta^{(T(V))} & {}\\
T(V)& \longrightarrow &FG\otimes T(V)\\
i  \uparrow&  \nearrow ({\rm id} \otimes i)\delta^{(V)}  & \uparrow  {\rm id} \otimes i \\
 V&  \longrightarrow &  FG\otimes V \\
& \delta ^{(V )}&  \ \ \ \ \ \ \ \ \  .  \end {array}$$
ii) $$ \begin {array} {lcccr} {}&\alpha_{g} ^{(V )}& {}\\
V& \longrightarrow &V\\
i  \downarrow & \searrow i\alpha_{g} ^{(V)}  & i\downarrow  \\
 T(V)&  \longrightarrow &  T(V) \\
 & \alpha _g ^{(T(V))} &    \ \ \ \ \ \ \ \ \  ,
 \end {array}$$ where $\alpha ^{(V)}_g (v) =: \alpha (g \otimes v) = g\cdot v$ for any $v \in V,$ $g\in G.$

iii) For $\forall g\in G,$ $x_{j} \in V_{g_j}$, $1\le j \le r$, See that
\begin {eqnarray*}
\delta(g\cdot(x_{1}\cdot\cdot\cdot
x_{r}))&=&\delta (\alpha_{g}(x_{1}\cdot\cdot\cdot x_{r}))\\
&=&\delta((g\cdot x_{1})\cdot\cdot\cdot(g\cdot x_{r}))=\delta(g\cdot
x_{1})\cdot\cdot\cdot\delta(g\cdot x_{r})\\
&=&(gg_{1}g^{-1}\otimes (g\cdot
x_{1}))\cdot\cdot\cdot(gg_{r}g^{-1}\otimes (g\cdot x_{r}))\\
&=&(gg_{1}g^{-1})\cdot\cdot\cdot(gg_{r}g^{-1})\otimes
x_{1}\cdot\cdot\cdot x_{r}\\
&=&g(g_{1}\cdot\cdot\cdot g_{r})g^{-1}\otimes x_{1}\cdot\cdot\cdot
x_{r}.
\end {eqnarray*}
Thus $(T(V), \alpha, \delta)$ is an $FG$-{\rm YD} module.
Furthermore, considering {\rm (i)} and {\rm (ii)}, we have that
$T(V)$ is an algebra in    $^{FG} _{FG} {\mathcal YD}$. $\Box$

\begin {Lemma} \label {3.4'} {\rm (i)}  $FB^*$ is an $FG$-{\rm YD} module.

{\rm (ii)} $FP$ is an $FG$-{\rm YD} sub-module of $FB^*.$

{\rm (iii)} $FP$ is an algebra in $^{FG}_{FG}{\cal YD}$.
\end {Lemma}
{\bf Proof.} {\rm (i)} It follows from Lemma \ref {3.4''}.

{\rm (ii) } and {\rm (iii)}  are  clear. $\Box$

\begin {Theorem} \label {3.4}(PBW). $(U(L), \varphi$) is the universal enveloping
algebra of braided m-Lie algebra $L$.
\end {Theorem}
{\bf Proof.} For any an algebra $W$ in  $^{FG} _{FG} {\mathcal YD}$
with a Lie algebra homomorphism $\psi: L \rightarrow W^-$  in $^{FG}
_{FG} {\mathcal YD}$, define $\bar \psi : FB^* \rightarrow FP$ such
that $\bar \psi \varphi  = \psi$ and $\theta = : \bar \psi \mid
_{FP}$, the restriction of $\bar \psi$ on $FP.$ It is clear that the
following is commutative. $$ \begin {array} {lcccr} {}&\varphi & {}
& \lambda & {}\\
L& \longrightarrow &FB^* &\longrightarrow & FP\\
&  \psi  \searrow &  \bar \psi \downarrow & \swarrow \theta \\
 & &W &  \ \ \ \ \ \ . \end {array}$$

Now we show that $\theta$ is an algebra homomorphism, i.e.
 \begin{eqnarray*}  \theta(r\ast s)&=&
\theta(r) \theta (s) \end {eqnarray*} for  any $r, s \in B^*$. We
show this using induction by following several steps.

$(1^\circ)$ If $rs\in P,$ then $\theta(r\ast
s)=\theta(\lambda(rs))=\theta(rs)=\theta(r)\theta(s)$.

 $(2^\circ)$ $r, s \in B$ and $r\prec s$. See that  \begin{eqnarray*}
   \theta(r\ast s)&=&
\theta(\lambda
(rs))\\
&=&\theta ( \lambda (sr \chi (r,s) + [rs]))\\
&=&\theta ( \lambda (sr ))\chi (r,s) + \theta  (\lambda ([rs]))\\
&=&\theta ( \lambda (sr) )\chi (r,s) + \theta  ([rs]) \ \ \  ( \mbox
{ since the length of } [rs] <2 \mbox
{ and } \nu (sr) < \nu (rs) )\\
&=&\theta (\lambda (sr))\chi (r,s) + \theta  ([rs])\\
&=&\theta ( sr)\chi (r,s) + \theta  ([rs])\ \ \ \ ( \mbox
{ since } sr \in P )\\
&=&\theta ( rs) = \theta (r)\theta (s).
\end {eqnarray*}

$(3^\circ)$ If $r=ub,$ $s=cv, u,v\in B^{\ast}$, $b, c\in B, b\prec
c$, $uv\not=1$,  then  \begin{eqnarray*} \theta(r\ast
s)&&=\theta(\lambda (rs)) =
\chi(b,c)\theta(\lambda(ucbv))+\theta(\lambda(u[bc]v))\\
& &=\chi(b,c)\theta((uc) *(bv))+\theta((u[bc]) *v)\\
& &=\chi(b,c)\theta(uc)\theta(bv)+\theta(u[bc])\theta(v)  \ \ \ {
\mbox {(by induction hypothesis)}}\\
& &=\chi(b,c)\theta(u)\theta(cb)\theta(v)+\theta(u)\theta([bc])\theta(v)\\
& &=\theta(u)\theta(bc)\theta(v)\\
& &=\theta(u)\theta(b)\theta(c)\theta(v)\\
& &=\theta(r)\theta(s). \ \ \Box
\end{eqnarray*}


TITLE: Prove by induction that $n^2 < 2^n$ for all $n \geq 5$?
QUESTION [4 upvotes]: So far I have this:
First consider $n = 5$. In this case $(5)^2 < 2^5$, or $25 < 32$. So the inequality holds for $n = 5$.
Next, suppose that $n^2 < 2^n$ and $n \geq 5$. Now I have to prove that $(n+1)^2 < 2^{(n+1)}$.
So I started with $(n+1)^2 = n^2 + 2n + 1$. Because $n^2 < 2^n$ by the hypothesis, $n^2 + 2n + 1$ < $2^n + 2n + 1$. As far as I know, the only way I can get $2^{n+1}$ on the right side is to multiply it by $2$, but then I get $2^{n+1} + 4n + 2$ on the right side and don't know how to get rid of the $4n + 2$. Am I on the right track, or should I have gone a different route?

REPLY [0 votes]: First, we prove a simple lemma.
$$
\begin{align}
n & \gt 5\\
\implies n-1 &\gt 4\\
\implies (n-1)^2 &\gt 16 \gt 2 \\
\implies n^2 - 2n + 1 &\gt  2\\
\implies n^2 &\gt 2n +1\\
\end{align}
$$
Now, we start with our induction step.
$$
\begin{align}
n^2 &\lt 2^n \text{ From hypothesis}\\
\implies 2n^2 & \lt 2^{n+1}\\
\implies n^2 + n^2 &\lt 2^{n+1}\\
\implies n^2 + 2n + 1 &\lt 2^{n+1} (n^2 \gt 2n+1)\\
\implies (n+1)^2 &\lt 2^{n+1} \\
\end{align}$$


TITLE: Showing that two random variables are independent
QUESTION [1 upvotes]: I have the following problem:
Given two independent standard normal random variables, call them $X$ and $Y$, how can I show that $Z = X^2 + Y^2$ and $W=\frac{X}{Y}$ are also independent?
I know that because $X$ and $Y$ are standard normal I can write their distributions as $$f_X(x) = \frac{1}{2\pi}e^\frac{-(x)^2}{2}$$ $$f_Y(y) = \frac{1}{2\pi}e^\frac{-(y)^2}{2}$$
Then because they are independent I can write their joint probability distribution as $$f_{X,Y}(x,y) = \frac{1}{2\pi}e^\frac{-(x^+y^2)}{2}$$
Now I know that to show $Z$ and $W$ are independent, I need to show that their joint probability distribution is equal to the product of the marginal distribution functions. But I'm not sure how to find
$f_{Z,W}(z,w)$, $f_Z(z)$ and $f_W(w)$.
Any help is much appreciated.

REPLY [1 votes]: The joint distribution for $(X^2,Y^2)$ is
$$\frac{x^{-1/2}e^{-x/2}}{\sqrt{2}\Gamma(1/2)}1_{(0,+\infty)}(x)\times \frac{y^{-1/2}e^{-y/2}}{\sqrt{2}\Gamma(1/2)}1_{(0,+\infty)}(x)=\frac{(xy)^{-1/2}e^{-(x+y)/2}}{2(\Gamma(1/2))^2}1_{(0,+\infty)}(x)1_{(0,+\infty)}(y)$$
Since $X^2=Z-\frac{Z}{W^2+1}=\frac{ZW^2}{W^2+1},Y^2=\frac{Z}{W^2+1}$, the Jacobian matrix is $$
\left|\begin{array}{cc}
   \frac{W^2}{W^2+1}& \frac{1}{W^2+1}\\
    \frac{2ZW}{(W^2+1)^2}  & -\frac{2ZW}{(W^2+1)^2}
\end{array}\right| =\frac{2ZW}{(W^2+1)^2}
$$
Therefore, the joint pdf of $(Z,W)$ is
$$\frac{(\frac{ZW^2}{W^2+1}\frac{Z}{W^2+1})^{-1/2}e^{-(\frac{ZW^2}{W^2+1}+\frac{Z}{W^2+1})/2}}{2(\Gamma(1/2))^2}\times \frac{2ZW}{(W^2+1)^2}1_{(0,+\infty)}(z)=\frac{1}{w^2+1}\frac{e^{-z/2}}{\pi}1_{(0,+\infty)}(z).$$
Hence, the pdf of $W$ and $Z$ are $\frac{1}{\pi (1+w^2)}$ and $\frac{1}{2}e^{-z/2}1_{(0,+\infty)}(z)$.
For now, one can see the independence of $W$ and $Z$.


TITLE: Some weird "system" of inequalities in nonnegative integers.
QUESTION [5 upvotes]: Suppose I have a bunch of nonnegative integers $(a_{ijkl})_{1 \leq i \leq j \leq k \leq l \leq 17}$ such that for all 17-tuples nonnegative integers $w_t$ (for $1 \leq t \leq 17$) we have that $$\min_{1\leq i\leq j\leq k \leq l\leq 17}(a_{ijkl} + w_i + w_j + w_k+w_l) \leq \frac{4}{17}\sum_{1 \leq t \leq 17} w_t.$$ What can we say about the $a_{ijkl}$? Are they bounded? What are the optimal bounds? I would like to get as much information on the $a_{ijkl}$ as possible. This problem comes from a question in number theory I'm trying to answer, but as you can see, this has a smell of linear programming, of which I know nothing at all. Also, maybe some things can be done with a computer, but I'm not good with computers...
(EDIT) If you suppose moreover that for all $t$, at least one of the inequalities $a_{ijkl} \geq n$, where $n$ is the number of indices from $(i,j,k,l)$ which are equal to $t$ ($n \geq 1$), is false, can we get something more?
(MOTIVATION) This comes from a semistability condition in geometric invariant theory.

REPLY [7 votes]: Take $a_{iiii}=0$ for all $i=1,\dots,17$ and let the other $a$'s be arbitrary large. Then the inequality is satisfied.
Indeed, let $w_1, \dots, w_{17}$ be arbitrary nonnegative integers. Without loss of generality assume that
$$\min \{ w_1, \dots, w_{17} \} = w_1.$$
Then
$$\min_{1\leq i\leq j\leq k\leq l\leq 17} (a_{ijkl} + w_i + w_j + w_k + w_l) \leq a_{1111} + 4w_1 = 4w_1 \leq \frac{4}{17} \sum_{t=1}^{17} w_t$$
as required.
Hence, $a_{ijkl}$ are not bounded in general.


TITLE: Evaluating $\lim_{t\to\infty}\frac{1}{t}\int_{\mathbb{R}^{n}/B_{r_{0}}(0)}\frac{1}{|x|}dx$
QUESTION [0 upvotes]: I want to evaluate
$$\lim_{t\to\infty}\frac{1}{t}\int_{\mathbb{R}^{n}/B_{r_{0}}(0)}\frac{1}{|x|}dx.$$
Attempt
We have
$$\int_{\mathbb{R}^n/B_{r_0}(0)}\frac{1}{|x|}dx=\int_{r_{0}}^{\infty}r \, dr =\infty.$$
So I guess
$$\lim_{t\to\infty}\frac{1}{t} \int_{\mathbb{R}^{n}/B_{r_0}(0)}\frac{1}{|x|} \, dx =\lim_{t\to\infty} \frac{1}{t} \infty=\infty$$
and not $1$.
If so, I want to understand the intuition behind
$$\lim_{t\to\infty}\frac{1}{t}\int_{r_{0}}^{\infty}r=\infty.$$
One guess is that the limit of $\frac{\infty}{t}$ as $t\to \infty$ is still infinity because $\frac{\infty}{t}=\infty$ for all t.
Otherwise it is like saying $\frac{\infty}{2}>\frac{\infty}{3}$ which makes no sense.

REPLY [1 votes]: Note that for any $a$,
$$
\lim_{t \to a} \infty = \infty
$$
Your limit is simply the special case $a = \infty$.


TITLE: How is $\operatorname{Gal}(K^{nr}/K)$ isomorphic to $\operatorname{Gal}(\bar{k}/k)$?
QUESTION [4 upvotes]: Let $K$ be a local field complete with a discrete valuation.
In a book I am reading it states that $\operatorname{Gal}(K^{nr}/K)$ is isomorphic to $\operatorname{Gal}(\bar{k}/k)$, but I wasn't sure how this was true.
How does one see this? I would greatly appreciate any comments and suggestions. Thank you.

REPLY [3 votes]: There is a unique unramified extension $K_n/K$ of degree $n$ for each $n$ given by adjoining a $q^n-1^{th}$ root of unity to $K$, where $q$ is the size of the residue field $k$. In fact, each of these unramified extensions is a cyclic Galois extension where the reduction map Gal$(K_n/K) \to$ Gal$(k_n/k)$ is an isomorphism ($k_n$ is the residue field of $K_n$). Thus by taking limits, the union of the $k_n$ is $\bar{k}$ and the union of the $K_n$ is $K^{nr}$, so we get an isomorphism Gal$(K^{nr}/K) \cong$ Gal$(\bar{k}/k) \cong \lim_n \mathbb{Z}/n\mathbb{Z} =  \hat{\mathbb{Z}}$.
To prove the facts I have mentioned, one can use the Teichmüller character $\omega: k^\times \to \mathcal{O}_K^\times$, where $\mathcal{O}_K$ is the ring of integers. The Teichmüller character is given by $\omega(\bar{x}) = \lim_n x^{q^n}$, where $x$ is any lift of $\bar{x}$ in $\mathcal{O}_K$.
It is easy to see that $x^{q^n}$ is a Cauchy sequence, and the fact that $\omega(\bar{x})$ doesn't depend on $x$ follows from uniqueness in Hensel's lemma on the polynomial $x^{q-1}-1$. One writes $\omega(x)$ for $x \in \mathcal{O}_K$ to mean $\omega$ applied to the reduction of $x$.
Now the important fact about the Teichmüller character that we need is that if $\mu_K'$ denote the roots of unity of $K$ of order coprime to $q$, then $\mu_K' = \omega(k^\times).$ This follows from looking at the formula for $\omega$ and noting that $\omega$ fixes every element of $\mu_K'$.
Theorem There is a unique unramified extension of degree $n$ for each $n$ given by $K_n=K(\mu_{q^n-1})$, which is cyclic Galois. Moreover the natural map Gal$(K_n/K) \to$ Gal$(k_n/k)$ is an isomorphism.
Proof
Let $K_n = K(\mu_{q^n-1})$. Then $k_n$ contains $\mathbb{F}_{q^n}$ since by our fact about the Teichmüller character the residue field contains a $q^n-1^{th}$ root of unity. Let $\bar{g}$ be the minimal polynomial of $a$, a primitive $q^n-1^{th}$ root of unity in $k$, and let $g$ be a lift of $\bar{g}$. By Hensel's lemma, there is a unique root of $g$ in $K_n$ reducing to each conjugate of $a$. Letting $\alpha$ be the lift of $a$, we must have $K(\alpha) = K_n$, since $\omega(\alpha)$ is a primitive $q^n-1^{th}$ root of unity. Thus $n = [K_n:K] \geq [k_n:k] \geq n$, so equality must hold. Then if $\pi$ is a uniformizer of $K$, $[k_n:k] = [K_n:K] = [\mathcal{O}_{K_n}/\pi\mathcal{O}_{K_n}:\mathcal{O}_{K_n}/\pi\mathcal{O}_{K_n}]$, so $\pi\mathcal{O}_{K_n}$ is the maximal ideal of $\mathcal{O}_{K_n}$, so $\pi$ stays prime in $K_n$, and the extension is unramified.
Now $K_n$ contains all the conjugates of $\alpha$ so is Galois. Reduction mod the maximal ideal of $\mathcal{O}_{K_n}$ gives a homomorphism from Gal$(K_n/K)$ to Gal$(k_n/k)$, but since $\alpha$'s conjugates reduce to $a$'s conjugates, and Gal$(K_n/K),$ Gal$(k_n/k)$ act faithfully on the conjugates of $\alpha$ and $a$ respectively, the homomorphism is injective and hence an isomorphism. Thus $K_n$ is a cyclic extension.
For uniqueness, if $L$ is unramified degree $n$, let $\pi$ be as before, $n = [L:K] = [\mathcal{O}_{L}/\pi\mathcal{O}_{L}:\mathcal{O}_K/\pi\mathcal{O}_K] = [l:k]$.
Write $l = k(a)$, and since $\omega(a)$ is a $q^n-1^{th}$ root of unity, $L \supset K(\mu_{q^n-1})$, but they are the same degree, and hence are equal.
I hope this has made it more clear why unramified extensions of (non-archimedian) local fields are easy to understand. It turns out the totally ramified abelian extensions are also easy to understand, and are constructed via Lubin Tate theory.


TITLE: How to determine the direction of the normal of the plane
QUESTION [1 upvotes]: I have a triangle represented with three points in $3D$ space and a normal vector of that triangle. How can I determine if the normal vector (starting at $(0,0,0)$ ) is pointing towards or away from that triangle (or at least the plane that this triangle is laying on) ?

REPLY [2 votes]: Let $\mathbf n$ be your normal vector and $\mathbf p_0$ be one of the triangle’s vertices. For any point $\mathbf p$ on the triangle’s plane, we have $\mathbf n\cdot\mathbf p=\mathbf n\cdot\mathbf p_0$ (this is just a rearrangement of the point-normal form of the plane’s equation). We can use this to find the multiple of $\mathbf n$ that lies on the plane: setting $\mathbf p=\lambda\mathbf n$ and solving for $\lambda$ gives $\lambda = {\mathbf n\cdot\mathbf p_0\over\mathbf n\cdot\mathbf n}$. If this is positive, then we have to move in the direction of $\mathbf n$ to reach the plane from the origin, that is, $\mathbf n$ points “toward” the plane. Now, $\mathbf n\cdot\mathbf n$ is always positive, so the sign of $\lambda$ is entirely determined by $\mathbf n\cdot\mathbf p_0$.
So, compute the dot product of your normal with any of the triangle’s vertices and check the sign: if positive, the normal points towards the triangle’s plane, if negative, away from it, and if zero, the triangle’s plane passes through the origin and it’s neither. I write “the triangle’s plane” instead of “the triangle” because it’s quite possible that the line through the origin in the direction of the normal doesn’t intersect the triangle at all, in which case it only points “toward” the triangle in a loose sense.


text:
section \<open>Separation of Roots: Sturm\<close>

text \<open>We adapt the existing theory on Sturm's theorem to work on rational numbers instead of real
  numbers. The reason is that we want to implement real numbers as real algebraic numbers with the
  help of Sturm's theorem to separate the roots. To this end, we just copy the definitions of
  of the algorithms w.r.t. Sturm and let them be executed on rational numbers. We then
  prove that corresponds to a homomorphism and therefore can transfer the existing soundness results.\<close>

theory Sturm_Rat
imports
  Sturm_Sequences.Sturm_Theorem
  Algebraic_Numbers_Prelim
  Berlekamp_Zassenhaus.Square_Free_Int_To_Square_Free_GFp
begin

hide_const (open) UnivPoly.coeff

(* TODO: Move *)
lemma root_primitive_part [simp]:
  fixes p :: "'a :: {semiring_gcd, semiring_no_zero_divisors} poly"
  shows  "poly (primitive_part p) x = 0 \<longleftrightarrow> poly p x = 0"
proof(cases "p = 0")
  case True
  then show ?thesis by auto
next
  case False
  have "poly p x = content p * poly (primitive_part p) x"
    by (metis content_times_primitive_part poly_smult)
  also have "\<dots> = 0 \<longleftrightarrow> poly (primitive_part p) x = 0" by (simp add: False)
  finally show ?thesis by auto
qed

(*TODO: Move*)
lemma irreducible_primitive_part:
  assumes "irreducible p" and "degree p > 0"
  shows "primitive_part p = p"
  using irreducible_content[OF assms(1), unfolded primitive_iff_content_eq_1] assms(2)
  by (auto simp: primitive_part_def abs_poly_def)

subsection \<open>Interface for Separating Roots\<close>

text \<open>For a given rational polynomial, we need to know how many real roots are in a given closed interval,
  and how many real roots are in an interval $(-\infty,r]$.\<close>

datatype root_info = Root_Info (l_r: "rat \<Rightarrow> rat \<Rightarrow> nat") (number_root: "rat \<Rightarrow> nat")
hide_const (open) l_r
hide_const (open) number_root

definition count_roots_interval_sf :: "real poly \<Rightarrow> (real \<Rightarrow> real \<Rightarrow> nat) \<times> (real \<Rightarrow> nat)" where
  "count_roots_interval_sf p = (let ps = sturm_squarefree p
    in ((\<lambda> a b. sign_changes ps a - sign_changes ps b + (if poly p a = 0 then 1 else 0)),
       (\<lambda> a. sign_changes_neg_inf ps - sign_changes ps a)))"

definition count_roots_interval :: "real poly \<Rightarrow> (real \<Rightarrow> real \<Rightarrow> nat) \<times> (real \<Rightarrow> nat)" where
  "count_roots_interval p = (let ps = sturm p
    in ((\<lambda> a b. sign_changes ps a - sign_changes ps b + (if poly p a = 0 then 1 else 0)),
       (\<lambda> a. sign_changes_neg_inf ps - sign_changes ps a)))"

lemma count_roots_interval_iff: "square_free p \<Longrightarrow> count_roots_interval p = count_roots_interval_sf p"
  unfolding count_roots_interval_def count_roots_interval_sf_def sturm_squarefree_def
    square_free_iff_separable separable_def by (cases "p = 0", auto)

lemma count_roots_interval_sf: assumes p: "p \<noteq> 0"
  and cr: "count_roots_interval_sf p = (cr,nr)"
  shows "a \<le> b \<Longrightarrow> cr a b = (card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0})"
    "nr a = card {x. x \<le> a \<and> poly p x = 0}"
proof -
  have id: "a \<le> b \<Longrightarrow> { x. a \<le> x \<and> x \<le> b \<and> poly p x = 0} =
    { x. a < x \<and> x \<le> b \<and> poly p x = 0} \<union> (if poly p a = 0 then {a} else {})"
    (is "_ \<Longrightarrow> _ = ?R \<union> ?S") using not_less by force
  have RS: "finite ?R" "finite ?S" "?R \<inter> ?S = {}"  using p by (auto simp: poly_roots_finite)
  show "a \<le> b \<Longrightarrow> cr a b = (card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0})"
    "nr a = card {x. x \<le> a \<and> poly p x = 0}" using cr unfolding arg_cong[OF id, of card] card_Un_disjoint[OF RS]
    count_roots_interval_sf_def count_roots_between_correct[symmetric]
    count_roots_below_correct[symmetric] count_roots_below_def
    count_roots_between_def Let_def using p by auto
qed

lemma count_roots_interval: assumes cr: "count_roots_interval p = (cr,nr)"
  and sf: "square_free p"
  shows "a \<le> b \<Longrightarrow> cr a b = (card {x. a \<le> x \<and> x \<le> b \<and> poly p x = 0})"
    "nr a = card {x. x \<le> a \<and> poly p x = 0}"
  using count_roots_interval_sf[OF _ cr[unfolded count_roots_interval_iff[OF sf]]]
    sf[unfolded square_free_def] by blast+

definition root_cond :: "int poly \<times> rat \<times> rat \<Rightarrow> real \<Rightarrow> bool" where
  "root_cond plr x = (case plr of (p,l,r) \<Rightarrow> of_rat l \<le> x \<and> x \<le> of_rat r \<and> ipoly p x = 0)"

definition root_info_cond :: "root_info \<Rightarrow> int poly \<Rightarrow> bool" where
  "root_info_cond ri p \<equiv> (\<forall> a b. a \<le> b \<longrightarrow> root_info.l_r ri a b = card {x. root_cond (p,a,b) x})
    \<and> (\<forall> a. root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> ipoly p x = 0})"

lemma root_info_condD: "root_info_cond ri p \<Longrightarrow> a \<le> b \<Longrightarrow> root_info.l_r ri a b = card {x. root_cond (p,a,b) x}"
  "root_info_cond ri p \<Longrightarrow> root_info.number_root ri a = card {x. x \<le> real_of_rat a \<and> ipoly p x = 0}"
  unfolding root_info_cond_def by auto

definition count_roots_interval_sf_rat :: "int poly \<Rightarrow> root_info" where
  "count_roots_interval_sf_rat  p = (let pp = real_of_int_poly p;
    (cr,nr) = count_roots_interval_sf pp
  in Root_Info (\<lambda> a b. cr (of_rat a) (of_rat b)) (\<lambda> a. nr (of_rat a)))"

definition count_roots_interval_rat :: "int poly \<Rightarrow> root_info" where
  [code del]: "count_roots_interval_rat  p = (let pp = real_of_int_poly p;
    (cr,nr) = count_roots_interval pp
  in Root_Info (\<lambda> a b. cr (of_rat a) (of_rat b)) (\<lambda> a. nr (of_rat a)))"

definition count_roots_rat :: "int poly \<Rightarrow> nat" where
  [code del]: "count_roots_rat  p = (count_roots (real_of_int_poly p))"

lemma count_roots_interval_sf_rat: assumes p: "p \<noteq> 0"
  shows "root_info_cond (count_roots_interval_sf_rat p) p"
proof -
  let ?p = "real_of_int_poly p"
  let ?r = real_of_rat
  let ?ri = "count_roots_interval_sf_rat p"
  from p have p: "?p \<noteq> 0" by auto
  obtain cr nr where cr: "count_roots_interval_sf ?p = (cr,nr)" by force
  have "?ri = Root_Info (\<lambda>a b. cr (?r a) (?r b)) (\<lambda>a. nr (?r a))"
    unfolding count_roots_interval_sf_rat_def Let_def cr by auto
  hence id: "root_info.l_r ?ri = (\<lambda>a b. cr (?r a) (?r b))" "root_info.number_root ?ri = (\<lambda>a. nr (?r a))"
    by auto
  note cr = count_roots_interval_sf[OF p cr]
  show ?thesis unfolding root_info_cond_def id
  proof (intro conjI impI allI)
    fix a
    show "nr (?r a) = card {x. x \<le> (?r a) \<and> ipoly p x = 0}"
      using cr(2)[of "?r a"] by simp
  next
    fix a b :: rat
    assume ab: "a \<le> b"
    from ab have ab: "?r a \<le> ?r b" by (simp add: of_rat_less_eq)
    from cr(1)[OF this] show "cr (?r a) (?r b) = card (Collect (root_cond (p, a, b)))"
      unfolding root_cond_def[abs_def] split by simp
  qed
qed

lemma of_rat_of_int_poly: "map_poly of_rat (of_int_poly p) = of_int_poly p"
  by (subst map_poly_map_poly, auto simp: o_def)

lemma square_free_of_int_poly: assumes "square_free p"
  shows "square_free (of_int_poly p :: 'a :: {field_gcd, field_char_0} poly)"
proof -
  have "square_free (map_poly of_rat (of_int_poly p) :: 'a poly)"
    unfolding of_rat_hom.square_free_map_poly by (rule square_free_int_rat[OF assms])
  thus ?thesis unfolding of_rat_of_int_poly .
qed

lemma count_roots_interval_rat: assumes sf: "square_free p"
  shows "root_info_cond (count_roots_interval_rat p) p"
proof -
  from sf have sf: "square_free (real_of_int_poly p)" by (rule square_free_of_int_poly)
  from sf have p: "p \<noteq> 0" unfolding square_free_def by auto
  show ?thesis
  using count_roots_interval_sf_rat[OF p]
  unfolding count_roots_interval_rat_def count_roots_interval_sf_rat_def
    Let_def count_roots_interval_iff[OF sf] .
qed

lemma count_roots_rat: "count_roots_rat p = card {x. ipoly p x = (0 :: real)}"
  unfolding count_roots_rat_def count_roots_correct ..

subsection \<open>Implementing Sturm on Rational Polynomials\<close>

function sturm_aux_rat where
"sturm_aux_rat (p :: rat poly) q =
    (if degree q = 0 then [p,q] else p # sturm_aux_rat q (-(p mod q)))"
  by (pat_completeness, simp_all)
termination by (relation "measure (degree \<circ> snd)",
                simp_all add: o_def degree_mod_less')

lemma sturm_aux_rat: "sturm_aux (real_of_rat_poly p) (real_of_rat_poly q) =
  map real_of_rat_poly (sturm_aux_rat p q)"
proof (induct p q rule: sturm_aux_rat.induct)
  case (1 p q)
  interpret map_poly_inj_idom_hom of_rat..
  note deg = of_int_hom.degree_map_poly_hom
  show ?case
    unfolding sturm_aux.simps[of "real_of_rat_poly p"] sturm_aux_rat.simps[of p]
    using 1 by (cases "degree q = 0"; simp add: hom_distribs)
qed

definition sturm_rat where "sturm_rat p = sturm_aux_rat p (pderiv p)"

lemma sturm_rat: "sturm (real_of_rat_poly p) = map real_of_rat_poly (sturm_rat p)"
  unfolding sturm_rat_def sturm_def
  apply (fold of_rat_hom.map_poly_pderiv)
  unfolding sturm_aux_rat..

definition poly_number_rootat :: "rat poly \<Rightarrow> rat" where
  "poly_number_rootat p \<equiv> sgn (coeff p (degree p))"

definition poly_neg_number_rootat :: "rat poly \<Rightarrow> rat" where
  "poly_neg_number_rootat p \<equiv> if even (degree p) then sgn (coeff p (degree p))
                                       else -sgn (coeff p (degree p))"

lemma poly_number_rootat: "poly_inf (real_of_rat_poly p) = real_of_rat (poly_number_rootat p)"
  unfolding poly_inf_def poly_number_rootat_def of_int_hom.degree_map_poly_hom of_rat_hom.coeff_map_poly_hom
    real_of_rat_sgn by simp

lemma poly_neg_number_rootat: "poly_neg_inf (real_of_rat_poly p) = real_of_rat (poly_neg_number_rootat p)"
  unfolding poly_neg_inf_def poly_neg_number_rootat_def of_int_hom.degree_map_poly_hom of_rat_hom.coeff_map_poly_hom
    real_of_rat_sgn by (simp add:hom_distribs)

definition sign_changes_rat where
"sign_changes_rat ps (x::rat) =
    length (remdups_adj (filter (\<lambda>x. x \<noteq> 0) (map (\<lambda>p. sgn (poly p x)) ps))) - 1"

definition sign_changes_number_rootat where
  "sign_changes_number_rootat ps =
    length (remdups_adj (filter (\<lambda>x. x \<noteq> 0) (map poly_number_rootat ps))) - 1"

definition sign_changes_neg_number_rootat where
  "sign_changes_neg_number_rootat ps =
      length (remdups_adj (filter (\<lambda>x. x \<noteq> 0) (map poly_neg_number_rootat ps))) - 1"

lemma real_of_rat_list_neq: "list_neq (map real_of_rat xs) 0
  = map real_of_rat (list_neq xs 0)"
  by (induct xs, auto)

lemma real_of_rat_remdups_adj: "remdups_adj (map real_of_rat xs) = map real_of_rat (remdups_adj xs)"
  by (induct xs rule: remdups_adj.induct, auto)

lemma sign_changes_rat: "sign_changes (map real_of_rat_poly ps) (real_of_rat x)
  = sign_changes_rat ps x" (is "?l = ?r")
proof -
  define xs where "xs = list_neq (map (\<lambda>p. sgn (poly p x)) ps) 0"
  have "?l = length (remdups_adj (list_neq (map real_of_rat (map (\<lambda>xa.  (sgn (poly xa x))) ps)) 0)) - 1"
    by (simp add: sign_changes_def real_of_rat_sgn o_def)
  also have "\<dots> = ?r" unfolding sign_changes_rat_def real_of_rat_list_neq
    unfolding real_of_rat_remdups_adj by simp
  finally show ?thesis .
qed

lemma sign_changes_neg_number_rootat: "sign_changes_neg_inf (map real_of_rat_poly ps)
  =  sign_changes_neg_number_rootat ps" (is "?l = ?r")
proof -
  have "?l = length (remdups_adj (list_neq (map real_of_rat (map poly_neg_number_rootat ps)) 0)) - 1"
    by (simp add: sign_changes_neg_inf_def o_def real_of_rat_sgn poly_neg_number_rootat)
  also have "\<dots> = ?r" unfolding sign_changes_neg_number_rootat_def real_of_rat_list_neq
    unfolding real_of_rat_remdups_adj by simp
  finally show ?thesis .
qed

lemma sign_changes_number_rootat: "sign_changes_inf (map real_of_rat_poly ps)
  =  sign_changes_number_rootat ps" (is "?l = ?r")
proof -
  have "?l = length (remdups_adj (list_neq (map real_of_rat (map poly_number_rootat ps)) 0)) - 1"
    unfolding sign_changes_inf_def
    unfolding map_map o_def real_of_rat_sgn poly_number_rootat ..
  also have "\<dots> = ?r" unfolding sign_changes_number_rootat_def real_of_rat_list_neq
    unfolding real_of_rat_remdups_adj by simp
  finally show ?thesis .
qed

lemma count_roots_interval_rat_code[code]:
  "count_roots_interval_rat p = (let rp = map_poly rat_of_int p; ps = sturm_rat rp
    in Root_Info
      (\<lambda> a b. sign_changes_rat ps a - sign_changes_rat ps b + (if poly rp a = 0 then 1 else 0))
      (\<lambda> a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a))"
  unfolding count_roots_interval_rat_def Let_def count_roots_interval_def split of_rat_of_int_poly[symmetric, where 'a = real]
    sturm_rat sign_changes_rat
    by (simp add: sign_changes_neg_number_rootat)

lemma count_roots_rat_code[code]:
  "count_roots_rat p = (let rp = map_poly rat_of_int p in if p = 0 then 0 else let ps = sturm_rat rp
    in sign_changes_neg_number_rootat ps - sign_changes_number_rootat ps)"
  unfolding count_roots_rat_def Let_def sturm_rat count_roots_code of_rat_of_int_poly[symmetric, where 'a = real]
    sign_changes_neg_number_rootat sign_changes_number_rootat
  by simp

hide_const (open) count_roots_interval_sf_rat

text \<open>Finally we provide an even more efficient implementation which
  avoids the "poly p x = 0" test, but it is restricted to irreducible polynomials.\<close>

definition root_info :: "int poly \<Rightarrow> root_info" where
  "root_info p = (if degree p = 1 then
    (let x = Rat.Fract (- coeff p 0) (coeff p 1)
     in Root_Info (\<lambda> l r. if l \<le> x \<and> x \<le> r then 1 else 0)  (\<lambda> b. if x \<le> b then 1 else 0)) else
    (let rp = map_poly rat_of_int p; ps = sturm_rat rp in
   Root_Info (\<lambda> a b. sign_changes_rat ps a - sign_changes_rat ps b)
      (\<lambda> a. sign_changes_neg_number_rootat ps - sign_changes_rat ps a)))"

lemma root_info:
  assumes irr: "irreducible p" and deg: "degree p > 0"
  shows "root_info_cond (root_info p) p"
proof (cases "degree p = 1")
  case deg: True
  from degree1_coeffs[OF this] obtain a b where p: "p = [:b,a:]" and "a \<noteq> 0" by auto
  from deg have "degree (real_of_int_poly p) = 1" by simp
  from roots1[OF this, unfolded roots1_def] p
  have id: "(ipoly p x = 0) = ((x :: real) = - b / a)" for x by auto
  have idd: "{x. real_of_rat aa \<le> x \<and>
                 x \<le> real_of_rat ba \<and> x = real_of_int (- b) / real_of_int a}
   = (if real_of_rat aa \<le> real_of_int (- b) / real_of_int a \<and>
                 real_of_int (- b) / real_of_int a \<le> real_of_rat ba then {real_of_int (- b) / real_of_int a} else {})"
    for aa ba by auto
  have iddd: "{x. x \<le> real_of_rat aa \<and> x = real_of_int (- b) / real_of_int a}
    = (if real_of_int (- b) / real_of_int a \<le> real_of_rat aa then {real_of_int (- b) / real_of_int a} else {})" for aa
    by auto
  have id4: "real_of_int x = real_of_rat (rat_of_int x)" for x by simp
  show ?thesis unfolding root_info_def deg unfolding root_info_cond_def id root_cond_def split
    unfolding p Fract_of_int_quotient Let_def idd iddd
    unfolding id4 of_rat_divide[symmetric] of_rat_less_eq by auto
next
  case False
  have irr_d: "irreducible\<^sub>d p" by (simp add: deg irr irreducible_connect_rev)
  from irreducible\<^sub>d_int_rat[OF this]
  have "irreducible (of_int_poly p :: rat poly)" by auto
  from irreducible_root_free[OF this]
  have idd: "(poly (of_int_poly p) a = 0) = False" for a :: rat
    unfolding root_free_def using False by auto
  have id: "root_info p = count_roots_interval_rat p"
    unfolding root_info_def if_False count_roots_interval_rat_code Let_def idd using False by auto
  show ?thesis unfolding id
    by (rule count_roots_interval_rat[OF irreducible\<^sub>d_square_free[OF irr_d]])
qed

end

subset_name: curated


TITLE: $\subset$ vs $\subseteq$ when *not* referring to strict inclusion
QUESTION [11 upvotes]: Inspired by the confusion in the comments on this question:
I always thought that the standard was to read $\subset$ as "is a strict subset of", and $\subseteq$ could mean proper or improper inclusion.
Was I wrong?

REPLY [1 votes]: My convention has always been $\subset$ is strict and that $\subseteq$ is nonstrict.  This maintains parallelism with $<$ and $\le$.
I have seen $\subset\subset$ in the comments. I have seen it used in this context.
Write $K\subset\subset G$, when $K$ is compact and $G$ is open.


TITLE: Can a functor be seen as a special case of a profunctor?
QUESTION [7 upvotes]: This is a conceptual question about category theory, more than a technical one. It has no practical purpose as far as I know, but it's been bugging me for ages.
The short version: a function can be seen as a special case of a relation, namely one in which every object in the domain is related to exactly one object in the codomain. Functors don't seem to be special cases of profunctors in the same sense. Is there some other, somewhat analogous, sense in which a functor can be seen as a special case of a profunctor?
The long version:
A profunctor can be seen as a particular type of functor: a profunctor $\phi\colon A\nrightarrow B$ is a functor $\phi\colon A^\text{op}\times B \to \mathbf{Set}$. (There seem to be multiple conventions about the order of $A$ and $B$ and where to put the ${}^\text{op}$. I'm using this one.) For objects $a\in\mathrm{Ob}(A), b\in\mathrm{Ob}(B)$, one can think of $\phi(a,b)$ as something like a hom-set between $a$ and $b$, even though they're in different categories. The elements of $\phi(a,b)$ are sometimes called "heteromorphisms." The functoriality of $\phi$ essentially means that these heteromorphisms have to compose with the (homo)morphisms in the categories $A$ and $B$.
This leads to the view that profunctors are to functors as relations are to functions. We can think of a relation $R$ between sets $S$ and $T$ as a function $R:S\times T\to \{0,1\}$, which corresponds to the definition of a profunctor as a functor, and the definition of a profunctor can be seen as a categorification of this.
We can also think of $R$ as just a subset of the Cartesian product $S\times T$. The picture of profunctors in terms of heteromorphisms can be seen as a categorification of this view. From this view, we can also see a function as a special case of a relation: it's a relation in which every object in $S$ is related to exactly one object in $T$.
However, at this point the profunctors$\leftrightarrow$relations analogy seems to break down. It would be very nice if we could say, analogously, that a functor $F\colon A\to B$ is a profunctor in which every object of $A$ is related to exactly one object of $B$. However, it seems this can't work. Consider the following example:

If we want to express a functor that maps $a\in\mathrm{Ob}(A)$ to $b_1\in \mathrm{Ob}(B)$ then we should draw a heteromorphism $h$ from $a$ to $b_1$. But since heteromorphisms must compose with morphisms we are forced to also add a heteromorphism $h{;}f$, contradicting the idea that $a$ should be related to exactly one object in $B$.
The question is, is there some other way in which a functor can be seen as a special case of a profunctor, analogous to the way in which a function can be seen as a special case of a relation? If someone for some reason knew about profunctors (via the heteromorphism definiton) but didn't know what a functor was, could you given them a "categorical" definition of a functor in terms of profunctors?

REPLY [2 votes]: Your insight is correct:
Given a functor $F:A\to B$, we can define a category by freely adjoining 'base heteromorphisms' $a\to F(a)$ to the disjoint union $A\sqcup B$, while enforcing the squares $\ \matrix{\quad a&\to&F(a)\qquad \\ \alpha\downarrow && \downarrow F(\alpha) \\ \quad x& \to &F(x)\qquad}\ $ to commute.
Observe that this just leads to the collage category of the profunctor $F_*=(a,b)\mapsto \hom_B(F(a),\,b)$, and that by construction, every base heteromorphism is a reflection arrow.
Dually, if we swap the direction of the base heteromorphisms but do the same construction, we'll arrive to a profunctor $B\not\to A$, namely $F^*=(b,a)\mapsto\hom_B(b,\,F(a))$ and the base heteromorphisms will be coreflection arrows.
Assuming the axiom of choice, the converse statements also hold:
If $B$ is a reflective subcategory of (the collage of) a profunctor $U:A\not\to B$, then $U\cong F_*$ for some functor $F:A\to B$ (namely, fix a reflection arrow for each object in $A$ and take their codomains).
If $A$ is a coreflective subcategory of the collage of $U$, then $U\cong G^*$ for some functor $G:B\to A$.
Moreover, if both happens, that means exactly that the profunctor itself is [or, encodes] an adjunction, namely $F\dashv G$.


TITLE: A criterion for independence based on Characteristic function
QUESTION [14 upvotes]: Let $X$ and $Y$ be real-valued random variables defined on the same space.  Let's use $\phi_X$ to denote the characteristic function of $X$.  If $\phi_{X+Y}=\phi_X\phi_Y$ then must $X$ and $Y$ be independent?

REPLY [23 votes]: As user75064 already pointed out, the answer is "no". However, there is the following result:

Let $X,Y$ be $\mathbb{R}^d$-valued random variables. Then the following statements are equivalent.

$X,Y$ are independent
$\forall \eta,\xi \in \mathbb{R}^d: \mathbb{E}e^{\imath \, (X,Y) \cdot (\xi,\eta)} = \mathbb{E}e^{\imath \, X \cdot \xi} \cdot \mathbb{E}e^{\imath \, Y \cdot \eta}$

i.e. if the characteristic function of the random vector $(X,Y)$ equals the product of the characteristic function of $X$ and $Y$, then $X$ and $Y$ are independent (proof).