text:
\begin{document}

\title{A Zero-attracting Quaternion-valued Least Mean Square Algorithm for Sparse System Identification}

\author{\IEEEauthorblockN{Mengdi Jiang, Wei Liu}
\IEEEauthorblockA{Communications Research Group\\ Department of
Electronic and Electrical Engineering\\ University of Sheffield,
UK\\\{mjiang3, w.liu\}@sheffield.ac.uk} \and \IEEEauthorblockN{Yi Li}
\IEEEauthorblockA{School of Mathematics and Statistics\\ University of Sheffield, S3 7RH
UK\\yili@sheffield.ac.uk}\thanks{This work is partially funded by National Grid, UK and will appear in the Proc. of the 9th International Symposium on Communication Systems, Networks and Digital Signal Processing (CSNDSP), Manchester, UK, July 2014 (submitted in March 2014 and accepted on 18 April 2014).}}

\maketitle

\begin{abstract}
Recently, quaternion-valued signal processing has received more and more attention. In this paper, the quaternion-valued sparse system identification problem is studied for the first time and a zero-attracting quaternion-valued least mean square (LMS) algorithm is derived by considering the $l_1$ norm of the quaternion-valued adaptive weight vector. By incorporating the sparsity information of the system into the update process, a faster convergence speed is achieved, as verified by simulation results.
\end{abstract}

{\bf \it Keywords:} quaternion; sparsity; system identification; adaptive filtering; LMS algorithm.

\IEEEpeerreviewmaketitle

\section{Introduction}\label{sec:introduction}

In adaptive filtering~\cite{haykin96a}, there is a class of algorithms specifically designed for sparse system identification, where the unknown system only has a few large  coefficients while the remaining ones have a very small amplitude so that they can be ignored without significant effect on the overall performance of the system. A good example of them is the zero-attracting least mean square (ZA-LMS) algorithm proposed in~\cite{chen09b}. This algorithm can achieve a higher convergence speed, and meanwhile, reduce the steady state excess mean square error (MSE). Compared to the classic LMS algorithm~\cite{widrow75a}, the ZA-LMS algorithm introduces an $l_1$ norm in its cost function, which modifies the weight vector update equation with a zero attractor term.

Recently, the hypercomplex concepts have been introduced to solve problems related to three or four-dimensional
signals~\cite{BihanN2004}, such as vector-sensor array signal processing~\cite{zhang13a,liu14e,liu14k}, color image processing~\cite{pei99a} and wind profile prediction~\cite{took09a,liu13j}. As quaternion-valued algorithms can be regarded as an extension of the
complex-valued ones, the adaptive filtering algorithms in complex domain could be extended to the quaternion
domain as well, such as the quaternion-valued LMS (QLMS) algorithm in~\cite{liu14f}.

In this paper, we propose a novel quaternion-valued adaptive algorithm with a sparsity constraint, which is called zero-attracting QLMS (ZA-QLMS) algorithm. The additional constraint is formulated based on the $l_1$ norm. Both the QLMS and ZA-QLMS algorithms can identify an unknown sparse system effectively. However,  a better performance in terms of convergence speed  is achieved by the latter one.

This paper is organized as follows. A review of basic operations in the quaternion domain is provided in Section \ref{sec:quaternion_basic} to facilitate the following derivation of the ZA-QLMS algorithm. The proposed ZA-QLMS algorithm is derived  in Section \ref{sec:ZA-QLMS}. Simulation results are given in Section \ref{sec:simulations}, and conclusions are drawn in Section \ref{sec:conclusions}.

\section{Quaternion-valued Adaptive Filtering}\label{sec:quaternion_basic}

\subsection{Basics of Quaternion}
Quaternion is a non-commutative extension of the complex number, and normally a quaternion consists of one real part and three imaginary parts, denoted by subscripts $a$, $b$, $c$ and $d$, respectively.

For a quaternion number $q$, it can be described as
\begin{equation}
q=q_{a} + (q_{b}i + q_{c}j + q_{d}k),
\label{eq:quaternion}
\end{equation}
where $q_{a}$, $q_{b}$, $q_{c}$, and $q_{d}$ are real-valued~\cite{hamilton1866a,kantor1989a}. For a quaternion, when its real part is zero, it becomes a pure quaternion. In this paper, we consider the conjugate operator of $q$ as $q^{*}=q_a-q_{b}i-q_{c}j-q_{d}k$. The three imaginary units $i$, $j$,  and $k$ satisfy
\begin{eqnarray}
ij=k,~jk=i,~ki=j,\nonumber\\
ijk=i^{2} = j^{2} = k^{2} = -1.
\label{eq:property}
\end{eqnarray}

As a quaternion has the noncommutativity property, in multiplication, the exchange of any two elements in their order will give a different result. For example, we have $ji=-ij$ rather than $ji=ij$.

\subsection{Differentiation with Respect to a Quaternion-valued Vector}\label{sec:Differentiation to a quaternion-valued vector}

To derive the quaternion-valued adaptive algorithm, the starting point is
the general operation of differentiation with respect to a quaternion-valued vector.

At first, we need to give
the definition of differentiation with respect to a quaternion $q$ and its conjugate $q^{*}$. Assume that $f(q)$ is a function of the quaternion variable $q$,
which is expressed as
\begin{equation}
f(q)=f_{a} + f_{b}i + f_{c}j + f_{d}k
\end{equation}
where $f(q)$ is in general quaternion-valued. The definition of $\dfrac{d f(q)}{d q}$ can be expressed as~\cite{mandic2011a,liu14f}
\begin{equation}
\dfrac{d f(q)}{d q}=\frac{1}{4}(\displaystyle\frac{\partial{f(q)}}{\partial q_a}-\displaystyle\frac{\partial{f(q)}}{\partial q_b} i-\displaystyle\frac{\partial{f(q)}}{\partial q_c} j- \displaystyle\frac{\partial{f(q)}}{\partial q_d} k)\;.
\label{eq:general_definition}
\end{equation}

The derivative of $f(q)$ with respect to $q^{*}$ can be defined in a similar way
\begin{equation}
\dfrac{d f(q)}{d q^{*}}=\frac{1}{4}(\displaystyle\frac{\partial{f(q)}}{\partial q_a}+\displaystyle\frac{\partial{f(q)}}{\partial q_b} i+\displaystyle\frac{\partial{f(q)}}{\partial q_c} j+ \displaystyle\frac{\partial{f(q)}}{\partial q_d} k)\;.
\label{eq:conj_general_definition}
\end{equation}

With this definition, we can easily obtain
\begin{equation}
 \frac{\partial q}{\partial q}=1,~\frac{\partial q}{\partial q^{*}}=-\frac{1}{2}\;.
 \end{equation}

Some product rules can be obtained from above formulations, such as the differentiation of quaternion-valued functions to real variables.

Suppose $f(q)$ and $g(q)$ are two quaternion-valued functions of the quaternion variable $q$, and $q_a$ is the real variable. Then we can have the following result
\begin{eqnarray}
\frac{\partial f(q)g(q)}{\partial q_a}&=&\frac{\partial }{\partial q_a}(f_a+if_b+jf_c+kf_d)g\nonumber\\
&=&\frac{\partial f_a g}{\partial q_a}+i\frac{\partial f_b g}{\partial q_a}+j\frac{\partial f_c g}{\partial q_a}+k\frac{\partial f_d g}{\partial q_a}\nonumber\\
&=&(f_a\frac{\partial g}{\partial q_a}+\frac{\partial f_a}{\partial q_a}g)+i(f_b\frac{\partial g}{\partial q_a}+\frac{\partial f_b}{\partial q_a}g)\nonumber\\
&~&+j(f_c\frac{\partial g}{\partial q_a}+\frac{\partial f_c}{\partial q_a}g)+k(f_d\frac{\partial g}{\partial q_a}+\frac{\partial f_d}{\partial q_a}g)\nonumber\\
&=&(f_a+if_b+jf_c+kf_d)\frac{\partial g}{\partial q_a}\nonumber\\
&~&+(\frac{\partial f_a}{\partial q_a}+i\frac{\partial f_b}{\partial q_a}+j\frac{\partial f_c}{\partial q_a}+k\frac{\partial f_d}{\partial q_a})g\nonumber\\
&=&f(q)\frac{\partial g(q)}{\partial q_a}+\frac{\partial f(q)}{\partial q_a} g(q)
\end{eqnarray}

When the quaternion variable $q$ is replaced by a quaternion-valued vector $\textbf{w}$, given by
\begin{equation}
\textbf{w} = [w_1~w_2~\cdots~w_{M}]^{T}
\end{equation}
where $w_m = a_m+b_mi+c_mj+d_mk$, $m=1,...,M$, the differentiation of the function $f(\textbf{w})$ with respect to the vector $\textbf{w}$ can be derived using a combination of (\ref{eq:general_definition}) straightforwardly in the following
\begin{eqnarray}
\dfrac{\partial f}{\partial \textbf{w}}=\frac{1}{4}\left[\begin{matrix}
              \dfrac{\partial f}{\partial a_0}-\dfrac{\partial f}{\partial b_0} i-\dfrac{\partial f}{\partial c_0} j-\dfrac{\partial f}{\partial d_0} k\\
              \dfrac{\partial f}{\partial a_1}-i\dfrac{\partial f}{\partial b_1} i-\dfrac{\partial f}{\partial c_1} j-\dfrac{\partial f}{\partial d_1} k\\
              \vdots \\
              \dfrac{\partial f}{\partial a_{M-1}}-\dfrac{\partial f}{\partial b_{M-1}} i-\dfrac{\partial f}{\partial c_{M-1}} j-\dfrac{\partial f}{\partial d_{M-1}} k
             \end{matrix}\right]
\label{eq:vector_definition}
\end{eqnarray}
Similarly, we define $\dfrac{\partial f}{\partial \textbf{w}^{*}}$ as
\begin{eqnarray}
\dfrac{\partial f}{\partial \textbf{w}^{*}}=\frac{1}{4}\left[\begin{matrix}
              \dfrac{\partial f}{\partial a_0}+\dfrac{\partial f}{\partial b_0} i+\dfrac{\partial f}{\partial c_0} j+\dfrac{\partial f}{\partial d_0} k\\
              \dfrac{\partial f}{\partial a_1}+\dfrac{\partial f}{\partial b_1} i+\dfrac{\partial f}{\partial c_1} j+\dfrac{\partial f}{\partial d_1} k\\
              \vdots \\
              \dfrac{\partial f}{\partial a_{M-1}}+\dfrac{\partial f}{\partial b_{M-1}} i+\dfrac{\partial f}{\partial c_{M-1}} j+ \dfrac{\partial f}{\partial d_{M-1}} k
             \end{matrix}\right]
\label{eq:conj_vector_definition}
\end{eqnarray}
Obviously, when $M=1$, (\ref{eq:vector_definition}) and (\ref{eq:conj_vector_definition}) are reduced to (\ref{eq:general_definition}) and (\ref{eq:conj_general_definition}), respectively.

\section{The Zero-attracting QLMS (ZA-QLMS) Algorithm}\label{sec:ZA-QLMS}

To improve the performance of the LMS algorithm for sparse system identification, the ZA-QLMS algorithm is derived in this section. To achieve this, similar to \cite{chen09b}, in the cost function, we add an $l_1$ norm penalty
term for the quaternion-valued weight vector $\textbf{w}[n]$.

For a standard adaptive filter, the output $y[n]$ and error $e[n]$ can be expressed as
\begin{eqnarray}
y[n]&=&{\textbf{w}^{T}[n]}{\textbf{x}[n]}\\
e[n]&=&d[n]-{\textbf{w}^{T}[n]}{\textbf{x}[n]},
\end{eqnarray}
where $\textbf{w}[n]$ is the adaptive weight vector with a length of $L$, $d[n]$ is the reference signal, $\textbf{x}[n]=[x[n-1], \cdots, x[n-L]]^{T}$ is the input sample vector, and $\{\cdot\}^{T}$ denotes the transpose operation. Moreover, the conjugate form $\textbf{e}^{*}[n]$ of the error signal $e[n]$ is given by
\begin{equation}
e^{*}[n]=d^{*}[n]-{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]},
\end{equation}

Our proposed cost function with a zero attractor term is given by
\begin{equation}
J_0[n]=e[n]e^{*}[n]+\gamma{\|\textbf{w}[n]\|}_1\;,
\end{equation}
where $\gamma$ is a small constant.

The gradient of the above cost function with respect to $\textbf{w}^{*}[n]$ and $\textbf{w}[n]$ can be respectively expressed as
\begin{equation}
\nabla_{\textbf{w}^{*}}J_0[n]=\frac{\partial {J_0[n]}}{\partial \textbf{w}^{*}}
\label{eq:conj_gradient_cost_function}
\end{equation}
and
\begin{equation}
\nabla_{\textbf{w}}J_0[n]=\frac{\partial {J_0[n]}}{\partial \textbf{w}}
\label{eq:gradient_cost_function}
\end{equation}

From~\cite{mandic2011a,brandwood83a}, we know that
the conjugate gradient gives the maximum steepness direction for the optimization surface.
Therefore, the conjugate gradient $\nabla_{\textbf{w}^{*}}J_0[n]$ will be used to derive the update of the
coefficient weight vector.

Expanding the cost function, we obtain
\begin{eqnarray}
J_0[n]&=&e[n]e^{*}[n]+\gamma{\|\textbf{w}[n]\|}_1\nonumber\\
&=&d[n]d^{*}[n]-d[n]{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]}-{\textbf{w}^{T}[n]} {\textbf{x}[n]}d^{*}[n]\nonumber\\
&~&+{\textbf{w}^{T}[n]} {\textbf{x}[n]}{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]}+\gamma{\|\textbf{w}[n]\|}_1\;.
\label{eq:extended_cost_function}
\end{eqnarray}
Furthermore,
\begin{eqnarray}
\frac{\partial {J_0[n]}}{\partial \textbf{w}^{*}}&=&\frac{\partial {(e[n]e^{*}[n]+\gamma{\|\textbf{w}[n]\|}_1)}}{\partial \textbf{w}^{*}}\nonumber\\
&=&\frac{\partial}{\partial \textbf{w}^{*}}(d[n]d^{*}[n]-d[n]{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]}\nonumber\\
&&-{\textbf{w}^{T}[n]} {\textbf{x}[n]}d^{*}[n]+{\textbf{w}^{T}[n]} {\textbf{x}[n]}{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]})\nonumber\\
&&+\frac{\partial ({\gamma{\|\textbf{w}[n]\|}_1})}{\partial \textbf{w}^{*}}\;.
\label{eq:extended_gradient_cost_function}
\end{eqnarray}

Details of the derivation process for the gradient are shown in the following
\begin{equation}
\frac {\partial (d[n]d^{*}[n])}{\partial {\textbf{w}^{*}[n]}} = 0
\label{eq:part_1}
\end{equation}
\begin{equation}
\frac {\partial (d[n]{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]})}{\partial {\textbf{w}^{*}[n]}} = d[n]\textbf{x}^{*}[n]
\label{eq:part_2}
\end{equation}
\begin{equation}
\frac {\partial ({\textbf{w}^{T}[n]}{\textbf{x}[n]}d^{*}[n])}{\partial {\textbf{w}^{*}[n]}} = -\frac{1}{2}d[n]\textbf{x}^{*}[n]
\label{eq:part_3}
\end{equation}
\begin{equation}
\frac{\partial({\textbf{w}^{T}[n]} {\textbf{x}[n]}{\textbf{x}^{H}[n]}{\textbf{w}^{*}[n]})}{\partial {\textbf{w}^{*}[n]}}=\frac{1}{2}{\textbf{w}^{T}[n]}{\textbf{x}[n]}{\textbf{x}^{*}[n]}.
\label{eq:part_4}
\end{equation}
Moreover, the last part of the gradient of cost function is given by
 \begin{equation}
\frac{\partial ({\gamma{\|\textbf{w}[n]\|}_1})}{\partial \textbf{w}^{*}} = \frac{1}{4} \gamma\cdot{sgn(\textbf{w}[n])}\;,
\label{eq:part_5}
\end{equation}
where the symbol $sgn$  is a component-wise sign function that is defined as~\cite{chen09b}
\[
  sgn(x) =
   \begin{cases}
    x/|x| &  x\neq0 \\
    0      &  x = 0
   \end{cases}
 \]

Combining the above results,  the final gradient can be obtained as follows
\begin{equation}
\nabla_{\textbf{w}^{*}}J_0[n]=-\frac{1}{2}e[n]\textbf{x}^{*}[n]+\frac{1}{4}\gamma\cdot{sgn(\textbf{w}[n])}\;.
\end{equation}

With the general update equation for the weight vector
\begin{equation}
\textbf{w}[n+1] = \textbf{w}[n]-\mu \nabla_{\textbf{w}^{*}}J_0[n],
\end{equation}
where $\mu$ is the step size, we arrive at the following update equation for the proposed ZA-QLMS algorithm
\begin{equation}
\textbf{w}[n+1] = \textbf{w}[n]+\mu(e[n]\textbf{x}^{*}[n])-\rho\cdot{sgn(\textbf{w}[n])}\;,
\label{eq:update_weight_vector}
\end{equation}
where  $\rho = \mu \gamma$. The last term represents the zero attractor, which enforces the near-zero coefficients to zero and therefore accelerates the convergence process when majority of the system  coefficients are nearly zero in a sparse system.

Note that equation \eqref{eq:update_weight_vector} will be reduced to the normal QLMS algorithm without the zero attractor term, given by~\cite{liu14f}
\begin{equation}
\textbf{w}[n+1]=\textbf{w}[n]+\mu(e[n]{\textbf{x}}^{*}[n])\;.
\end{equation}

\section{Simulation Results}\label{sec:simulations}
In this part, simulations are performed for sparse system identification using the proposed algorithm in comparison with the QLMS algorithm. Two different sparse systems are considered corresponding to Scenario One and Scenario Two in the following.   The input signal to the adaptive filter is colored and generated by passing a quaternion-valued white gaussian signal through a randomly generated filter. The noise part is  quaternion-valued white Gaussian and added to the output of the unknown sparse system, with a 30dB signal to noise ratio (SNR) for both scenarios.

\subsection{Scenario One}
For the first scenario, the parameters are: the step size $\mu$ is $3\times10^{-7}$; the unknown sparse FIR filter length $L$ is $32$, with $4$ non-zero coefficients at the 2nd, 8th, 16th and 31st taps, and its magnitude of the impulse response is shown in Fig.~\ref{fig:w};  the coefficient of the zero attractor $\rho$ is $5\times10^{-7}$. The learning curve obtained by averaging $100$ runs of the corresponding algorithm is given in Fig.~\ref{fig:learning_curve_1}, where we can see that the ZA-QLMS algorithm has achieved a faster convergence speed than the QLMS algorithm when they both reach a similar steady state.
\begin{figure}[htbp]
\begin{center}
   \includegraphics[width=.49\textwidth]{w.eps}
   \caption{Magnitude of the impulse response of the sparse system.
    \label{fig:w}}
\end{center}
\end{figure}
\begin{figure}[htbp]
\begin{center}
   \includegraphics[width=.49\textwidth]{learning_error_1.eps}
   \caption{Learning curves for the first scenario.
    \label{fig:learning_curve_1}}
\end{center}
\end{figure}

\subsection{Scenario Two}
For this case, length of the unknown FIR filter is reduced to $16$, still with $4$ active taps. The parameters are: step size $\mu$ is $2\times10^{-7}$ and the value of $\rho$ is $2\times10^{-7}$. The results are shown in  Fig.~\ref{fig:learning_curve_2}. Again we see that the ZA-QLMS algorithm has a faster convergence speed and has even converged to a lower steady state error in this specific scenario.
\begin{figure}[htbp]
\begin{center}
   \includegraphics[width=.49\textwidth]{learning_error_2.eps}
   \caption{Learning Curves for the second scenario.
    \label{fig:learning_curve_2}}
\end{center}
\end{figure}

\section{Conclusion}\label{sec:conclusions}
In this paper, a quaternion-valued adaptive algorithm has been proposed for more efficient identification of unknown sparse systems. It is derived by introducing an $l_1$ penalty term in the original cost function and the resultant zero-attracting quaternion-valued LMS algorithm can achieve a faster convergence rate by incorporating the sparsity information of the system into the update process. Simulation results have been provided to show the effectiveness of the new algorithm.


TITLE: Partially ordered set defined by two comparisons?
QUESTION [0 upvotes]: I have a set of items, each of them with a grade and a price. On this set, a partial order is defined where x <= y if grade(x) <= grade(y) and price(x) <= price(y).
I have items like price(x) = 3 , grade(x) = 1  and price(y) = 2, grade(y) = 3. I don't understand how these should be ordered. Please help me!

REPLY [2 votes]: Remember that in a partial order, two objects don't necessarily have to be comparable; maybe $a\not\le b$ and $b\not\le a$!
That's what happens here. By definition, $x\le y$ iff $grade(x)\le grade(y)$ and $price(x)\le price(y)$. In the specific case you mention, the grade of $x$ is lower than the grade of $y$, but the price of $x$ is higher than the price of $y$; this means that $x$ and $y$ are not comparable.

On an abstract level, you're seeing a way to combine two partial orders to get a third. If $\le_1,\le_2$ are two different partial orderings on the same set $X$, then their intersection - $x\le_3 y$ iff $x\le_1y$ and $x\le_2 y$ - is also a partial ordering on $X$. You're looking at the intersection of the "price" and "grade" partial orderings. (And there are lots of other methods for building new partial orderings from old.)


TITLE: what would be the FOL of this: "Happy people have exciting lives"
QUESTION [0 upvotes]: I am confused whether I should use Existential Quantifier or not.
i only use existential quantifier on cases with "some", so how should I solve this one?

REPLY [2 votes]: $\forall x (Hx \rightarrow EL x)$ where $H$ denotes the predicate 'is happy' and $EL$ denotes the predicate 'has an exiting life'.


TITLE: Can a sentence in a model-theoretic conservative extension be translated in the language of its reduct?
QUESTION [2 upvotes]: Let $L1$ and $L2$ two languages with $L1 \subset L2$ and $T1$ and $T2$ respectively a theory in $L1$ and $L2$. We say that $T2$ is a model-theoretic conservative extension of $T2$ iff every model $M1$ of $T1$ can be expanded to a model $M2$ of $T2$ (see Conservative extension ).
When we have $T1$ which proves something like $\forall x \exists !y F[x,y]$ where $F[x,y]$ is a formula with free variables x and y, we can define $L2=L1 \cup \{f\}$ where $f$ is a symbol constant with arity 2, and $T2=T1 \cup \{\forall xF(x,f(x))\}$ (see Conservativity theorem ), which is a model-theoretic extension of T1
Hence my question is the following.
Is there any way to translate a sentence in $L2$ to a sentence in $L1$ ? For example, if $F$ is a $L2$-sentence, is there a $L1$-sentence $F'$ such as $T2 \vdash F \Leftrightarrow F'$ ? For example, if we take the theory of groups expressed in $L1$ which contains the symbols for the unity (constant), equality (2-ary relation), product (2-ary function), one can easily see that there is a natural model-theoretic conservative extension $L2$ equals $L1$ plus a symbol for the inverse (1-ary function). It would be convenient to use $L2$, and to say, not only for $L1$-sentences, that $T2 \vdash F$, hence $T1 \vdash$ (place here a formula not so much different from F). Because we use a stronger language and theory, but not so much.
My main concern is that in day-to-day mathematics, we use constants (0, empty set, etc.) and function symbols (for the pair, for sinus, etc.) introduced in that fashion and we say that everything is translatable in ZFC. Well, how ?

REPLY [2 votes]: The answer is no in general, but yes for definable extensions, such as the one you mentioned.
To see the "no" part, consider $L_1=T_1=T_2=\emptyset$, $L_2=\{f\}$ (a single function symbol); you can't write that $f$ is injective without referring to it, obviously.
On the other hand, if you have $L_2=L_1\cup\{f\}$, where $f$ is a ($\emptyset$-)definable function symbol, then if you take $\varphi(x,y)$ the definition of $f$, then you can just replace every occurence of $f$ in a sentence by its definition. For example
$$(\forall x,y) (x\neq y)\rightarrow f(x)\neq f(y)$$
can be rewritten as
$$(\forall x,y,z) (x\neq y)\rightarrow (f(x)=z\rightarrow f(y)\neq z)$$
and then as
$$(\forall x,y,z) (x\neq y)\rightarrow (\varphi(x,z)\rightarrow \neg\varphi(y,z))$$


TITLE: Bound on complex exponential
QUESTION [0 upvotes]: I was reading the following question, A function is $L^2$-differentiable if and only if $\xi\widehat{f}(\xi) \in L^2$., and in the accepted answer there is a bound
$$\left\lvert\frac{e^{2\pi ih\xi}-1}{h} \right\rvert \leqslant 2\pi \lvert \xi\rvert$$
and although it may not be complicated i got stuck on showing this bound, i do see that
$$ \lim_{h \to 0} \left\lvert\frac{e^{2\pi ih\xi}-1}{h} \right\rvert = 2\pi \lvert \xi\rvert$$
So i thought of showing this function is an increasing function but all i got was a mess on calculations, is there an easier way to see that bound?
Edit: i dont know what my idea was but definetely increasing function is not a way to show the bound

REPLY [1 votes]: $|e^{2\pi i\xi}-1|=2\pi |\xi||\int_0^{h} e^{2\pi i t\xi} dt|\leq 2\pi |\xi||\int_0^{h} 1 dt| \leq 2\pi |\xi|$ if $|h| \leq 1$.


TITLE: Expected number of jumps in regular jump HMC
QUESTION [2 upvotes]: Consider a homogeneous Markov Chain $X$ on a countable state space, ie a jump process.
It is said to be regular (does not explode) if there are only a finite number of jumps in every finite interval.
$$X(t) < \infty\quad \forall t > 0$$
What can you say the expected number of jumps in some interval? Is it finite too for regular processes in general? Is there a $a > 0$ so that
$$E[X(a)] < \infty$$
holds?
Consider for example a Poisson process with paramter $\lambda$. It is regular, and the expected number of jumps in a unit time is $\lambda$.
Especially I'd like to find out if the expected number of jumps of a regular pure birth-process is finite in some interval. That is a process process that jumps from $k$ to $k+1$ with rate $\lambda_k$, where for the rates
$$\sum_{k=1}\frac{1}{\lambda_k} = \infty$$
holds. By Reuter's criterion this is sufficient for the pure-birth process to be regular.

REPLY [2 votes]: The answer is: not necessarily.

We begin with some partial positive results. Recall that for every pure birth-process $(X_t)_{t\geqslant0}$ with positive rates $(\lambda(k))_{k\geqslant0}$ and for every suitable function $u$,
$$
\frac{\mathrm d}{\mathrm dt}\mathrm E(u(X_t))=\mathrm E((u(X_t+1)-u(X_t))\cdot\lambda(X_t)).
$$
In particular, the expectation $\mathrm E(X_t)$, if it exists, solves the differential equation
$$
\frac{\mathrm d}{\mathrm dt}\mathrm E(X_t)=\mathrm E(\lambda(X_t)).
$$
If $\lambda(k)\leqslant\lambda_0(k)$ for every integer $k$, for some positive concave function $\lambda_0$, then Jensen inequality yields $\mathrm E(\lambda(X_t))\leqslant\mathrm E(\lambda_0(X_t))\leqslant\lambda_0(\mathrm E(X_t))$. Integrating this yields $t\geqslant M(\mathrm E(X_t))$, where
$$
M(x)=\int_{\mathrm E(X_0)}^{x}\frac{\mathrm dz}{\lambda_0(z)}.
$$
If the integral of the function $1/\lambda_0$ diverges at infinity, $M$ is unbounded and this proves that $\mathrm E(X_t)\leqslant M^{-1}(t)$ is finite for every $t$.
Here is another integrability result, always valid. Consider
$$
\Lambda(k)=\sum_{i=0}^{k-1}\frac1{\lambda(i)}.
$$
Then the derivative of the function $t\mapsto\mathrm E(\Lambda(X_t))$ is $1$, hence $\mathrm E(\Lambda(X_t))=\Lambda(X_0)+t$ for every $t$ and in particular $\mathrm E(\Lambda(X_t))$ is finite for every $t$.
But of course, nothing guarantees that such a concave function $\lambda_0$ exists nor that $\Lambda(k)$ would be equivalent to a multiple of $k$ when $k\to\infty$...

...Which brings us to the negative result. Consider an infinite increasing positive integer sequence $(K(i))_{i\geqslant0}$, to be chosen later on. The sites in the set $\mathcal K=\{K(i)\,;\,i\geqslant0\}$ are slow sites and the other sites are fast sites, in the sense that one assumes that $\lambda(k)=1$ for every $k$ in $\mathcal K$ and that
$$
\sum\limits_{k\notin \mathcal K}\frac1{\lambda(k)}\ \text{is finite}.
$$
Then, Reuter criterion holds thanks to the infinitely many slow sites hence $(X_t)_{t\geqslant0}$ is regular. However, the total time $T$ spent at fast sites is almost surely finite, hence, on $[T\leqslant t]$,
$$
X_t\geqslant K(Y_{t-T(t)})\geqslant K(Y_{t-T}),
$$
where $T(t)$ is the time spent at fast sites up to time $t$, and $(Y_t)_{t\geqslant0}$ is a pure birth-process with constant rate $1$, independent on $T$. For every $t\gt0$, $[T\leqslant t]$ has positive probability and
$$
\mathrm E(X_{2t}:T\leqslant t)\geqslant\mathrm E(K(Y_{2t-T}):T\leqslant t)\geqslant\mathrm E(K(Y_{t}):T\leqslant t)=\mathrm E(K(Y_{t}))\cdot\mathrm P(T\leqslant t).
$$
Since $Y_t$ is Poisson with parameter $t$, the choice $K(i)=(i!)^2$ yields
$$
\mathrm E(K(Y_t))=\mathrm e^{-t}\sum_{i=0}^{+\infty}i!\,t^i,
$$
which diverges, for every positive $t$. Thus, $\mathrm E(X_{2t})\geqslant\mathrm E(X_{2t}:T\leqslant t)$ is infinite for every positive $t$.


text:
{\bf Problem.} When the base-12 integer $1531_{12}$ is divided by $8$, what is the remainder?
{\bf Level.} Level 3
{\bf Type.} Number Theory
{\bf Solution.} We have $$1531_{12} = 12^3 + 5\cdot 12^2 + 3\cdot 12 + 1.$$Note that $12^2$ is divisible by $8$, so $$1531_{12} = (\text{a multiple of 8}) + 3\cdot 12 + 1.$$Therefore, the remainder upon dividing $1531_{12}$ by $8$ is the same as the remainder upon dividing $3\cdot 12+1$ by $8$. This remainder is $\boxed{5}$.

set_name: MATH


text:
section\<open>Forcing notions\<close>
text\<open>This theory defines a locale for forcing notions, that is,
 preorders with a distinguished maximum element.\<close>

theory Forcing_Notions
  imports "ZF-Constructible.Relative"
begin

subsection\<open>Basic concepts\<close>
text\<open>We say that two elements $p,q$ are
  \<^emph>\<open>compatible\<close> if they have a lower bound in $P$\<close>
definition compat_in :: "i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>o" where
  "compat_in(A,r,p,q) \<equiv> \<exists>d\<in>A . \<langle>d,p\<rangle>\<in>r \<and> \<langle>d,q\<rangle>\<in>r"

definition
  is_compat_in :: "[i\<Rightarrow>o,i,i,i,i] \<Rightarrow> o" where
  "is_compat_in(M,A,r,p,q) \<equiv> \<exists>d[M]. d\<in>A \<and> (\<exists>dp[M]. pair(M,d,p,dp) \<and> dp\<in>r \<and>
                                   (\<exists>dq[M]. pair(M,d,q,dq) \<and> dq\<in>r))"

lemma compat_inI :
  "\<lbrakk> d\<in>A ; \<langle>d,p\<rangle>\<in>r ; \<langle>d,g\<rangle>\<in>r \<rbrakk> \<Longrightarrow> compat_in(A,r,p,g)"
  by (auto simp add: compat_in_def)

lemma refl_compat:
  "\<lbrakk> refl(A,r) ; \<langle>p,q\<rangle> \<in> r | p=q | \<langle>q,p\<rangle> \<in> r ; p\<in>A ; q\<in>A\<rbrakk> \<Longrightarrow> compat_in(A,r,p,q)"
  by (auto simp add: refl_def compat_inI)

lemma  chain_compat:
  "refl(A,r) \<Longrightarrow> linear(A,r) \<Longrightarrow>  (\<forall>p\<in>A.\<forall>q\<in>A. compat_in(A,r,p,q))"
  by (simp add: refl_compat linear_def)

lemma subset_fun_image: "f:N\<rightarrow>P \<Longrightarrow> f``N\<subseteq>P"
  by (auto simp add: image_fun apply_funtype)

lemma refl_monot_domain: "refl(B,r) \<Longrightarrow> A\<subseteq>B \<Longrightarrow> refl(A,r)"
  unfolding refl_def by blast

definition
  antichain :: "i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>o" where
  "antichain(P,leq,A) \<equiv> A\<subseteq>P \<and> (\<forall>p\<in>A.\<forall>q\<in>A.(\<not> compat_in(P,leq,p,q)))"

definition
  ccc :: "i \<Rightarrow> i \<Rightarrow> o" where
  "ccc(P,leq) \<equiv> \<forall>A. antichain(P,leq,A) \<longrightarrow> |A| \<le> nat"

locale forcing_notion =
  fixes P leq one
  assumes one_in_P:         "one \<in> P"
    and leq_preord:       "preorder_on(P,leq)"
    and one_max:          "\<forall>p\<in>P. \<langle>p,one\<rangle>\<in>leq"
begin

abbreviation Leq :: "[i, i] \<Rightarrow> o"  (infixl "\<preceq>" 50)
  where "x \<preceq> y \<equiv> \<langle>x,y\<rangle>\<in>leq"

lemma refl_leq:
  "r\<in>P \<Longrightarrow> r\<preceq>r"
  using leq_preord unfolding preorder_on_def refl_def by simp

text\<open>A set $D$ is \<^emph>\<open>dense\<close> if every element $p\in P$ has a lower
bound in $D$.\<close>
definition
  dense :: "i\<Rightarrow>o" where
  "dense(D) \<equiv> \<forall>p\<in>P. \<exists>d\<in>D . d\<preceq>p"

text\<open>There is also a weaker definition which asks for
a lower bound in $D$ only for the elements below some fixed
element $q$.\<close>
definition
  dense_below :: "i\<Rightarrow>i\<Rightarrow>o" where
  "dense_below(D,q) \<equiv> \<forall>p\<in>P. p\<preceq>q \<longrightarrow> (\<exists>d\<in>D. d\<in>P \<and> d\<preceq>p)"

lemma P_dense: "dense(P)"
  by (insert leq_preord, auto simp add: preorder_on_def refl_def dense_def)

definition
  increasing :: "i\<Rightarrow>o" where
  "increasing(F) \<equiv> \<forall>x\<in>F. \<forall> p \<in> P . x\<preceq>p \<longrightarrow> p\<in>F"

definition
  compat :: "i\<Rightarrow>i\<Rightarrow>o" where
  "compat(p,q) \<equiv> compat_in(P,leq,p,q)"

lemma leq_transD:  "a\<preceq>b \<Longrightarrow> b\<preceq>c \<Longrightarrow> a \<in> P\<Longrightarrow> b \<in> P\<Longrightarrow> c \<in> P\<Longrightarrow> a\<preceq>c"
  using leq_preord trans_onD unfolding preorder_on_def by blast

lemma leq_transD':  "A\<subseteq>P \<Longrightarrow> a\<preceq>b \<Longrightarrow> b\<preceq>c \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> P\<Longrightarrow> c \<in> P\<Longrightarrow> a\<preceq>c"
  using leq_preord trans_onD subsetD unfolding preorder_on_def by blast

lemma leq_reflI: "p\<in>P \<Longrightarrow> p\<preceq>p"
  using leq_preord unfolding preorder_on_def refl_def by blast

lemma compatD[dest!]: "compat(p,q) \<Longrightarrow> \<exists>d\<in>P. d\<preceq>p \<and> d\<preceq>q"
  unfolding compat_def compat_in_def .

abbreviation Incompatible :: "[i, i] \<Rightarrow> o"  (infixl "\<bottom>" 50)
  where "p \<bottom> q \<equiv> \<not> compat(p,q)"

lemma compatI[intro!]: "d\<in>P \<Longrightarrow> d\<preceq>p \<Longrightarrow> d\<preceq>q \<Longrightarrow> compat(p,q)"
  unfolding compat_def compat_in_def by blast

lemma denseD [dest]: "dense(D) \<Longrightarrow> p\<in>P \<Longrightarrow>  \<exists>d\<in>D. d\<preceq> p"
  unfolding dense_def by blast

lemma denseI [intro!]: "\<lbrakk> \<And>p. p\<in>P \<Longrightarrow> \<exists>d\<in>D. d\<preceq> p \<rbrakk> \<Longrightarrow> dense(D)"
  unfolding dense_def by blast

lemma dense_belowD [dest]:
  assumes "dense_below(D,p)" "q\<in>P" "q\<preceq>p"
  shows "\<exists>d\<in>D. d\<in>P \<and> d\<preceq>q"
  using assms unfolding dense_below_def by simp
    (*obtains d where "d\<in>D" "d\<in>P" "d\<preceq>q"
  using assms unfolding dense_below_def by blast *)

lemma dense_belowI [intro!]:
  assumes "\<And>q. q\<in>P \<Longrightarrow> q\<preceq>p \<Longrightarrow> \<exists>d\<in>D. d\<in>P \<and> d\<preceq>q"
  shows "dense_below(D,p)"
  using assms unfolding dense_below_def by simp

lemma dense_below_cong: "p\<in>P \<Longrightarrow> D = D' \<Longrightarrow> dense_below(D,p) \<longleftrightarrow> dense_below(D',p)"
  by blast

lemma dense_below_cong': "p\<in>P \<Longrightarrow> \<lbrakk>\<And>x. x\<in>P \<Longrightarrow> Q(x) \<longleftrightarrow> Q'(x)\<rbrakk> \<Longrightarrow>
           dense_below({q\<in>P. Q(q)},p) \<longleftrightarrow> dense_below({q\<in>P. Q'(q)},p)"
  by blast

lemma dense_below_mono: "p\<in>P \<Longrightarrow> D \<subseteq> D' \<Longrightarrow> dense_below(D,p) \<Longrightarrow> dense_below(D',p)"
  by blast

lemma dense_below_under:
  assumes "dense_below(D,p)" "p\<in>P" "q\<in>P" "q\<preceq>p"
  shows "dense_below(D,q)"
  using assms leq_transD by blast

lemma ideal_dense_below:
  assumes "\<And>q. q\<in>P \<Longrightarrow> q\<preceq>p \<Longrightarrow> q\<in>D"
  shows "dense_below(D,p)"
  using assms leq_reflI by blast

lemma dense_below_dense_below:
  assumes "dense_below({q\<in>P. dense_below(D,q)},p)" "p\<in>P"
  shows "dense_below(D,p)"
  using assms leq_transD leq_reflI  by blast
    (* Long proof *)
    (*  unfolding dense_below_def
proof (intro ballI impI)
  fix r
  assume "r\<in>P" \<open>r\<preceq>p\<close>
  with assms
  obtain q where "q\<in>P" "q\<preceq>r" "dense_below(D,q)"
    using assms by auto
  moreover from this
  obtain d where "d\<in>P" "d\<preceq>q" "d\<in>D"
    using assms leq_preord unfolding preorder_on_def refl_def by blast
  moreover
  note \<open>r\<in>P\<close>
  ultimately
  show "\<exists>d\<in>D. d \<in> P \<and> d\<preceq> r"
    using leq_preord trans_onD unfolding preorder_on_def by blast
qed *)

definition
  antichain :: "i\<Rightarrow>o" where
  "antichain(A) \<equiv> A\<subseteq>P \<and> (\<forall>p\<in>A.\<forall>q\<in>A.(\<not>compat(p,q)))"

text\<open>A filter is an increasing set $G$ with all its elements
being compatible in $G$.\<close>
definition
  filter :: "i\<Rightarrow>o" where
  "filter(G) \<equiv> G\<subseteq>P \<and> increasing(G) \<and> (\<forall>p\<in>G. \<forall>q\<in>G. compat_in(G,leq,p,q))"

lemma filterD : "filter(G) \<Longrightarrow> x \<in> G \<Longrightarrow> x \<in> P"
  by (auto simp add : subsetD filter_def)

lemma filter_leqD : "filter(G) \<Longrightarrow> x \<in> G \<Longrightarrow> y \<in> P \<Longrightarrow> x\<preceq>y \<Longrightarrow> y \<in> G"
  by (simp add: filter_def increasing_def)

lemma filter_imp_compat: "filter(G) \<Longrightarrow> p\<in>G \<Longrightarrow> q\<in>G \<Longrightarrow> compat(p,q)"
  unfolding filter_def compat_in_def compat_def by blast

lemma low_bound_filter: \<comment> \<open>says the compatibility is attained inside G\<close>
  assumes "filter(G)" and "p\<in>G" and "q\<in>G"
  shows "\<exists>r\<in>G. r\<preceq>p \<and> r\<preceq>q"
  using assms
  unfolding compat_in_def filter_def by blast

text\<open>We finally introduce the upward closure of a set
and prove that the closure of $A$ is a filter if its elements are
compatible in $A$.\<close>
definition
  upclosure :: "i\<Rightarrow>i" where
  "upclosure(A) \<equiv> {p\<in>P.\<exists>a\<in>A. a\<preceq>p}"

lemma  upclosureI [intro] : "p\<in>P \<Longrightarrow> a\<in>A \<Longrightarrow> a\<preceq>p \<Longrightarrow> p\<in>upclosure(A)"
  by (simp add:upclosure_def, auto)

lemma  upclosureE [elim] :
  "p\<in>upclosure(A) \<Longrightarrow> (\<And>x a. x\<in>P \<Longrightarrow> a\<in>A \<Longrightarrow> a\<preceq>x \<Longrightarrow> R) \<Longrightarrow> R"
  by (auto simp add:upclosure_def)

lemma  upclosureD [dest] :
  "p\<in>upclosure(A) \<Longrightarrow> \<exists>a\<in>A.(a\<preceq>p) \<and> p\<in>P"
  by (simp add:upclosure_def)

lemma upclosure_increasing :
  assumes "A\<subseteq>P"
  shows "increasing(upclosure(A))"
  unfolding increasing_def upclosure_def
  using leq_transD'[OF \<open>A\<subseteq>P\<close>] by auto

lemma  upclosure_in_P: "A \<subseteq> P \<Longrightarrow> upclosure(A) \<subseteq> P"
  using subsetI upclosure_def by simp

lemma  A_sub_upclosure: "A \<subseteq> P \<Longrightarrow> A\<subseteq>upclosure(A)"
  using subsetI leq_preord
  unfolding upclosure_def preorder_on_def refl_def by auto

lemma  elem_upclosure: "A\<subseteq>P \<Longrightarrow> x\<in>A  \<Longrightarrow> x\<in>upclosure(A)"
  by (blast dest:A_sub_upclosure)

lemma  closure_compat_filter:
  assumes "A\<subseteq>P" "(\<forall>p\<in>A.\<forall>q\<in>A. compat_in(A,leq,p,q))"
  shows "filter(upclosure(A))"
  unfolding filter_def
proof(auto)
  show "increasing(upclosure(A))"
    using assms upclosure_increasing by simp
next
  let ?UA="upclosure(A)"
  show "compat_in(upclosure(A), leq, p, q)" if "p\<in>?UA" "q\<in>?UA" for p q
  proof -
    from that
    obtain a b where 1:"a\<in>A" "b\<in>A" "a\<preceq>p" "b\<preceq>q" "p\<in>P" "q\<in>P"
      using upclosureD[OF \<open>p\<in>?UA\<close>] upclosureD[OF \<open>q\<in>?UA\<close>] by auto
    with assms(2)
    obtain d where "d\<in>A" "d\<preceq>a" "d\<preceq>b"
      unfolding compat_in_def by auto
    with 1
    have 2:"d\<preceq>p" "d\<preceq>q" "d\<in>?UA"
      using A_sub_upclosure[THEN subsetD] \<open>A\<subseteq>P\<close>
        leq_transD'[of A d a] leq_transD'[of A d b] by auto
    then
    show ?thesis unfolding compat_in_def by auto
  qed
qed

lemma  aux_RS1:  "f \<in> N \<rightarrow> P \<Longrightarrow> n\<in>N \<Longrightarrow> f`n \<in> upclosure(f ``N)"
  using elem_upclosure[OF subset_fun_image] image_fun
  by (simp, blast)

lemma decr_succ_decr:
  assumes "f \<in> nat \<rightarrow> P" "preorder_on(P,leq)"
    "\<forall>n\<in>nat.  \<langle>f ` succ(n), f ` n\<rangle> \<in> leq"
    "m\<in>nat"
  shows "n\<in>nat \<Longrightarrow> n\<le>m \<Longrightarrow> \<langle>f ` m, f ` n\<rangle> \<in> leq"
  using \<open>m\<in>_\<close>
proof(induct m)
  case 0
  then show ?case using assms leq_reflI by simp
next
  case (succ x)
  then
  have 1:"f`succ(x) \<preceq> f`x" "f`n\<in>P" "f`x\<in>P" "f`succ(x)\<in>P"
    using assms by simp_all
  consider (lt) "n<succ(x)" | (eq) "n=succ(x)"
    using succ le_succ_iff by auto
  then
  show ?case
  proof(cases)
    case lt
    with 1 show ?thesis using leI succ leq_transD by auto
  next
    case eq
    with 1 show ?thesis using leq_reflI by simp
  qed
qed

lemma decr_seq_linear:
  assumes "refl(P,leq)" "f \<in> nat \<rightarrow> P"
    "\<forall>n\<in>nat.  \<langle>f ` succ(n), f ` n\<rangle> \<in> leq"
    "trans[P](leq)"
  shows "linear(f `` nat, leq)"
proof -
  have "preorder_on(P,leq)"
    unfolding preorder_on_def using assms by simp
  {
    fix n m
    assume "n\<in>nat" "m\<in>nat"
    then
    have "f`m \<preceq> f`n \<or> f`n \<preceq> f`m"
    proof(cases "m\<le>n")
      case True
      with \<open>n\<in>_\<close> \<open>m\<in>_\<close>
      show ?thesis
        using decr_succ_decr[of f n m] assms leI \<open>preorder_on(P,leq)\<close> by simp
    next
      case False
      with \<open>n\<in>_\<close> \<open>m\<in>_\<close>
      show ?thesis
        using decr_succ_decr[of f m n] assms leI not_le_iff_lt \<open>preorder_on(P,leq)\<close> by simp
    qed
  }
  then
  show ?thesis
    unfolding linear_def using ball_image_simp assms by auto
qed

end (* forcing_notion *)

subsection\<open>Towards Rasiowa-Sikorski Lemma (RSL)\<close>
locale countable_generic = forcing_notion +
  fixes \<D>
  assumes countable_subs_of_P:  "\<D> \<in> nat\<rightarrow>Pow(P)"
    and     seq_of_denses:        "\<forall>n \<in> nat. dense(\<D>`n)"

begin

definition
  D_generic :: "i\<Rightarrow>o" where
  "D_generic(G) \<equiv> filter(G) \<and> (\<forall>n\<in>nat.(\<D>`n)\<inter>G\<noteq>0)"

text\<open>The next lemma identifies a sufficient condition for obtaining
RSL.\<close>
lemma RS_sequence_imp_rasiowa_sikorski:
  assumes
    "p\<in>P" "f : nat\<rightarrow>P" "f ` 0 = p"
    "\<And>n. n\<in>nat \<Longrightarrow> f ` succ(n)\<preceq> f ` n \<and> f ` succ(n) \<in> \<D> ` n"
  shows
    "\<exists>G. p\<in>G \<and> D_generic(G)"
proof -
  note assms
  moreover from this
  have "f``nat  \<subseteq> P"
    by (simp add:subset_fun_image)
  moreover from calculation
  have "refl(f``nat, leq) \<and> trans[P](leq)"
    using leq_preord unfolding preorder_on_def by (blast intro:refl_monot_domain)
  moreover from calculation
  have "\<forall>n\<in>nat.  f ` succ(n)\<preceq> f ` n" by (simp)
  moreover from calculation
  have "linear(f``nat, leq)"
    using leq_preord and decr_seq_linear unfolding preorder_on_def by (blast)
  moreover from calculation
  have "(\<forall>p\<in>f``nat.\<forall>q\<in>f``nat. compat_in(f``nat,leq,p,q))"
    using chain_compat by (auto)
  ultimately
  have "filter(upclosure(f``nat))" (is "filter(?G)")
    using closure_compat_filter by simp
  moreover
  have "\<forall>n\<in>nat. \<D> ` n \<inter> ?G \<noteq> 0"
  proof
    fix n
    assume "n\<in>nat"
    with assms
    have "f`succ(n) \<in> ?G \<and> f`succ(n) \<in> \<D> ` n"
      using aux_RS1 by simp
    then
    show "\<D> ` n \<inter> ?G \<noteq> 0"  by blast
  qed
  moreover from assms
  have "p \<in> ?G"
    using aux_RS1 by auto
  ultimately
  show ?thesis unfolding D_generic_def by auto
qed

end (* countable_generic *)

text\<open>Now, the following recursive definition will fulfill the
requirements of lemma \<^term>\<open>RS_sequence_imp_rasiowa_sikorski\<close> \<close>

consts RS_seq :: "[i,i,i,i,i,i] \<Rightarrow> i"
primrec
  "RS_seq(0,P,leq,p,enum,\<D>) = p"
  "RS_seq(succ(n),P,leq,p,enum,\<D>) =
    enum`(\<mu> m. \<langle>enum`m, RS_seq(n,P,leq,p,enum,\<D>)\<rangle> \<in> leq \<and> enum`m \<in> \<D> ` n)"

context countable_generic
begin

lemma preimage_rangeD:
  assumes "f\<in>Pi(A,B)" "b \<in> range(f)"
  shows "\<exists>a\<in>A. f`a = b"
  using assms apply_equality[OF _ assms(1), of _ b] domain_type[OF _ assms(1)] by auto

lemma countable_RS_sequence_aux:
  fixes p enum
  defines "f(n) \<equiv> RS_seq(n,P,leq,p,enum,\<D>)"
    and   "Q(q,k,m) \<equiv> enum`m\<preceq> q \<and> enum`m \<in> \<D> ` k"
  assumes "n\<in>nat" "p\<in>P" "P \<subseteq> range(enum)" "enum:nat\<rightarrow>M"
    "\<And>x k. x\<in>P \<Longrightarrow> k\<in>nat \<Longrightarrow>  \<exists>q\<in>P. q\<preceq> x \<and> q \<in> \<D> ` k"
  shows
    "f(succ(n)) \<in> P \<and> f(succ(n))\<preceq> f(n) \<and> f(succ(n)) \<in> \<D> ` n"
  using \<open>n\<in>nat\<close>
proof (induct)
  case 0
  from assms
  obtain q where "q\<in>P" "q\<preceq> p" "q \<in> \<D> ` 0" by blast
  moreover from this and \<open>P \<subseteq> range(enum)\<close>
  obtain m where "m\<in>nat" "enum`m = q"
    using preimage_rangeD[OF \<open>enum:nat\<rightarrow>M\<close>] by blast
  moreover
  have "\<D>`0 \<subseteq> P"
    using apply_funtype[OF countable_subs_of_P] by simp
  moreover note \<open>p\<in>P\<close>
  ultimately
  show ?case
    using LeastI[of "Q(p,0)" m] unfolding Q_def f_def by auto
next
  case (succ n)
  with assms
  obtain q where "q\<in>P" "q\<preceq> f(succ(n))" "q \<in> \<D> ` succ(n)" by blast
  moreover from this and \<open>P \<subseteq> range(enum)\<close>
  obtain m where "m\<in>nat" "enum`m\<preceq> f(succ(n))" "enum`m \<in> \<D> ` succ(n)"
    using preimage_rangeD[OF \<open>enum:nat\<rightarrow>M\<close>] by blast
  moreover note succ
  moreover from calculation
  have "\<D>`succ(n) \<subseteq> P"
    using apply_funtype[OF countable_subs_of_P] by auto
  ultimately
  show ?case
    using LeastI[of "Q(f(succ(n)),succ(n))" m] unfolding Q_def f_def by auto
qed

lemma countable_RS_sequence:
  fixes p enum
  defines "f \<equiv> \<lambda>n\<in>nat. RS_seq(n,P,leq,p,enum,\<D>)"
    and   "Q(q,k,m) \<equiv> enum`m\<preceq> q \<and> enum`m \<in> \<D> ` k"
  assumes "n\<in>nat" "p\<in>P" "P \<subseteq> range(enum)" "enum:nat\<rightarrow>M"
  shows
    "f`0 = p" "f`succ(n)\<preceq> f`n \<and> f`succ(n) \<in> \<D> ` n" "f`succ(n) \<in> P"
proof -
  from assms
  show "f`0 = p" by simp
  {
    fix x k
    assume "x\<in>P" "k\<in>nat"
    then
    have "\<exists>q\<in>P. q\<preceq> x \<and> q \<in> \<D> ` k"
      using seq_of_denses apply_funtype[OF countable_subs_of_P]
      unfolding dense_def by blast
  }
  with assms
  show "f`succ(n)\<preceq> f`n \<and> f`succ(n) \<in> \<D> ` n" "f`succ(n)\<in>P"
    unfolding f_def using countable_RS_sequence_aux by simp_all
qed

lemma RS_seq_type:
  assumes "n \<in> nat" "p\<in>P" "P \<subseteq> range(enum)" "enum:nat\<rightarrow>M"
  shows "RS_seq(n,P,leq,p,enum,\<D>) \<in> P"
  using assms countable_RS_sequence(1,3)
  by (induct;simp)

lemma RS_seq_funtype:
  assumes "p\<in>P" "P \<subseteq> range(enum)" "enum:nat\<rightarrow>M"
  shows "(\<lambda>n\<in>nat. RS_seq(n,P,leq,p,enum,\<D>)): nat \<rightarrow> P"
  using assms lam_type RS_seq_type by auto

lemmas countable_rasiowa_sikorski =
  RS_sequence_imp_rasiowa_sikorski[OF _ RS_seq_funtype countable_RS_sequence(1,2)]
end (* countable_generic *)

end

subset_name: curated


TITLE: Solutions to PDE $\langle\nabla\psi,\nabla\psi+\mathbf{f} \rangle= 0$
QUESTION [2 upvotes]: Consider the vector field
$$
\mathbf{f}(x_1,x_2)=\begin{bmatrix}f_1(x_1,x_2)\\ f_2(x_1,x_2)\end{bmatrix}=\begin{bmatrix}\frac{1}{1+x_2}+x_1\\ \frac{1}{1+x_1}+x_2\end{bmatrix}.
$$
I'm interested in finding a scalar function $\psi(x_1,x_2)$ such that:
$$\tag{$\ast$}\label{ast}
\langle\nabla\psi,\nabla\psi+\mathbf{f} \rangle= \frac{\partial\psi(x_1,x_2)}{\partial x_1} \left(f_1(x_1,x_2)+\frac{\partial\psi(x_1,x_2)}{\partial x_1}\right)+\frac{\partial\psi(x_1,x_2)}{\partial x_2} \left(f_2(x_1,x_2)+\frac{\partial\psi(x_1,x_2)}{\partial x_2}\right)=0
$$

My question. Does there exist a solution $\psi(x_1,x_2)$ to \eqref{ast}? If so, how to compute it?

I'm aware that my question could be a trivial or naive one, but since I'm new to this kind of problems I would really appreciate any help/comment/suggestion. Thank you.

REPLY [2 votes]: On the one hand, the nullity of the scalar product
$$
\nabla\psi\cdot (f+\nabla\psi) = \psi_{,1} (f_1+ \psi_{,1} )
+ \psi_{,2} (f_2+ \psi_{,2} ) = 0
$$
leads to the orthogonality of $\nabla\psi$ and $f+\nabla\psi$. Thus, $f+\nabla\psi$ is proportional to the vector $\nabla\psi^\perp = (\psi_{,1}, -\psi_{,2})^\top$. There exists $\alpha(x_1,x_2)$ such that $f+\nabla\psi = \alpha \nabla\psi^\perp$, or equivalently
$$
(1-\alpha)\psi_{,1} = -f_1
\qquad\text{and}\qquad
(1+\alpha)\psi_{,2} = -f_2 .
$$
By eliminating successively $\alpha$ and unity of the previous system, we get to
\begin{aligned}
2\psi_{,1}\psi_{,2} &= -f_2\psi_{,1} - f_1\psi_{,2}
\\
2\alpha\psi_{,1}\psi_{,2} &= -f_2\psi_{,1} + f_1\psi_{,2} .
\end{aligned}
On the other hand, the nullity of the scalar product rewrites as
$$
(\psi_{,1} + \psi_{,2})^2 - 2\psi_{,1}\psi_{,2} + f_1\psi_{,1} + f_2\psi_{,2} = 0 ,
$$
so that previous identities lead to
$$
(\psi_{,1} + \psi_{,2})^2 + (f_1+f_2)(\psi_{,1}  + \psi_{,2}) = 0 .
$$
Thus, the solutions satisfy $\psi_{,1} + \psi_{,2} = -(f_1+f_2)$ if they have nonzero divergence -- otherwise, they satisfy $\psi_{,1} + \psi_{,2} = 0$, which is a particular case of the previous non-homogeneous equation. Solutions to these linear first-order PDEs can be obtained by using the method of characteristics for the Lagrange-Charpit system
$\text d x_1 = \text d x_2 = {\text d \psi}/{r}$ with $r = -(f_1+f_2)$ (see related posts on this site). Solutions are of the form
$$
\psi(x_1, x_2) = \int^{x_1} r(\xi,\xi + x_2-x_1)\, \text d \xi + F(x_2-x_1) ,
$$
where $F$ is an arbitrary function. The latter is determined by injecting the previous expression in the orthogonality condition $\nabla\psi\cdot (f+\nabla\psi) = 0$.
If $f$ is constant, then linear solutions of the form
\begin{aligned}
\psi(x_1,x_2) &= -f_1x_1 - f_2x_2 + C \\
\text{or}\qquad
\psi(x_1,x_2) &= -\tfrac12(f_1+f_2)(x_1+x_2)+ C
\end{aligned}
are obtained.
In particular, one notes that the solutions are constant if $f \equiv 0$.
In theory, such solutions can be obtained similarly in the case
$$
f_1(x_1,x_2) = x_1 + (1+x_2)^{-1}, \qquad
f_2(x_1,x_2) = x_2 + (1+x_1)^{-1} ,
$$
but computations are more involved.


TITLE: Probability of an element being the maximum element in an array?
QUESTION [0 upvotes]: I've come up with a problem that seems so simple but I could not find where the problem is.
Assume we have three elements $A$, $B$, and $C$. Each element is a random number from $(0,1)$. What is the probability that $A$ is the maximum element in this array?
I think it can be expressed as $P( \{A>B\} \cap \{A>C\} )$, where $\{A>B\}$ and $\{A>C\}$ are independent events. Then seems the probability is 1/4. But surely we know the probability should be 1/3.
Where's the problem and what is the correct approach to calculate this probability?

REPLY [3 votes]: The answer is clearly $1/3$. What is written below may make that fact more obscure rather than less.
The joint density function is $1$ on the unit cube, and $0$ elsewhere. We can replace $>$ by $\ge$ without changing the probability.
The probability can be expressed as the iterated integral
$$\int_{x=0}^1 \left(\int_{y=0}^x \left(\int_{z=0}^x 1\,dz\right) \,dy\right)\,dx.$$
Or else we can note that unit cube has volume $1$.  Our probability is the volume of the part $K$ of the unit cube such that $x \ge y$ and $x \ge z$. That volume is the iterated integral above. But we can find the volume of $K$ more geometrically by noting that $3$ copies of it fit together to make up the unit cube.

REPLY [0 votes]: I'm trying to see if it is possible to calculate the probability in the basic approach

If $A = \alpha$, then the conditional probability that
$\{B < \alpha, C < \alpha\}$ is $\alpha^2$ by independence.
So, the unconditional probability can be found by multiplying
by the pdf of $A$ and integrating.  ($\int_0^1 \alpha^2 d\alpha = 1/3$).
If you don't like conditional probabilities,
$$P(A > B, C) = \int_0^1 \int_0^\alpha \int_0^\alpha
f(\alpha, \beta, \gamma) \mathrm d\gamma \mathrm d\beta \mathrm d\alpha
= \int_0^1 \int_0^\alpha \int_0^\alpha 1 \mathrm d\gamma \mathrm d\beta \mathrm d\alpha = \frac{1}{3}$$

REPLY [0 votes]: I assume that the random variables $A$, $B$ and $C$ are independent.  Since these are continuous random variables, with probability $1$ they are all different.  There are $6$ disjoint events, the possible orderings: $A < B < C$, $A < C < B$, $B < A < C$,
$B < C < A$, $C < A < B$, $C < B < A$, each of which (by symmetry) has probability $1/6$. All
the other events can be written as unions of these. So e.g.
$P((B<A) \cap (C<A)) = P(B < C < A) + P(C < B < A) = 1/3$, while
$P(B<A) = P(B < C < A) + P(B < A < C) + P(C < B < A) = 1/2$.

REPLY [0 votes]: There are six equally probable orders for independent identically distributed continuous random variables:

{A > B > C}
{A > C > B}
{B > A > C}
{B > C > A}
{C > A > B}
{C > B > A}

plus various orders with some equality, each of probability $0$.
So clearly the probability that $A$ is the maximum element is $\frac{2}{6} = \frac{1}{3}$.
As opt says, $\{A > B \}$ and $\{A > C \}$  are not independent events.  For example $\Pr(\{A > B\} |\{A > C\}) = \frac{2}{3}$ rather than $\frac{1}{2}$ and so $\Pr( \{A>B\} \cap \{A>C\} ) =  \frac{2}{3}\times \frac{1}{2}=\frac{1}{3}.$