# On the sequence $n!\bmod p$

Alexandr Grebennikov, Arsenii Sagdeev,
Aliaksei Semchankau, Aliaksei Vasilevskii

###### Abstract.

We prove, that the sequence $1!,2!,3!,\dots$ produces at least
$(\sqrt{2}+o(1))\sqrt{p}$ distinct residues modulo prime $p$. Moreover,
factorials on an interval $\mathcal{I}\subseteq\\{0,1,\dots,p-1\\}$ of length
$N>p^{7/8+\varepsilon}$ produce at least $(1+o(1))\sqrt{p}$ distinct residues
modulo $p$. As a corollary, we prove that every non-zero residue class can be
expressed as a product of seven factorials $n_{1}!\dots n_{7}!$ modulo $p$,
where $n_{i}=O(p^{6/7+\varepsilon})$ for all $i=1,\dots,7$, which provides a
polynomial improvement upon the preceding results.

MSC: 11N56, 11L03, 11B65

###### Contents

  1. 1 Introduction
  2. 2 Conventions and Preliminary Results
  3. 3 On images of generic polynomials
  4. 4 Properties of polynomials $P_{j}$
  5. 5 On inequality $|{\mathcal{A}}(p){\mathcal{A}}(p)|\geqslant p+o(p)$
  6. 6 On inequality $|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant p+o(p)$

##  1\. Introduction

Wilson’s theorem represents one of the most elegant results in elementary
number theory. It states that if $p$ is a prime number, then $(p-1)!=-1\bmod
p$. As one of its simple corollaries, we note that $(p-2)!=1!\bmod p$, and
thus not all the residues from

${\mathcal{A}}(p)\coloneqq\\{i!\bmod p:i\in[p-1]\\}$

are distinct. Erdős conjectured [16], that this is not the only coincidence,
i.e., that $|{\mathcal{A}}(p)|<p-2$. Surprisingly, despite the long history of
this natural problem, Erdős’ conjecture remains widely open though verified
[17] for all primes $p<10^{9}$.

At the same time, it is widely believed (see [2, 6] and [12], F11) that the
elements of ${\mathcal{A}}(p)$ may be considered as more or less ‘independent
uniform random variables’ for large $p$. In particular, it is conjectured that

$|{\mathcal{A}}(p)|=\left(1-\frac{1}{e}+o(1)\right)p$

as $p\rightarrow\infty$. However, the best lower bound up to now is due to
García [10]:

######  Theorem (García).

$|{\mathcal{A}}(p)|\geqslant\left(\sqrt{\frac{41}{24}}+o(1)\right)\sqrt{p}.$

The strategy in [10] was to prove that ${\mathcal{A}}(p){\mathcal{A}}(p)$
contains residues with certain properties, which forces the estimate
$|{\mathcal{A}}(p){\mathcal{A}}(p)|\geqslant(41/48+o(1))p$ to hold; combined
with the observation

${|{\mathcal{A}}(p)|+1\choose 2}\geqslant|{\mathcal{A}}(p){\mathcal{A}}(p)|$

this yields the result. We improve it to the following:

######  Theorem 1.

$|{\mathcal{A}}(p){\mathcal{A}}(p)|\geqslant p+O(p^{13/14}(\log{p})^{4/7}).$

######  Corollary 1.

$|{\mathcal{A}}(p)|\geqslant\big{(}\sqrt{2}+o(1)\big{)}\sqrt{p}.$

One of the natural ways to generalize this problem is to consider it in a
‘short interval’ setting (see [8, 9, 13, 15]). Throughout this paper, let $p$
be a large enough prime and $L,N$ be integers such that $0<L+1<L+N<p$.
Following Garaev and Hernández [8], we define a ‘short interval’ analogue of
${\mathcal{A}}(p)$ as follows:

${\mathcal{A}}(L,N)\coloneqq\\{n!\bmod p:L+1\leqslant n\leqslant L+N\\}.$

As $L$ will not play any role, we write ${\mathcal{A}}_{N}$ for short. To
bound the cardinality of this set from below, it is usually fruitful to
estimate the size of ${\mathcal{A}}_{N}/{\mathcal{A}}_{N}$, the set of
pairwise fractions, since we trivially have
$|{\mathcal{A}}_{N}|^{2}\geqslant|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|$. The
first lower bounds on the size of this set of fractions were linear on $N$
(see [9, 13]), while Garaev and Hernández [8] found the following logarithmic
improvement.

######  Theorem (Garaev-Hernández).

Let $p^{1/2+\varepsilon}<N<p/10$. Then

$\left|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}\right|\geqslant
c_{0}N\log\left(\frac{p}{N}\right)$

for some $c_{0}=c_{0}(\varepsilon)>0$.

The strategy in [8] was to observe ${\mathcal{A}}_{N}/{\mathcal{A}}_{N}$ to
contain the sets $X_{1},X_{2},\dots,X_{M}$ defined as
$X_{j}=\\{(x+1)(x+2)\dots(x+j):L+1\leqslant x\leqslant L+N-M\\}$, and then
prove $X_{j}$’s to be ‘large’, but their intersections $X_{k}\cap X_{j}$ to be
‘small’, which makes inclusion-exclusion formula applicable:

$|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant|X_{1}\cup
X_{2}\cup\dots|\geqslant\sum_{j}|X_{j}|-\sum_{k<j}|X_{k}\cap
X_{j}|\gg\sum_{j}|X_{j}|.$

In the present paper we give the following improvement of this result.

######  Theorem 2.

Let $N$ be such that $c_{5}\sqrt{p}(\log{p})^{2}\leqslant N\leqslant p$. Let
$K:=\frac{p}{N},Q:=\frac{N}{\sqrt{p}(\log{p})^{2}}$. Then

$|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant\begin{cases}p+O(p^{13/14}(\log{p})^{4/7})&\mbox{
if }N\geqslant c_{1}p^{13/14}(\log{p})^{4/7},\\\
p+O(p^{5/6}K^{4/3}(\log{p})^{4/3})&\mbox{ if
}c_{1}p^{13/14}(\log{p})^{4/7}\geqslant N\geqslant c_{2}p^{7/8}\log{p},\\\
cNQ^{1/3}(\log{Q})^{-2/3}&\mbox{ if }c_{2}p^{7/8}\log{p}\geqslant N\geqslant
c_{3}p^{4/5}(\log{p})^{8/5},\\\ cNK^{1/2}&\mbox{ if
}c_{3}p^{4/5}(\log{p})^{8/5}\geqslant N\geqslant
c_{4}p^{4/5}(\log{p})^{4/5},\\\ cNQ^{1/3}&\mbox{ if
}c_{4}p^{4/5}(\log{p})^{4/5}\geqslant N\geqslant
c_{5}p^{1/2}(\log{p})^{2}.\end{cases}$

where $c,c_{1},c_{2},c_{3},c_{4},c_{5}>0$ are some absolute constants, whose
values can be extracted from the proof.

######  Corollary 2.

For $N\gg p^{7/8}\log{p}$,

$|{\mathcal{A}}_{N}|\geqslant(1+o(1))\sqrt{p}.$

To derive it, we continue the strategy from [8] as follows: using strong
results from Algebraic Geometry, we prove ‘best possible’ bounds
$|X_{j}|\geqslant(1+o(1))N$ and $|X_{k}\cap X_{j}|\leqslant(1+o(1))N^{2}/p$
for prime $k,j$. Then we observe, that bounds on sets $X_{j}$ and their
intersections imply they behave ‘too independently’, and therefore the size of
their union is at least $p+o(p)$ (see Lemma 1), which implies that
${\mathcal{A}}_{N}/{\mathcal{A}}_{N}$ has size at least $p+o(p)$.

This strategy turns out to be helpful when proving Theorem 1 as well.

One of the nice applications of these results deals with representation of the
residues as a product of several factorials. It is not hard to see that the
classical Wilson’s theorem implies the following. Any given $a\in[p-1]$ can be
represented111Indeed, one may easily verify that, depending on the ‘parity’ of
the inverse residue $b\equiv a^{-1}$, we have either $a\equiv(b-1)!(p-1-b)!$,
or $a\equiv-(b-1)!(p-1-b)!\equiv(b-1)!(p-1-b)!(p-1)!$ modulo $p$. as a product
of three factorials

$a\equiv n_{1}!n_{2}!n_{3}!\bmod p$

for some $n_{1},n_{2},n_{3}\in[p-1]$. The aforementioned conjecture on the
‘randomness’ of ${\mathcal{A}}(p)$ implies that even two factorials are
enough. However, if we add an additional constraint the all $n_{i}$ should be
of the magnitude $o(p)$ as $p\rightarrow\infty$, it becomes not so clear how
many factorials are required. Garaev, Luca, and Shparlinski [9] coped with
seven.

######  Theorem (Garaev, Luca, and Shparlinski).

Fix any positive $\varepsilon<1/12$. Then for all prime $p$, every residue
class $a\not\equiv 0\bmod p$ can be represented as a product of seven
factorials,

$a\equiv n_{1}!\dots n_{7}!\pmod{p},$

such that $n_{0}\coloneqq\max_{1\leq i\leq 7}{n_{i}}=O(p^{11/12+\varepsilon})$
as $p\rightarrow\infty$.

During the last two decades, the number of multipliers from the last theorem
was not reduced even to $6$. However, there were certain improvements on the
value of $n_{0}$. García [11] showed that the Theorem above holds with
$n_{0}=O(p^{11/12}\log^{1/2}p)$, while Garaev and Hernández [8] relaxed it to
$O(p^{11/12}\log^{-1/2}p)$. Since our new Theorem 2 improves the bounds used
in the latter proof, one can obtain a slight (again, polynomial) improvement
on the value of $n_{0}$ by following the same proof.

######  Theorem 3.

Fix any positive $\varepsilon<1/7$. Then for all prime $p$, every residue
class $a\not\equiv 0\bmod p$ can be represented as a product of seven
factorials,

$a\equiv n_{1}!\dots n_{7}!\pmod{p},$

such that $n_{0}\coloneqq\max_{1\leq i\leq 7}{n_{i}}=O(p^{6/7+\varepsilon})$
as $p\rightarrow\infty$.

The remainder of the text has the following structure. In Section 2 we
introduce some notations and useful lemmas, in Section 3 we prove results on
images of ‘generic’ polynomials, in Section 4 we apply these results to
polynomials $P_{j}(x)=(x+1)\ldots(x+j)$, and, finally, in Sections 5 and 6 wee
prove theorems 1 and 2.

##  2\. Conventions and Preliminary Results

Here and below, $p$ denotes a large prime number.

Whenever $A$ is a set, we identify it with its indicator function, meaning

$A(x)=\begin{cases}1,\ x\in A,\\\ 0,\ x\not\in A.\end{cases}$

Throughout the paper, the standard notation $\ll,\gg$, and respectively $O$
and $\Omega$ is applied to positive quantities in the usual way. That is,
$X\ll Y,Y\gg X,X=O(Y)$ and $Y=\Omega(X)$ all mean that $Y\geqslant cX$, for
some absolute constant $c>0$.

A polynomial $f\in\mathbb{F}_{p}[x]$ is _decomposable_ , if $f=g\circ h$ for
some polynomials $g,h\in\mathbb{F}_{p}[x]$ of degrees at least $2$. Otherwise
it is _indecomposable_.

We recall that for any integer $d>0$ and $a\in\mathbb{F}_{p}$, the _Dickson
polynomial_ $D_{d,a}\in\mathbb{F}_{p}[x]$ is defined to be the unique
polynomial such that $D_{d,a}(x+\frac{a}{x})=x^{d}+(\frac{a}{x})^{d}$. There
is also an explicit formula for it:

$D_{d,a}(x)=\sum_{i=0}^{\lfloor d/2\rfloor}\frac{d}{d-i}{{d-i}\choose
i}(-a)^{i}x^{d-2i}.$

For a positive integer $j$ define the polynomial

$P_{j}(x)=\prod_{i=1}^{j}(x+i).$

Given a set $A$ and a polynomial $P\in\mathbb{F}_{p}[x]$, denote by $P(A)$ the
set $\\{P(a)\ (\bmod\ p):a\in A\\}$.

A key lemma to estimate the union of sets:

######  Lemma 1.

Let $A_{1},A_{2},\dots,A_{n}$ be finite sets, and let $a\geqslant b$ be
positive integers, such that the properties hold:

  * •

$|A_{i}|\geqslant a$ for all $i$,

  * •

$|A_{i}\cap A_{j}|\leqslant b$ for all $i\neq j$.

Let $A:=A_{1}\cup A_{2}\cup\dots A_{n}$. Then

$|A|\geqslant\frac{a^{2}}{b}\bigg{(}1-\frac{a}{nb}\bigg{)}.$

###### Proof.

Let $S=\sum_{i\leqslant n}\sum_{a\in A}A_{i}(a)\geqslant na$. Observe that

$S^{2}=\bigg{(}\sum_{a\in A}\big{(}\sum_{i\leqslant
n}A_{i}(a)\big{)}\bigg{)}^{2}\leqslant|A|\sum_{a\in A}\big{(}\sum_{i\leqslant
n}A_{i}(a)\big{)}^{2}=|A|\sum_{a\in A}\sum_{i,j\leqslant n}A_{i}(a)A_{j}(a)=$
$=|A|\sum_{i,j\leqslant n}|A_{i}\cap
A_{j}|\leqslant|A|\big{(}S+(n^{2}-n)b\big{)},$

which implies

$|A|\geqslant\frac{S^{2}}{S+(n^{2}-n)b}\geqslant\frac{(na)^{2}}{na+(n^{2}-n)b}\geqslant\frac{na^{2}}{a+nb}=\frac{a^{2}}{b}\frac{1}{1+\frac{a}{bn}}\geqslant\frac{a^{2}}{b}\bigg{(}1-\frac{a}{bn}\bigg{)}.$

∎

##  3\. On images of generic polynomials

The two following results seem to be well-known, yet not explicitly written in
the literature (see [5], [4] for more information on related questions); we
prove them in here for the sake of transparency.

######  Lemma 2.

Let $P\in\mathbb{F}_{p}[x]$ of degree $d$ be such that $\frac{P(x)-P(y)}{x-y}$
is absolutely irreducible over $\mathbb{F}_{p}$, and let $\mathcal{I}$ be an
arithmetical progression in $\mathbb{F}_{p}$, then:

$|P(\mathcal{I})|=|\mathcal{I}|+O\big{(}|\mathcal{I}|^{2}p^{-1}+d^{2}\sqrt{p}(\log{p})^{2}\big{)}.$

######  Lemma 3.

Let $P,Q\in\mathbb{F}_{p}[x]$ of maximal degree $d$ be such that $P(x)-Q(y)$
is absolutely irreducible over $\mathbb{F}_{p}$, and let $\mathcal{I}$ be an
arithmetical progression in $\mathbb{F}_{p}$, then:

$|P(\mathcal{I})\cap
Q(\mathcal{I})|\leqslant|\mathcal{I}|^{2}p^{-1}+O(d^{2}\sqrt{p}(\log{p})^{2}).$

We postpone their proofs until the end of the section, and formulate some
helpful results, which are only to be used in this section.

Given $P,Q\in\mathbb{F}_{p}[x]$, let us define
$\phi(P,Q)\in\mathbb{F}_{p}[x,y]$ as

$\phi(P,Q)(x,y):=\begin{cases}P(x)-Q(y),\text{ if }P\neq Q,\\\ \\\
\frac{P(x)-P(y)}{x-y},\ \ \ \ \ \text{ if }P=Q.\end{cases}$

Let us also define

$J(P,Q):=\\#\\{(x,y)\in\mathbb{F}_{p}\times\mathbb{F}_{p}:\phi(P,Q)(x,y)=0\\}.$

######  Lemma 4.

Given $P,Q\in\mathbb{F}_{p}[x]$, suppose that $\phi(P,Q)$ is absolutely
irreducible over $\mathbb{F}_{p}$. Then

$J(P,Q)=p+O(d^{2}\sqrt{p}),$

where $d$ is a degree of $\phi(P,Q)$.

###### Proof.

We recall the modification of classical Lang-Weil result [14], with error term
due to Aubry and Perret [1]:

######  Theorem (Lang-Weil).

Let $\mathbb{F}_{q}$ be a finite field. Let
$X\subseteq\mathbb{A}_{\mathbb{F}_{q}}^{2}$ be a geometrically irreducible
hypersurface of degree $d$. Then

$|X(\mathbb{F}_{q})-q|\leqslant(d-1)(d-2)\sqrt{q}+d-1.$

Since $\phi(P,Q)(x,y)$ is absolutely irreducible over $\mathbb{F}_{p}$, its
set of zeros is (by definition) a geometrically irreducible hypersurface, and
therefore the Lang-Weil Theorem is applicable.

This implies the conclusion of the lemma. ∎

Given a subset $\mathcal{I}\subseteq\mathbb{F}_{p}$, let us define

$J_{\mathcal{I}}(P,Q):=\\#\\{(x,y)\in\mathcal{I}\times\mathcal{I}:\phi(P,Q)(x,y)=0\\}.$

We need the following lemma, proof of which is already contained in [8] but we
write it down in full generality for explicity.

######  Lemma 5.

Let $P,Q\in\mathbb{F}_{p}[x]$ be such that $\phi(P,Q)$ has no linear divisors.
Let $\mathcal{I}$ be an arithmetical progression in $\mathbb{F}_{p}$. Then

$J_{\mathcal{I}}(P,Q)=\frac{|\mathcal{I}|^{2}}{p^{2}}J(P,Q)+O(d^{2}\sqrt{p}(\log{p})^{2}),$

where $d$ is a degree of $\phi(P,Q)$.

###### Proof.

We recall the statement of Lemma 1 in [8] (originated in [3]):

######  Theorem (Bombieri, Chalk-Smith).

Let $(b_{1},b_{2})\in\mathbb{F}_{p}\times\mathbb{F}_{p}$ be a nonzero vector
and let $f(x,y)\in\mathbb{F}_{p}[x,y]$ be a polynomial of degree $d\geqslant
1$ with the following property: there is no $c\in\mathbb{F}_{p}$ for which the
polynomial $f(x,y)$ is divisible by $b_{1}x+b_{2}y+c$. Then

$\bigg{|}\sum_{\begin{subarray}{c}(x,y)\in\mathbb{F}_{p}\times\mathbb{F}_{p}:\\\
f(x,y)=0\end{subarray}}e^{2\pi i(b_{1}x+b_{2}y)/p}\bigg{|}\leqslant
2d^{2}p^{1/2}.$

In what follows, we will need a bit of Discrete Fourier Transform in
$\mathbb{F}_{p}$. Given function $f:\mathbb{F}_{p}\rightarrow\mathbb{C}$
define its Discrete Fourier Transform
$\hat{f}:\mathbb{F}_{p}\rightarrow\mathbb{C}$ by

$\hat{f}(r)=\sum_{x\in\mathbb{F}_{p}}f(x)e^{-2\pi i\frac{rx}{p}}.$

One can easily verify the Fourier Inverse Transform formula:

$f(x)=\frac{1}{p}\sum_{r\in\mathbb{F}_{p}}\hat{f}(r)e^{2\pi i\frac{rx}{p}}.$

We also need the following well-known result. Let $\mathcal{I}$ be a (finite)
arithmetic progression in $\mathbb{F}_{p}$. Then

$\sum_{r\in\mathbb{F}_{p}}|\hat{\mathcal{I}}(r)|\ll p\log{p},$

where $\mathcal{I}:\mathbb{F}_{p}\rightarrow\mathbb{C}$ is interpreted as
characteristic function of the set $\mathcal{I}\subseteq\mathbb{F}_{p}$.

Let us consider $\mathcal{I}$ as a characteristic functions of a set. Then

$J_{\mathcal{I}}(P,Q)=\sum_{\begin{subarray}{c}(x,y)\in\mathbb{F}_{p}\times\mathbb{F}_{p}:\\\
\phi(P,Q)(x,y)=0\end{subarray}}\mathcal{I}(x)\mathcal{I}(y)=\sum_{\begin{subarray}{c}(x,y)\in\mathbb{F}_{p}\times\mathbb{F}_{p}:\\\
\phi(P,Q)(x,y)=0\end{subarray}}\frac{1}{p^{2}}\sum_{r_{1},r_{2}\in\mathbb{F}_{p}}\hat{\mathcal{I}}(r_{1})\hat{\mathcal{I}}(r_{2})e^{2\pi\frac{(r_{1}x+r_{2}y)}{p}}=$
$=\frac{|\mathcal{I}||\mathcal{I}|}{p^{2}}J(P,Q)+\frac{1}{p^{2}}\sum_{(r_{1},r_{2})\neq(0,0)}\hat{\mathcal{I}}(r_{1})\hat{\mathcal{I}}(r_{2})\sum_{\begin{subarray}{c}(x,y)\in\mathbb{F}_{p}\times\mathbb{F}_{p}\\\
\phi(P,Q)(x,y)=0\end{subarray}}e^{2\pi i\frac{(r_{1}x+r_{2}y)}{p}}.$

Last summand might be bounded as

$\frac{1}{p^{2}}\sum_{r_{1}\in\mathbb{F}_{p}}|\hat{\mathcal{I}}(r_{1})|\sum_{r_{2}\in\mathbb{F}_{p}}|\hat{\mathcal{I}}(r_{2})|\max_{(r_{1},r_{2})\neq
0}\bigg{|}\sum_{\begin{subarray}{c}(x,y)\in\mathbb{F}_{p}\times\mathbb{F}_{p}:\\\
\phi(P,Q)(x,y)=0\end{subarray}}e^{2\pi
i\frac{r_{1}x+r_{2}y}{p}}\bigg{|}\ll(\log{p})^{2}\sqrt{p}d^{2}.$

This completes the proof. ∎

Now, let us turn to the proof of the Lemma 2:

###### Proof.

Clearly, $|P(\mathcal{I})|\leqslant|\mathcal{I}|$. Now let us obtain a lower
bound. Cauchy-Bunyakovsky-Schwarz inequality implies:

$\\#\\{(x,y)\in\mathcal{I}\times\mathcal{I}:P(x)=P(y)\\}|P(\mathcal{I})|\geqslant|\mathcal{I}|^{2},$

Clearly,

$\\#\\{(x,y)\in\mathcal{I}\times\mathcal{I}:P(x)=P(y)\\}=|\mathcal{I}|+J_{\mathcal{I}}(P,P)\leqslant|\mathcal{I}|+|\mathcal{I}|^{2}p^{-1}+O(d^{2}\sqrt{p}\log^{2}{p}),$

where we applied Lemmas 5 and 4. Deriving the lower bound on
$|P(\mathcal{I})|$ completes the proof. ∎

Now we prove Lemma 3:

###### Proof.

By Lemmas 5 and 4:

$|P(\mathcal{I})\cap Q(\mathcal{I})|\leqslant
J_{\mathcal{I}}(P,Q)=\frac{|\mathcal{I}|^{2}}{p^{2}}J(P,Q)+O(d^{2}\sqrt{p}\log^{2}{p})\leqslant\frac{|\mathcal{I}|^{2}}{p}+O(d^{2}\sqrt{p}\log^{2}{p}).$

∎

##  4\. Properties of polynomials $P_{j}$

Let us deduce the following simple lemma:

######  Lemma 6.

For given $5\leqslant j<p$, the polynomial $P_{j}(x)\in\mathbb{F}_{p}[x]$ is
not equal to $\alpha D_{j,a}(x+b)+c$ for $\alpha,a,b,c\in\mathbb{F}_{p}$.
Moreover, if $j$ is prime, then $P_{j}(x)$ is indecomposable.

###### Proof.

The second assertion is clear since $\deg P_{j}=j$. The first assertion can be
proved by straightforward comparison of the first five leading coefficients of
these two polynomials. ∎

For given $k,j$ (possibly equal) we define the polynomial $Q_{kj}(x,y)$, equal
to $P_{k}(x)-P_{j}(y)$, divided by all possible linear factors. If $k=j$, we
denote this polynomial by $Q_{j}(x,y)$. One can show that for $k,j<p-2$

$Q_{kj}(x,y)=\begin{cases}P_{k}(x)-P_{j}(y)&\mbox{if }j\neq k,\\\ \\\
\frac{P_{j}(x)-P_{j}(y)}{x-y}&\mbox{if }k=j,\ j\mbox{ is odd},\\\ \\\
\frac{P_{j}(x)-P_{j}(y)}{(x-y)(x+y-j-1)}&\mbox{if }k=j,\ j\mbox{ is even}.\\\
\end{cases}$

######  Lemma 7.

$Q_{kj}(x,y)$ is absolutely irreducible over $\mathbb{F}_{p}$ for (possibly
equal) primes $2<j,k<p-2$.

###### Proof.

First, consider the case $j=k$. Recall a Theorem of Fried [7], with
modification by Turnwald [18]. We adopt it for the field $\mathbb{F}_{p}$ and
polynomial $f$ of degree less than $p$:

######  Theorem (Fried-Turnwald).

Let $f\in\mathbb{F}_{p}[x]$ be a polynomial of degree $n$, $4<n<p$. Consider
the polynomial

$\phi(x,y):=\frac{f(x)-f(y)}{x-y}$

If $f$ is indecomposable, and is not equal $\alpha D_{n,a}(x+b)+c$ for some
$\alpha,a,b,c\in\mathbb{F}_{p}$, then $\phi(x,y)$ is absolutely irreducible.

Application to the polynomial $P_{j}$ (along with the Lemma 6), with the
explicit check for $j=3$, gives the result.

Now, consider the case $j\neq k$. Recall the statement of Theorem 1B in [19]:

######  Theorem (Schmidt).

Let

$f(x,y)=g_{0}y^{d}+g_{1}(x)y^{d-1}+\ldots+g_{d}(x),$

be a polynomial from $\mathbb{K}[x,y]$ for some field $\mathbb{K}$, where
$g_{0}$ is a non-zero constant. Denote

$\psi(f)=\max_{1\leq i\leq d}{\frac{\deg g_{i}}{i}}$

and suppose $\psi(f)=\frac{m}{d}$ where $m$ is coprime to $d$. Then $f(x,y)$
is absolutely irreducible.

Notice that $\psi(Q_{kj})=\frac{k}{j}$, and therefore this gives the result. ∎

Clearly, if $j>k$ are odd primes, Lemma 7 is applicable, and Lemmas 2, 3 imply
the following:

(1)
$|P_{j}(\mathcal{I})|=|\mathcal{I}|+O\big{(}|\mathcal{I}|^{2}p^{-1}+j^{2}\sqrt{p}(\log{p})^{2}\big{)},$
(2) $|P_{j}(\mathcal{I})\cap
P_{k}(\mathcal{I})|\leqslant|\mathcal{I}|^{2}p^{-1}+O(j^{2}\sqrt{p}(\log{p})^{2}),$

where $\mathcal{I}$ is a finite arithmetic progression in $\mathbb{F}_{p}$.

##  5\. On inequality $|{\mathcal{A}}(p){\mathcal{A}}(p)|\geqslant p+o(p)$

Now we prove Theorem 1:

###### Proof.

Let $\varepsilon_{1},\varepsilon_{2}>0$ be dependent on $p$, but separated
from zero. Set

$N:=\lfloor p^{1-\varepsilon_{1}}\rfloor,\ \ M:=\lfloor
p^{\varepsilon_{2}}\rfloor,\ \ \kappa:=\log\log{p}/\log{p},\ \
\delta:=\min(\varepsilon_{1},1/2-2\varepsilon_{1}-2\varepsilon_{2}-2\kappa,\varepsilon_{2}-\varepsilon_{1}-\kappa)>0.$

Let $\mathcal{I}$ be the set of odd numbers, not exceeding $2N-M$, and let
$Y_{j}:=P_{j}(\mathcal{I})$. Clearly, $|\mathcal{I}|=N+O(M)$. Set

${\mathcal{A}}:=\\{1!,2!,\dots,(2N)!\\}\cup\\{(p-2N)!,\dots,(p-2)!,(p-1)!\\}\mod
p.$

Clearly,
${\mathcal{A}}{\mathcal{A}}\subseteq{\mathcal{A}}(p){\mathcal{A}}(p)$, and
from now on we work with ${\mathcal{A}}{\mathcal{A}}$.

From Wilson’s theorem it follows, that $y!(p-1-y)!=(-1)^{y+1}\mod p$.
Therefore, $y$ being odd implies $1/(p-1-y)!=y!\mod p$. Let $j\leqslant M$.
Then

${\mathcal{A}}{\mathcal{A}}\supseteq\\{(y+j)!(p-1-y)!\ |\ y+j<2N,y\text{ is
odd}\\}=$ $=\\{(y+j)!/y!\ |\ y+j<2N,y\text{ is odd}\\}=\\{P_{j}(y)\ |\
y+j<2N,y\text{ is odd}\\}.$

This implies $Y_{j}\subseteq{\mathcal{A}}{\mathcal{A}}$ for all $j\leqslant
M$.

By equations 1 and 2, implied by the Lemmas 2 and 3, we obtain the following
(note, that
$\delta\leqslant\varepsilon_{1},1/2-2\varepsilon_{1}-2\varepsilon_{2}-2\kappa$
now plays a role):

$|Y_{j}|\geqslant N+O(Np^{-\delta}),\ \ |Y_{k}\cap Y_{j}|\leqslant
N^{2}/p+O(N^{2}p^{-1-\delta}),\ k\neq j\text{ odd primes below $M$}.$

Set $A:=\bigcup_{j}Y_{j}$ for prime $j\leqslant M$. We reduced the problem to
show that $|A|\geqslant p+o(p)$.

Let us apply Lemma 1 with

$a:=N(1+O(p^{-\delta})),\ b:=\frac{N^{2}}{p}(1+O(p^{-\delta})),\ n\gg
M/\log{M}\gg p^{\varepsilon_{2}-\kappa}$

Notice that by definition of $\delta$, which includes
$\delta\leqslant\varepsilon_{2}-\varepsilon_{1}-\kappa$, inequality $a/bn\ll
p^{-\delta}$ holds, and therefore

$|A|\geqslant\frac{a^{2}}{b}\bigg{(}1-\frac{a}{bn}\bigg{)}\geqslant
p(1+O(p^{-\delta}))=p+O(p^{1-\delta}).$

Now our goal is to maximize $\delta$ subject to

(3) $\delta\leqslant\begin{cases}\varepsilon_{1},\\\
1/2-2\varepsilon_{1}-2\varepsilon_{2}-2\kappa,\\\
\varepsilon_{2}-\varepsilon_{1}-\kappa.\end{cases}$

Solving this system, we obtain optimal parameters
$\varepsilon_{1}:=1/14-4\kappa/7$, $\varepsilon_{2}:=1/7-\kappa/7$, giving
$\delta=1/14-4\kappa/7$. This completes the proof. ∎

##  6\. On inequality $|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant p+o(p)$

We turn to the proof of Theorem 2.

###### Proof.

Let $\mathcal{I}:=\\{L+1,\dots,L+N-M\\}$, and
$X_{j}:=P_{j}(\mathcal{I}),j\leqslant M$, with parameters $N,M$ depending on
the case:

Case 1: $N\gg p^{13/14}(\log{p})^{4/7}$.

For this case one can apply the same argument as in the proof of Theorem 1 to
obtain the desired bound.

Case 2: $p^{13/14}(\log{p})^{4/7}\gg N\gg p^{7/8}\log{p}$.

Same as in the proof above, we write $N=p^{1-\varepsilon_{1}}$ and set
$M=\lfloor p^{\varepsilon_{2}}\rfloor$ for $\varepsilon_{2}>0$. Observe, that
now $\varepsilon_{1}$ is fixed, but $\varepsilon_{2}$ is not.

Arguing as before, we obtain $|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant
p+O(p^{1-\delta})$, where

(4) $\delta\leqslant\begin{cases}\varepsilon_{1},\\\
1/2-2\varepsilon_{1}-2\varepsilon_{2}-2\kappa,\\\
\varepsilon_{2}-\varepsilon_{1}-\kappa.\end{cases}$

Let us set $\varepsilon_{2}:=1/6-\varepsilon_{1}/3-\kappa/3$. Observe that
$\varepsilon_{2}>0$ since $\varepsilon_{1}\leqslant 1/2-\kappa$. From here we
obtain, that
$\delta=\min(\varepsilon_{1},1/6-4\varepsilon_{1}/3-4\kappa/3)=1/6-4\varepsilon_{1}/3-4\kappa/3$
works. Notice, that $\delta>0$ as long as $\varepsilon_{1}<1/8-\kappa$.

This concludes the proof in case $N\gg p^{7/8}\log{p}$.

Case 3: $p^{7/8}\log{p}\gg N\gg p^{4/5}(\log{p})^{8/5}$.

Let $R$ be a positive integer we choose later. Let $M$ be a number with
exactly $R$ odd primes below it. Clearly, $M\approx R\log{R}$.

Clearly, for odd prime $j$ below $M$ we have $|X_{j}|\geqslant
N+O(N^{2}p^{-1}+j^{2}\sqrt{p}(\log{p})^{2})\gg N$ if $M^{2}\ll Q$.

Clearly, summing $|X_{k}\cap X_{j}|$ for odd primes $k$ below odd prime
$j\leqslant M$, we have

$\sum_{k<j}|X_{k}\cap X_{j}|\ll\frac{N^{2}}{p}R+RM^{2}\sqrt{p}(\log{p})^{2}\ll
N\;\text{ if }R\ll K,R^{3}(\log{R})^{2}\ll Q.$

Therefore, setting $R:=Q^{1/3}(\log{Q})^{-2/3}$, we obtain

$|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant\underbrace{|X_{3}\cup
X_{5}\cup\dots|}_{\text{first $R$ odd primes}}-\sum_{k<j,\text{odd
primes}}|X_{k}\cap X_{j}|\gg\underbrace{|X_{3}|+|X_{5}|+\dots}_{\text{first
$R$ odd primes}}\gg NR,$

which completes the proof in this case.

Case 4: $p^{4/5}(\log{p})^{8/5}\gg N\gg p^{1/2}(\log{p})^{2}$.

We follow the same line of argumentation, as in the [8], but with modified
bounds on sets $X_{j}$ and their intersections.

From now on we work with all $j$, not just prime ones. Clearly,
$J(j),J(k,j)\leqslant pj$, and therefore estimates

$J_{N}(j),J_{N}(k,j)\leqslant\frac{N^{2}}{p^{2}}pj+O(j^{2}\sqrt{p}(\log{p})^{2})$

hold, same as in [8].

Same as in the proof of Lemma 2, we apply Cauchy-Bunyakovskii-Shwarz
inequality:

$\\#\\{(x,y):P_{j}(x)=P_{j}(y),1\leqslant x,y\leqslant
N-M\\}|X_{j}|\geqslant(N-M)^{2},$

from where we obtain

$|X_{j}|\geqslant\frac{N^{2}}{N+J_{N}(j)}\geqslant
N+O\bigg{(}\frac{N^{2}j}{p}+j^{2}\sqrt{p}(\log{p})^{2}\bigg{)}\ \ \forall\
j\leqslant M.$

For $X_{k}\cap X_{j}$ we have the bound

$|X_{k}\cap X_{j}|\leqslant
J_{N}(k,j)\leqslant\frac{N^{2}}{p}j+O(j^{2}\sqrt{p}(\log{p})^{2})\ \ \forall\
k<j\leqslant M,$

same as in [8].

Clearly, we have $|X_{j}|\gg N$ as long as $M\ll K,M^{2}\ll Q$.

Clearly, we have $\sum_{k<j}|X_{k}\cap X_{j}|\ll N\ll|X_{j}|$ as long as
$M^{2}\ll K,M^{3}\ll Q$.

Therefore, similarly to [8], we conclude

$|{\mathcal{A}}_{N}/{\mathcal{A}}_{N}|\geqslant\sum_{j\leqslant
M}\bigg{(}|X_{j}|-\sum_{k<j}|X_{k}\cap X_{j}|\bigg{)}\gg\sum_{j\leqslant
M}|X_{j}|\gg MN,$

where we set $M:=\min(\sqrt{K},\sqrt[3]{Q})$, which gives the desired bound. ∎

### Acknowledgments

A. Grebennikov is supported by Ministry of Science and Higher Education of the
Russian Federation, agreement № 075–15–2019–1619. A. Sagdeev is supported in
part by ERC Advanced Grant ‘GeoScape’. He is also a winner of Young Russian
Mathematics Contest and would like to thank its sponsors and jury. A.
Semchankau was supported by the Foundation for the Advancement of Theoretical
Physics and Mathematics “BASIS”. Also, A. Semchankau was partially supported
by the University of Bordeaux Pause Program, the ANR project JINVARIANT, and
Journal de Théorie des Nombres de Bordeaux. Besides that, he is very happy to
thank the Institut de Mathématiques de Bordeaux for their hospitality and
excellent working conditions. A significant part of this project was done
during the research workshop “Open problems in Combinatorics and Geometry
III”, held in Adygea in October 2021.

## References

  * [1] Y. Aubry, M. Perret A Weil theorem for singular curves https://doi.org/10.1515/9783110811056.1.
  * [2] K.A. Broughan, A.R. Barnett, On the missing values of $n!\bmod p$, J. Ramanujan Math. Soc., 24(3):277–284, 2009.
  * [3] J. H. H. Chalk and R. A. Smith, On Bombieri’s estimate for exponential sums, Acta Arith. 18 (1971), 191–212 http://matwbn.icm.edu.pl/ksiazki/aa/aa18/aa18121.pdf
  * [4] J. Cilleruelo, M.Z. Garaev, A. Ostafe, I. Shparlinski On the concentration of points of polynomial maps and applications, Mathematische Zeitschrift. 272(2011). http://matematicas.uam.es/~franciscojavier.cilleruelo/Papers/Concentr-Poly.pdf
  * [5] M.-C. Chang, Sparsity of the intersection of polynomial images of an interval, Acta Arith., 165 (2014), 243–249. https://math.ucr.edu/~mcc/paper/149%20SolBox.pdf
  * [6] C. Cobeli, M. Vâjâitu, A. Zaharescu, The sequence $n!\pmod{p}$, J. Ramanujan Math. Soc., 15(2):135–154, 2000.
  * [7] M. Fried, On a conjecture of Schur, Michigan Mathematical Journal, 1970. https://doi.org/10.1307/mmj/1029000374.
  * [8] Garaev, M.Z., Hernández, J. “A note on $n!$ modulo $p$“ . _Monatsh Math_ 182, 23–31 (2017). https://doi.org/10.1007/s00605-015-0867-8. https://arxiv.org/abs/1505.05912.
  * [9] M.Z. Garaev, F. Luca, I.E. Shparlinski, Character sums and congruences with $n!$, Trans. Amer. Math. Soc., 356(12):5089–5102 (electronic), 2004.
  * [10] V.C. García, On the value set of n!m! modulo a large prime, Bol. Soc. Mat. Mexicana, 13 (2007), 1–6.
  * [11] V.C. García, Representations of residue classes by product of factorials, binomial coefficients and sum of harmonic sums modulo a prime, Bol. Soc. Mat. Mexicana 14 (2008), 165-175.
  * [12] R.K. Guy, Unsolved problems in number theory, Springer-Verlag, New York, 1994.
  * [13] O. Klurman, M. Munsch, Distribution of factorials modulo $p$, Journal de Théorie des Nombres de Bordeaux (2017), 29(1), 169-177.
  * [14] S. Lang, A. Weil, Number of Points of Varieties in Finite Fields., American Journal of Mathematics 76, no. 4 (1954): 819–27. https://doi.org/10.2307/2372655.
  * [15] V.F. Lev, Permutations in abelian groups and the sequence $n!\pmod{p}$, European J. Combin., 27(5):635–643, 2006.
  * [16] B. Rokowska, A. Schinzel, Sur un probléme de M. Erdős, Elem. Math., 15:84–85, 1960\.
  * [17] T. Trudgian, There are no socialist primes less than $10^{9}$, Integers, 14:Paper No. A63, 4, 2014.
  * [18] G. Turnwald, On Schur’s conjecture, Journal of the Australian Mathematical Society. Series A. Pure Mathematics and Statistics, 58(3), 312-357 (1995). doi:10.1017/S1446788700038349,
  * [19] W. M. Schmidt, Absolutely irreducible equations $f(x,y)=0$. In: Equations over Finite Fields An Elementary Approach. Lecture Notes in Mathematics, vol 536. Springer, Berlin, Heidelberg (1976). https://doi.org/10.1007/BFb0080441

A. Grebennikov
Saint-Petersburg State University, Saint-Petersburg, Russia
IMPA, Rio de Janeiro, Brazil
<EMAIL_ADDRESS>
A. Sagdeev
Alfréd Rényi Institute of Mathematics, Budapest, Hungary
<EMAIL_ADDRESS>
A. Semchankau
Moscow State University, Moscow, Russia
Saint-Petersburg State University, Saint-Petersburg, Russia
<EMAIL_ADDRESS>
A. Vasilevskii
Carnegie Mellon University, Pittsburgh, US
<EMAIL_ADDRESS>


# Advanced Super-Resolution using Lossless Pooling Convolutional Networks

Farzad Toutounchi, Ebroul Izquierdo
Multimedia and Vision Research Group
Queen Mary University of London
<EMAIL_ADDRESS>
###### Abstract

In this paper, we present a novel deep learning-based approach for still image
super-resolution, that unlike the mainstream models does not rely solely on
the input low resolution image for high quality upsampling, and takes
advantage of a set of artificially created auxiliary self-replicas of the
input image that are incorporated in the neural network to create an enhanced
and accurate upscaling scheme. Inclusion of the proposed lossless pooling
layers, and the fusion of the input self-replicas enable the model to exploit
the high correlation between multiple instances of the same content, and
eventually result in significant improvements in the quality of the super-
resolution, which is confirmed by extensive evaluations.

##  1 Introduction

Super-resolution (SR) has received significant attention in recent years, and
the learning-based approaches in designing SR solutions have been providing
promising results for spatial upsampling of still images and videos. In
particular, application of deep learning and Convolutional Neural Networks
(CNN) has become a trendy approach for SR, leading to major improvements in
the performance of the state-of-the-art SR solutions.

Dong et al. [3, 4] presented the first concrete deep learning-based SR
approach for still images, exploiting deep CNNs, capable of upsampling still
images with high visual quality and reasonable complexity. Dong et al.
improved their work further in [5] by introduction of transposed convolutional
layers to their framework for upsampling from source to target resolution. Shi
et al. [13] used a similar concept as [5] for reducing the complexity of the
framework, except they introduced a sub-pixel upscaling layer instead of the
transposed convolution layer, with which they achieved an efficient
performance.

Other major contributions in still image SR using deep learning have been made
by Kim et al. [7, 8]. In [7], the concept of residual learning was introduced
to deep SR models, which led to quicker convergence of the network and high
visual quality reconstruction. In [8], a deep and recursive architecture was
employed, that achieved very good performance in terms of image quality,
although expensive in terms of computation cost. In other deep learning-
related efforts, Wang et al. [15] introduced a deep joint SR model to exploit
both external and self-similarities for reconstruction, in which a stacked
denoising convolutional auto-encoder was first trained on external training
data, then it was fine-tuned with multi-scale self-examples from the input
data.

0.40.50.60.70.80.93030.53131.532SRCNNESPCNFSRCNNREDNetLPCN-SR (ours)LPCN-SR+
(ours)Average processing time on GPU [sec]

Average PSNR [dB]

Figure 1: Performance comparison of the proposed SR approach with the state-
of-the-art models on Set 5 images.

Another interesting endeavor in devising deep learning models for image SR was
done by Mao et al. [12]. They introduced a deep hourglass-shaped CNN that
included multiple convolution and transposed convolution layers with symmetric
skip connections and was designed originally for image denoising. However, the
model was also applied for SR and image upscaling, and it was reported as one
of the best SR models in the literature for high quality image upscaling.
Ledig et al. [10] also made a contribution to SR by using a generative
adversarial network for performing high quality SR on images, and they showed
promising results in highly textured images, and high subjective quality,
although the method falls behind the state-of-the-art approaches in terms of
the objective metrics.

$H/r$$W/r$$W$$H$(a)(b) Figure 2: The lossless pooling process: (a) Input and
output of the layer for $r=2$, and (b) a sample lossless pooling on a
grayscale image.

While major improvements are reported in the still image SR domain, video SR
has also been an active research field, and several interesting contributions
have been made in recent years by applying deep learning-based solutions to
multi-frame SR [2, 6, 14, 11]. In multi-frame SR, unlike the typical still
image SR problem, several input frames that are highly correlated contribute
in generation of one high quality upsampled target image, hence a better
objective and subjective quality can be expected when compared to the single
image SR. Inspired by this approach, we aimed at devising a model that
utilizes the multi-frame concept within the still image frameworks for an
enhanced SR experience, using artificially generated self-replicas of the
input image.

In this paper, we propose a novel approach for still image SR which exploits
the incorporation of several auxiliary downscaled versions of the input image
in CNNs, that results in a significant improvement in the quality of the
reconstructed output image (Figure 1). The followings summarize the main
contributions of this paper:

  * •

Introduction of lossless pooling layers that create several highly correlated
downsampled replicas from the input image, that can fuse in the SR network.

  * •

Designing a lossless pooling convolutional network SR (LPCN-SR) model, that
only exploits the downsampled self-replicas, and can provide faster
performance than the existing high quality approaches.

  * •

Designing a lossless pooling convolutional network SR model that also
incorporates the original input image in addition to the self-replicas (LPCN-
SR+), and can outperform the existing approaches in terms of quality.

The rest of this paper is organized as follows. In Section 2, we introduce the
novelties including the lossless pooling mechanism, as well as incorporation
of the self-replicas in SR networks. Section 3 covers the technical
specifications of the proposed CNN architecture and the proposed SR model.
Section 4 summarizes the results of our evaluations and comparisons with
state-of-the-art approaches, followed by conclusions in Section 5.

##  2 Proposed Approach

Our proposed approach is inspired by the multi-frame SR models that take
several highly correlated low resolution inputs and generate a high resolution
version of a target image. In order to extend this concept to still image SR,
we require multiple versions of the low resolution image as the input. Hence a
mechanism is needed to create different replicas of the input image. We
propose a particular pooling process which downsamples the input image to
several lower resolution versions by reshuffling the pixel positions and
without any information loss. The resulting replicas of the input image can be
incorporated in a multi-frame model for upsampling the target image. In the
following, the proposed pooling operation is described in details. The process
of self-replicas fusion and their inclusion in the SR network are described
next.

###  2.1 Lossless Pooling Layer

Normal pooling layers in CNNs result in the loss of data, however we propose a
pooling layer that downscales a single-channel image to a multi-channel image
with lower spatial resolution. Lossless pooling process is performed by
rearranging a $H\times W$ matrix $\mathbf{M}$ into a
$\frac{H}{r}\times\frac{W}{r}\times r^{2}$ tensor $\mathbf{T}$. This operation
can be considered as a reverse sub-pixel upscaling defined in [13], and can be
described mathematically as the following $\mathcal{LP}$ function:

$\mathbf{T}={\mathcal{LP}(\mathbf{M})}_{x,\ y,\ c}=\mathbf{M}_{r\cdot
x-\bmod(r^{2}-c,r),\ r\cdot y-\left\lfloor\frac{r^{2}-c}{r}\right\rfloor}$ (1)

where x, y, and c represent the coordinates of a pixel in the output tensor.
Although the above description aims at lossless pooling of single-channel
(grayscale) images, the concept can be easily extended to multi-channel
images. Figure 2 demonstrates the lossless pooling operation, along with a
visual example.

Application of lossless pooling layer reduces the spatial size of the input
data without losing any information, and reduces the computation cost of
convolution operation by a factor of $r^{2}$. Moreover, the process results in
several replicas of the input image with very high correlations, which can
eventually act as a data augmentation process that can enhance the still image
SR.

###  2.2 Self-Replicas Fusion

Lossless Pooling

Convolution Layers

Concatenation

Reshuffling

Figure 3: The process of fusing the self-replicas in CNNs by concatenation and
reshuffling of the convolution outputs.

In multi-frame SR, application of multiple input frames for creating a high
quality upsampled target frame is well studied, and Caballero et al. [2] and
Kapperler et al. [6] present different ways of fusing the inputs within the
CNN architectures to obtain a single-image output from a multi-frame input,
while fully exploiting the correlations between the input frames. We adopt a
similar approach, namely early fusion, for coping with the downsampled
replicas created by the lossless pooling layer.

If an input frame of size $H\times W$ is fed to the lossless pooling layer
with parameter $r$, $r^{2}$ downsampled replicas are generated, and each
replica is fed to a convolutional layer with $n$ filters. The resulting output
is an ensemble of $r^{2}$ feature maps, each with the size
$(\frac{H}{r},\frac{W}{r},n)$. The feature maps can then be concatenated and
create one set of feature maps $\mathbf{F}$ with the size
$(\frac{H}{r},\frac{W}{r},n\times r^{2})$. This is similar to the early fusion
concept introduced in [2, 6], also demonstrated in Figure 3 for the case of
$r=2$ and $n=4$.

In addition to the concatenation of the feature maps, which is a widely used
approach in multi-frame processing, we perform a reshuffling of the feature
maps in order to create a better mix of the features produced by different
replicas. The reshuffling is performed by rearranging the order of the
features in the depth dimension as the following $\mathcal{RS}$ function:

${\mathcal{RS}(\mathbf{F})}_{x,\ y,\ c}={\mathbf{F}}_{x,\ y,\
\left\lceil\frac{c}{r^{2}}\right\rceil+n\cdot\bmod(c-1,r^{2})}$ (2)

where the reshuffled output of the process is depicted in Figure 3. This
output can be treated as a normal feature map and be further processed in a
CNN with different layers. Similar to the lossless pooling process, the
concatenation and reshuffling processes can also be easily extended to multi-
channel images.

##  3 Architecture and Implementation

Bicubic Upscaling $\times s$

Lossless Pooling $\times 2$

Concatenation & Reshuffling

Sub-pixel Upscaling $\times 2$

Downsampled Replicas

conv $5\times 5$ stride 1 + ReLU

conv $1\times 1$ stride 1 + ReLU

conv $3\times 3$ stride 1 + ReLU

conv $3\times 3$ stride 2 + ReLU

transconv $3\times 3$ stride 2 + ReLU

6416161616411

Input LR Image

Final SR Image

641282562562562562561286464

Encoder-Decoder

Bicubic HR Image

SR Image A

SR Image B

Figure 4: The architecture of the proposed CNN for still image SR. The solid
connections depict the LPCN-SR model. Inclusion of the dashed connections in
the model results in the LPCN-SR+. The red lines present the skip connections
between layers.

With the introduction of the lossless pooling and the concatenation and
reshuffling mechanisms, a CNN architecture can be devised to incorporate the
abovementioned processes in the still image SR problem. Our proposed network
is illustrated in Figure 4. The first step in the process is a bicubic
interpolation similar to many state-of-the-art approaches to reach the target
resolution. This step also ensures that one architecture can be applied for
upsampling with different scaling factors. Hence given an input low resolution
image, a high resolution version using bicubic upscaling is created, and then
the lossless pooling, individual convolutional layers on downsampled replicas,
concatenation of the feature maps, and reshuffling is performed. Depending on
the selected architecture, the network can work on two different modes, each
described in details in the following.

###  3.1 LPCN-SR

The proposed CNN architecture for still image SR can be operational in two
modes. The first mode is a basic version of the model, namely LPCN-SR, that
only takes the downsampled replicas as the key inputs for SR, and ignores the
original low quality input image generated by bicubic interpolation. This
model is depicted by solid lines and connections in Figure 4. The output to
this model is denoted as _SR Image A_ in the figure. As mentioned earlier, an
input grayscale image of size $(\frac{H}{s},\frac{W}{s})$ is interpolated to
the target resolution of $(H,W)$ using bicubic filtering. The first step after
the bicubic interpolation is the lossless pooling with $r=2$, which results in
four downsampled replicas, each with the size of $(\frac{H}{2},\frac{W}{2})$.
Each of the replicas goes through separate convolutional layers with 16
filters, resulting in four tensors of size $(\frac{H}{2},\frac{W}{2},16)$. The
four tensors are concatenated and reshuffled according to Section 2.2 to
create a feature map of size $(\frac{H}{2},\frac{W}{2},64)$.

The resulting feature map is then fed to a typical encoder-decoder
architecture consisting of 10 layers with the kernel specifications presented
in Figure 4. The encoder-decoder structure contains coupled convolution and
transposed convolution layers with stride of 2, that are also connected using
skip connections. The output of this stage is a tensor with a similar size as
the input feature map to the encoder-decoder network. The generated feature
map is then fed to one last convolution layer resulting in a tensor of size
$(\frac{H}{2},\frac{W}{2},4)$. We then use a sub-pixel upscaling operation as
proposed in [13] to upsample the tensor to the target resolution and create an
image of the target size $(H,W)$. This image is denoted as _SR Image A_ , and
is a high quality reconstruction of the input image created by the downsampled
replicas as the only input to the model.

###  3.2 LPCN-SR+

In addition to the downsampled replicas created by the lossless pooling, the
original bicubic version of the image can also be incorporated in the network,
and provide more information for creating a higher quality SR image. This
process is depicted using the dashed lines and connections in Figure 4,
complementing the model described previously. The first step after the bicubic
filtering is a convolution layer with 64 filters that results in a feature map
of size $(H,W,64)$. This feature map is then fed to the same encoder-decoder
network described earlier with the same weights. We apply weight sharing for
this section of the model in order to avoid extra complexity and having too
many network parameters. The output of the encoder-decoder network will be a
feature map of size $(H,W,64)$, which is then fed to a single kernel
convolution layer, that results in a high quality SR image, denoted as _SR
Image B_ in the figure.

The two created SR images, _SR Image A_ and _SR Image B_ , are then combined
using a single kernel convolution layer with the kernel size of $1\times 1$ to
create the _Final SR Image_. The final convolution layer operates as an
averaging mechanism to mix the two created SR images. It is worth noting, that
the dashed section of the model in Figure 4 is essentially a similar concept
to the REDNet model proposed in [12].

###  3.3 Training

Training the proposed SR model is performed by solving an optimization problem
to minimize the error between the ground truth labels and the network outputs.
The training for the basic and the full models can be performed separately.
For both cases, the training labels are a set of high resolution image samples
$\mathbf{X}$, and the network outputs are the high quality high resolution
images $\mathbf{X}^{\ast}$ generated by the model (_SR Image A_ for LPCN-SR
and _Final SR Image_ for LPCN-SR+). The network outputs can be formulated as
the following:

$\mathbf{X}^{\ast}={\boldsymbol{\theta}}_{m}(\mathbf{Y})$ (3)

where $\mathbf{Y}$ is the input low resolution image, $\boldsymbol{\theta}$ is
the end-to-end SR model encompassing all the parameters, and $m$ defines the
network model of operation with is either LPCN-SR or LPCN-SR+.

Table 1: Quality and complexity analysis of the proposed method and state-of-the-art approaches for the scaling factor of 4. |  | Bicubic | SRCNN | ESPCN | FSRCNN | REDNet | LPCN-SR | LPCN-SR+
---|---|---|---|---|---|---|---|---
Set 5 | PSNR | 28.44 | 30.09 | 30.41 | 30.58 | 31.38 | 31.44 | 31.71
SSIM | 0.8110 | 0.8520 | 0.8590 | 0.8658 | 0.8820 | 0.8833 | 0.8872
GPU time | - | 0.57 | 0.45 | 0.55 | 0.61 | 0.54 | 0.83
CPU time | - | 0.11 | 0.02 | 0.02 | 0.27 | 0.27 | 1.17
Set 14 | PSNR | 26.00 | 27.18 | 27.37 | 27.52 | 27.98 | 27.98 | 28.12
SSIM | 0.7009 | 0.7385 | 0.7457 | 0.7506 | 0.7636 | 0.7643 | 0.7686
GPU time | - | 0.60 | 0.46 | 0.58 | 0.70 | 0.56 | 1.03
CPU time | - | 0.22 | 0.03 | 0.03 | 0.55 | 0.53 | 2.39
BSD 100 | PSNR | 25.89 | 26.64 | 26.77 | 26.85 | 27.16 | 27.14 | 27.26
SSIM | 0.6651 | 0.6994 | 0.7073 | 0.7100 | 0.7207 | 0.7215 | 0.7253
GPU time | - | 0.57 | 0.44 | 0.57 | 0.68 | 0.59 | 0.96
CPU time | - | 0.15 | 0.02 | 0.02 | 0.36 | 0.36 | 1.57

The mean squared error, defined as the following, is employed as the cost
function for the training process.

$J_{MSE}(\mathbf{X},\mathbf{Y},\boldsymbol{\theta}_{m})=\frac{1}{N}\sum_{i=0}^{N}\left({\mathbf{X}}_{i}-{\boldsymbol{\theta}}_{m}({\mathbf{Y}}_{i})\right)^{2}$
(4)

with $N$ denoting the total number of training samples. The training input
samples are created by downsampling the high resolution samples, and upscaling
them back to the original resolution by bicubic interpolation. The scaling
factor can be fixed to focus on training a particular scaling, or
alternatively can include several values to cover a wide range of scaling.

##  4 Experiments

We focused the experiments on the SR with a scaling factor of 4, which is a
challenging factor in image scaling, and it is also the basis for most of the
SR evaluations. We used the DIV2K data set [1] as our training set, which
comprises 800 high quality images. The images were partitioned into $96\times
96$ samples with a stride of 80, which led to around 325,000 training sample
pairs. We used Adam optimizer [9] for training the model with a learning rate
of 0.0001, $\beta_{1}$ of 0.9, $\beta_{2}$ of 0.999, $\epsilon$ of $10^{-8}$
and a training batch size of 128. The proposed model, along with the existing
state-of-the-art approaches, were implemented using
TensorFlow111https://www.tensorflow.org/ library.

###  4.1 Quantitative Evaluations

To compare the presented model with the existing solutions, we used Set 5, Set
14 and BSD 100 data sets, which are widely used in SR task. We compared the
approach with well-known deep learning-based SR models including SRCNN [3],
ESPCN [13], FSRCNN [5], and REDNet [12]. All the models were implemented and
trained according to the provided information in the literature. All the
trainings were performed on Tesla K80 NVIDIA GPUs, and all the tests were
performed on a machine with a generic Intel Core i7-6700 CPU with a 3.40GHz
clock and 16GB RAM, and a GeForce GTX 1070 GPU.

Table 1 summarizes the performance results of the presented model, in
comparison with state-of-the-art methods. The quality metrics are the Peak
Signal-to-Noise Ratio (PSNR) and Structural SIMilarity (SSIM) index. According
to the results, the proposed approach can outperform the baseline models in
all datasets, promising a high quality enhancement for still images.

The basic LPCN-SR model can perform as good as the best existing model,
REDNet, and in some cases outperform it slightly. The strength of this model
however is in the lower computation cost on GPU, which is due to using
lossless pooling, that results in downscaling of the input, and consequently
performing all the convolutional processes in a lower resolution than the
native target resolution. The full LPCN-SR+ model, on the other hand, shows a
solid outperformance on all data sets and provides major improvements in PSNR
and SSIM results. The computation cost is however higher than the existing
models due to the structure of the model, and incorporating multiple input
signals in the approach.

Bicubic: 25.11 dBESPCN: 25.72 dBREDNet: 25.68 dBLPCN-SR+: 25.80 dBGround
TruthBicubic: 21.63 dBESPCN: 22.58 dBREDNet: 22.86 dBLPCN-SR+: 22.93 dBGround
Truth Figure 5: Upscaling _Barbara_ and _Comic_ from Set 14 with a factor of
4. Bicubic: 27.32 dBESPCN: 29.79 dBREDNet: 31.27 dBLPCN-SR+: 31.82 dBGround
TruthBicubic: 21.76 dBESPCN: 23.74 dBREDNet: 24.91 dBLPCN-SR+: 25.14 dBGround
Truth Figure 6: Upscaling _Monarch_ and _PPT3_ from Set 14 with a factor of 4.

###  4.2 Qualitative Evaluations

We also examined the subjective quality of the enhanced images on the test
content, as objective metrics cannot always grasp the intricacies detected by
human eyes. Application of the proposed approach resulted in clear visual
improvements in the reconstructed high resolution images, some of which are
presented in Figure 5 and Figure 6. In these examples only the luma signal is
upsampled by the proposed SR approach, and the color components are scaled
using bicubic interpolation.

One of the most challenging scenarios in SR is coping with the low resolution
images with major aliasing distortions. The _Barbara_ image from Set 14 of the
test sets is an extreme example for this case. Upscaling the downsampled
version of this image can result in magnifying those aliasing artifacts in
most cases. However, as depicted in Figure 5, our proposed model does a good
job in restoring some of the content that is highly distorted by the
downsampling process, and is outperforming the other SR approaches. Another
example is in the _PPT3_ image, depicted in Figure 6, which reconstruction of
a distorted patterned texture is shown, and LPCN-SR+ provides a better
prediction of the original image compared to the state-of-the-art models.

##  5 Conclusions

Still image SR can benefit from application of auxiliary correlated inputs
derived from the original low resolution source input. The process of creating
self-replicas and their incorporation in the CNNs is performed by a novel
lossless pooling layer, that generates multiple downscaled versions of the
input image, which are later fused in the general SR framework. The presented
LPCN-SR model can perform as good as the state of the art with a reduced
computation cost on GPUs, and the full LPCN-SR+ outperforms the existing
approaches, and promises high quality and accurate image upscaling.

## Acknowledgments

The work described in this paper has been conducted within the project
COGNITUS. This project has received funding from the European Union’s Horizon
2020 research and innovation program under grant agreement No 687605\. This
research utilized Queen Mary’s Apocrita HPC facility, supported by QMUL
Research-IT. The authors gratefully acknowledge the support of NVIDIA
Corporation with the donation of the Titan X Pascal GPU used for this
research.

## References

  * [1] E. Agustsson and R. Timofte.  NTIRE 2017 challenge on single image super-resolution: Dataset and study.  In The IEEE Conference on Computer Vision and Pattern Recognition (CVPR) Workshops, 2017.
  * [2] J. Caballero, C. Ledig, A. P. Aitken, A. Acosta, J. Totz, Z. Wang, and W. Shi.  Real-time video super-resolution with spatio-temporal networks and motion compensation.  In 2017 IEEE Conference on Computer Vision and Pattern Recognition, pages 2848–2857, 2017.
  * [3] C. Dong, C. C. Loy, K. He, and X. Tang.  Learning a Deep Convolutional Network for Image Super-Resolution.  In European Conference on Computer Vision (ECCV) 2014, pages 184–199, 2014.
  * [4] C. Dong, C. C. Loy, K. He, and X. Tang.  Image Super-Resolution Using Deep Convolutional Networks.  IEEE Trans. Pattern Anal. Mach. Intell., 38(2):295–307, Feb. 2016\.
  * [5] C. Dong, C. C. Loy, and X. Tang.  Accelerating the Super-Resolution Convolutional Neural Network.  In European Conference on Computer Vision (ECCV) 2016, pages 184–199, 2016.
  * [6] A. Kappeler, S. Yoo, Q. Dai, and A. K. Katsaggelos.  Video Super-Resolution With Convolutional Neural Networks.  IEEE Transactions on Computational Imaging, 2(2):109–122, June 2016\.
  * [7] J. Kim, J. Kwon Lee, and K. Mu Lee.  Accurate Image Super-Resolution Using Very Deep Convolutional Networks.  In The IEEE Conference on Computer Vision and Pattern Recognition (CVPR), June 2016.
  * [8] J. Kim, J. Kwon Lee, and K. Mu Lee.  Deeply-Recursive Convolutional Network for Image Super-Resolution.  In The IEEE Conference on Computer Vision and Pattern Recognition (CVPR), June 2016.
  * [9] D. Kingma and J. Ba.  Adam: A Method for Stochastic Optimization.  In International Conference on Learning Representations, 12 2014\.
  * [10] C. Ledig, L. Theis, F. Huszar, J. Caballero, A. Cunningham, A. Acosta, A. Aitken, A. Tejani, J. Totz, Z. Wang, et al.  Photo-Realistic Single Image Super-Resolution Using a Generative Adversarial Network.  In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pages 4681–4690, 2017.
  * [11] O. Makansi, E. Ilg, and T. Brox.  End-to-End Learning of Video Super-Resolution with Motion Compensation.  In German Conference on Pattern Recognition (GCPR) 2017, 2017.
  * [12] X. Mao, C. Shen, and Y. Yang.  Image Restoration Using Very Deep Convolutional Encoder-Decoder Networks with Symmetric Skip Connections.  In Advances in Neural Information Processing Systems (NIPS), pages 2802–2810, 2016.
  * [13] W. Shi, J. Caballero, F. Huszar, J. Totz, A. P. Aitken, R. Bishop, D. Rueckert, and Z. Wang.  Real-Time Single Image and Video Super-Resolution Using an Efficient Sub-Pixel Convolutional Neural Network.  In 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, pages 1874–1883, 2016.
  * [14] X. Tao, H. Gao, R. Liao, J. Wang, and J. Jia.  Detail-Revealing Deep Video Super-Resolution.  In The IEEE International Conference on Computer Vision (ICCV), 2017\.
  * [15] Z. Wang, Y. Yang, Z. Wang, S. Chang, W. Han, J. Yang, and T. S. Huang.  Self-Tuned Deep Super Resolution.  In CVPR Workshops, pages 1–8. IEEE Computer Society, 2015.


3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y}=U$
$\displaystyle=\mathit{id}_{a\otimes b}(U)$

     * •

$\rho_{a\otimes
b,c}=(\rho_{a,c}\otimes\mathit{id}_{b})\circ(\mathit{id}_{a}\otimes\rho_{b,c})$

Let $U\subseteq[Y+Z+W]^{a+b+c}$, then:

$\displaystyle((\rho_{a,c}\otimes\mathit{id}_{b})\circ(\mathit{id}_{a}\otimes\rho_{b,c}))(U)$
$\displaystyle=(\rho_{a,c}\otimes\mathit{id}_{b})(\mathit{id}_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y}}\rho_{b,c}(\vec{U}_{Y}))$
$\displaystyle=(\rho_{a,c}\otimes\mathit{id}_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}(\overrightarrow{(\vec{U}_{Y})}_{Z}\mathop{\cup_{W}}\overleftarrow{(\vec{U}_{Y})}_{Z}))$
$\displaystyle=(\rho_{a,c}\otimes\mathit{id}_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}(\vec{U}_{Y+Z}\mathop{\cup_{W}}\overleftarrow{(\vec{U}_{Y})}_{Z}))$
$\displaystyle=(\rho_{a,c}\otimes\mathit{id}_{b})((\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y+Z})\mathop{\cup_{Y+W}}\overleftarrow{(\vec{U}_{Y})}_{Z}))$
$\displaystyle=\rho_{a,c}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y+Z})\mathop{\cup_{W+Y}}\mathit{id}_{b}(\overleftarrow{(\vec{U}_{Y})}_{Z})$
$\displaystyle=(\vec{U}_{Y+Z}\mathop{\cup_{W}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{W+Y}}\overleftarrow{(\vec{U}_{Y})}_{Z}$
$\displaystyle=\vec{U}_{Y+Z}\mathop{\cup_{W}}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\overleftarrow{(\vec{U}_{Y})}_{Z})$
$\displaystyle=\vec{U}_{Y+Z}\mathop{\cup_{W}}(\overleftarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}\mathop{\cup_{Y}}\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y})$
$\displaystyle=\vec{U}_{Y+Z}\mathop{\cup_{W}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z}=\rho_{a\otimes b,c}(U)$

where we use $\overrightarrow{(\vec{U}_{Y})}_{Z}=\vec{U}_{Y+Z}$,
$\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}=\overleftarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}$ and
$\overleftarrow{(\vec{U}_{Y})}_{Z}=\overrightarrow{(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y+Z})}_{Y}$.

  5. (5)

gs-monoidality:

     * •

$!_{e}=\nabla_{e}=\mathit{id}_{e}$

In this case $\emptyset$ is the only possible argument and we have:

$!_{e}(\emptyset)=\emptyset=\mathit{id}_{e}(\emptyset)=\emptyset=\emptyset\mathop{\cup_{\emptyset}}\emptyset=\nabla_{e}(\emptyset)$

     * •

coherence axioms:

For $U\subseteq[Y]^{a}$, we note that
$\overleftarrow{(U\cup_{Y}U)}_{Y}=\overrightarrow{(U\cup_{Y}U)}_{Y}=U$.

       * –

$(\mathit{id}_{a}\otimes\nabla_{a})\circ\nabla_{a}=(\nabla_{a}\otimes\mathit{id}_{a})\circ\nabla_{a}$

Let $U\subseteq[Y]^{a}$, then:

$\displaystyle((\mathit{id}_{a}\otimes\nabla_{a})\circ\nabla_{a})(U)=(\mathit{id}_{a}\otimes\nabla_{a})(U\mathop{\cup_{Y}}U)$
$\displaystyle=\mathit{id}_{a}(U)\mathop{\cup_{Y}}\nabla_{a}(U)=U\mathop{\cup_{Y}}(U\mathop{\cup_{Y}}U)$
$\displaystyle=(U\mathop{\cup_{Y}}U)\mathop{\cup_{Y+Y}}U=\nabla_{a}(U)\mathop{\cup_{Y+Y}}\mathit{id}_{a}(U)$
$\displaystyle=(\nabla_{a}\otimes\mathit{id}_{a})(U\mathop{\cup_{Y}}U)=(\nabla_{a}\otimes\mathit{id}_{a})(\nabla_{a}(U))$

       * –

$\mathit{id}_{a}=(\mathit{id}_{a}\otimes!_{a})\circ\nabla_{a}$

Let $U\subseteq[Y]^{a}$, then:

$\displaystyle((\mathit{id}_{a}\otimes!_{a})\circ\nabla_{a})(U)=(\mathit{id}_{a}\otimes!_{a})(U\mathop{\cup_{Y}}U)$
$\displaystyle=\mathit{id}_{a}(U)\mathop{\cup_{Y}}!_{a}(U)=\mathit{id}_{a}(U)\mathop{\cup_{Y}}\emptyset$
$\displaystyle=\mathit{id}_{a}(U)$

       * –

$\rho_{a,a}\circ\nabla_{a}=\nabla_{a}$

Let $U\subseteq[Y]^{a}$, then:

$(\rho_{a,a}\circ\nabla_{a})(U)=\rho_{a,a}(U\mathop{\cup_{Y}}U)=U\mathop{\cup_{Y}}U=\nabla_{a}(U)$

     * •

monoidality axioms:

       * –

$!_{a\otimes b}=!_{a}\otimes!_{b}$

Let $U\subseteq[Y+Z]^{a+b}$, then:

$\displaystyle!_{a\otimes b}(U)$
$\displaystyle=\emptyset=\emptyset\mathop{\cup_{\emptyset}}\emptyset=!_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{\emptyset}}!_{b}(\vec{U}_{Y})$
$\displaystyle=(!_{a}\otimes!_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y})=(!_{a}\otimes!_{b})(U)$

       * –

$\nabla_{a}\otimes\nabla_{b}=(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})\circ\nabla_{a\otimes
b}$

Let $U\subseteq[Y+Z]^{a+b}$, then:

$\displaystyle(\mathit{id}_{a}\otimes\rho_{b,a}\otimes\mathit{id}_{b})(\nabla_{a\otimes
b}(U))$
$\displaystyle=(\mathit{id}_{a}\otimes(\rho_{b,a}\otimes\mathit{id}_{b}))(U\mathop{\cup_{Y+Z}}U)$
$\displaystyle=\mathit{id}_{a}(\overleftarrow{(U\mathop{\cup_{Y+Z}}U)}_{Y})\mathop{\cup_{Y}}(\rho_{b,a}\otimes\mathit{id}_{b})(\overrightarrow{(U\mathop{\cup_{Y+Z}}U)}_{Y})$
$\displaystyle=\mathit{id}_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y}}(\rho_{b,a}\otimes\mathit{id}_{b})(\overrightarrow{(U\mathop{\cup_{Y+Z}}U)}_{Y})$
$\displaystyle=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}(\rho_{b,a}\otimes\mathit{id}_{b})(\overrightarrow{(U\mathop{\cup_{Y+Z}}U)}_{Y})$
$\displaystyle=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}(\rho_{b,a}\otimes\mathit{id}_{b})((\vec{U}_{Y}\mathop{\cup_{Z}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z+Y}}\vec{U}_{Y})$
$\displaystyle=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}((\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y})\mathop{\cup_{Y+Z}}\vec{U}_{Y})$
$\displaystyle=(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y+Y}}(\vec{U}_{Y}\mathop{\cup_{Z}}\vec{U}_{Y})$
$\displaystyle=\nabla_{a}(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Y+Y}}\nabla_{b}(\vec{U}_{Y})$
$\displaystyle=(\nabla_{a}\otimes\nabla_{b})(\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern
2.0mu$}}$}\mkern-2.0mu}_{Y}\mathop{\cup_{Y}}\vec{U}_{Y})=(\nabla_{a}\otimes\nabla_{b})(U)$

where we use the fact that
$\overleftarrow{(U\mathop{\cup_{Y+Z}}U)}_{Y}=\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y}$ and
$\overrightarrow{(U\mathop{\cup_{Y+Z}}U)}_{Y}=(\vec{U}_{Y}\mathop{\cup_{Z}}\mathchoice{\mkern
3.0mu\reflectbox{$\displaystyle\vec{\reflectbox{$\mkern-3.0mu\displaystyle
U\mkern 3.0mu$}}$}\mkern-3.0mu}{\mkern
3.0mu\reflectbox{$\textstyle\vec{\reflectbox{$\mkern-3.0mu\textstyle U\mkern
3.0mu$}}$}\mkern-3.0mu}{\mkern
2.0mu\reflectbox{$\scriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}{\mkern
2.0mu\reflectbox{$\scriptscriptstyle\vec{\reflectbox{$\mkern-2.0mu\scriptscriptstyle
U\mkern 2.0mu$}}$}\mkern-2.0mu}_{Y})\mathop{\cup_{Z+Y}}\vec{U}_{Y}$.

Finally, the approximation $\\#$ is indeed gs-monoidal, i.e., it preserves all
the additional structure (tensor, symmetry, unit, duplicator and discharger).

[$\\#$ is gs-monoidal] $\\#\colon\mathbb{C}_{f}\to\mathbb{A}_{f}$ is a gs-
monoidal functor.

######  Proof 7.4.

We write
$e^{\prime},\otimes^{\prime},!^{\prime},\nabla^{\prime},\rho^{\prime}$ for the
corresponding operators in category $\mathbb{A}_{f}$. Note that by definition
$e=e^{\prime}$ and $\otimes$, $\otimes^{\prime}$ agree on objects.

First, categories $\mathbb{C}_{f}$ and $\mathbb{A}_{f}$ are gs-monoidal by
Theorem 4 and 7.2.

Furthermore we verify that:

  1. (1)

monoidality:

     * •

$\\#(e)=e^{\prime}$

We have $\\#(e)=e=e^{\prime}$

     * •

$\\#(a\otimes b)=\\#(a)\otimes^{\prime}\\#(b)$

We have:

$\\#(a\otimes b)=a\otimes b=\\#(a)\otimes^{\prime}\\#(b)$

  2. (2)

symmetry:

     * •

$\\#(\rho_{a,b})=\rho^{\prime}_{\\#(a),\\#(b)}$

Let $U\subseteq[Y+Z]^{a+b}$, then for sufficiently small $\delta\sqsupset 0$
(note that such $\delta$ exists due to finiteness):

$\displaystyle\\#(\rho_{a,b})(U)$
$\displaystyle=(\rho_{a,b})_{\\#}^{a+b,\delta}(U)$
$\displaystyle=\\{w\in[Z+Y]^{b+a}\mid\rho_{a,b}(a+b)(w)\ominus\rho_{a,b}((a+b)\ominus\delta_{U})(w)\sqsupseteq\delta\\}$
$\displaystyle=\\{w\in[Z+Y]^{b+a}\mid(b+a)(w)\ominus((b+a)\ominus\delta_{\rho^{\prime}_{a,b}(U)})(w)\sqsupseteq\delta\\}$
$\displaystyle=\rho^{\prime}_{a,b}(U)=\rho^{\prime}_{\\#(a),\\#(b)}(U)$

since $\rho_{a,b}$ distributes over componentwise subtraction and
$\rho_{a,b}(\delta_{U})=\delta_{\rho^{\prime}_{a,b}(U)}$. The second-last
equality holds since for all $w$ in the set we have $(b+a)(w)\sqsupset 0$.

  3. (3)

gs-monoidality:

     * •

$\\#(!_{a})=!^{\prime}_{\\#(a)}$

Let $U\subseteq[Y]^{a}$, then for some $\delta$:

$\\#(!_{a})(U)=(!_{a})_{\\#}^{a,\delta}(U)=\emptyset=!^{\prime}_{a}(U)=!^{\prime}_{\\#(a)}(U)$

since the codomain of $(!_{a})_{\\#}^{a,\delta}(U)$ is
$\mathcal{P}(\emptyset)$ and hence the only possible value for
$(!_{a})_{\\#}^{a,\delta}(U)$ is $\emptyset$.

     * •

$\\#(\nabla_{a})=\nabla^{\prime}_{\\#(a)}$

Let $U\subseteq[Y]^{a}$, then for sufficiently small $\delta\sqsupset 0$:

$\displaystyle\\#(\nabla_{a})(U)$
$\displaystyle=(\nabla_{a})^{a,\delta}_{\\#}(U)$
$\displaystyle=\\{w\in[Y+Y]^{a+a}\mid\nabla_{a}(a)(w)\ominus\nabla_{a}(a\ominus\delta_{U})(w)\sqsupseteq\delta\\}$
$\displaystyle=\\{w\in[Y+Y]^{a+a}\mid(a+a)(w)\ominus((a+a)\ominus\delta_{\nabla^{\prime}_{a}(U)})(w)\sqsupseteq\delta\\}$
$\displaystyle=\nabla^{\prime}_{a}(U)=\nabla^{\prime}_{\\#(a)}(U)$

since $\nabla_{a}$ distributes over componentwise subtraction and
$\nabla_{a}(\delta_{U})=\delta_{\nabla^{\prime}_{a}(U)}$. The second-last
equality holds since for all $w$ in the set we have $(a+a)(w)\sqsupset 0$.

##  8\. UDEfix: A Tool for Fixpoints Checks

inline]B: I now used the more extended version from Richard’s thesis. I would
however make the tutorial there a bit shorter (with fewer figures).

###  8.1. Overview

We present a tool, called UDEfix, which exploits gs-monoidality as discussed
before and allows the user to construct functions
$f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Y}$ as a sort of circuit. As basic
components, UDEfix can handle all functions presented in Section 4 (Table 2)
and addition and subtraction by a fixed constant $w$ ($\mathit{add}_{w}$,
$\mathit{sub}_{w}$, both are non-expansive functions). Since the approximation
functor $\\#$ is gs-monoidal, this circuit can be then transformed
automatically, in a compositional way, into the corresponding abstraction
$f_{\\#}^{a}$, for some given $a\in\mathbb{M}^{Y}$. By computing the greatest
fixpoint of $f_{\\#}^{a}$ and checking for emptiness, UDEfix can check whether
$a=\mu f$. In addition, it is possible to check whether a given post-fixpoint
$a$ is below the least fixpoint $\mu f$ (recall that in this case the check is
sound but not complete). The dual checks (for greatest fixpoint and pre-
fixpoints) are implemented as well.

The tool is shipped with pre-defined functions implementing examples
concerning case studies on termination probability, bisimilarity, simple
stochastic games, energy games, behavioural metrics and Rabin automata.

UDEfix is a Windows-Tool created in Python, which can be obtained from
https://github.com/TimoMatt/UDEfix.

Building the desired function $f\colon\mathbb{M}^{Y}\to\mathbb{M}^{Y}$
requires three steps:

  * •

Choosing the MV-algebra $\mathbb{M}$ of interest.

  * •

Creating the required basic functions by specifying their parameters.

  * •

Assembling $f$ from these basic functions.

###  8.2. Tool Areas

Concretely, the GUI of UDEfix is separated into three areas: the Content area,
Building area and Basic-Functions area. Under File-Settings the user can set
the MV-algebra. Currently the MV-chains $[0,k]$ (algebra 1) and
$\\{0,\dots,k\\}$ (algebra 2) for arbitrary $k$ are supported (see Example
3.2)

####  Basic-Functions Area:

The Basic-Functions area (see Figure 5) contains the basic functions,
encompassing those listed in Table 2 in Section 2 as well as addition and
subtraction by a constant $w$. Via drag-and-drop (or right-click) these basic
functions can be added to the Building area to create a Function box. Each
such box requires three (in the case of $\tilde{\mathcal{D}}$ two) Contents:
The Input set, the Output set and an additional required parameter (see Table
3). These Contents can be created in the Content area.

Figure 5. List of basic functions Basic Function | $c_{k}$ | $u^{*}$ | $\min_{\mathcal{R}}/\max_{\mathcal{R}}$ | $\mathit{add}_{w}$ | $\mathit{sub}_{w}$
---|---|---|---|---|---
Req. Parameter | $k\in\mathbb{M}^{Z}$ | $u\colon Z\to Y$ | $R\subseteq Y\times Z$ | $w\in\mathbb{M}^{Y}$ | $w\in\mathbb{M}^{Y}$
Table 3. Additional parameters for the basic functions from Table 2.

Additionally the Basic-Functions area offers functionalities for composing
functions via disjoint union (more concretely, this is handled by the the
auxiliary Higher-Order Function) and the Testing functionality for fixpoint
checks which we will discuss in the next paragraph.

####  Building Area:

The user can connect the created Function boxes to construct the function $f$
of interest. Composing functions is as simple as connecting two Function boxes
in the correct order by mouse-click. Disjoint union is achieved by connecting
two boxes to the same box. Note that Input and Output sets of connected
Function boxes need to match. As an example, in Figure 6 we show how the
function $\mathcal{W}$, discussed in Section 2, for computing the behavioural
distance of a labeled Markov chain can be assembled. The construction exactly
follows the structure of the diagram in Figure 2. Here, the parameters are
instantiated for the labeled Markov chain displayed in Figure 1 (left-hand
side).

Figure 6. Assembling the function $\mathcal{W}$ from Section 2.

The special box Testing is always required to appear at the end. Here, the
user can enter some mapping $a\colon Y\to\mathbb{M}$, test if $a$ is a
fixpoint of the function $f$ of interest and then verify if $a=\mu f$. As
explained before, this is realised by computing the greatest fixpoint of the
approximation $\nu f_{\\#}^{a}$ . In case this is not empty and thus $a\neq\mu
f$, the tool can produce a suitable value which can be used for decreasing
$a$, needed for iterating to the least fixpoint from above (respectively
increasing $a$ for iterating to the greatest fixpoint from below). There is
also support for comparison with pre- and post-fixpoints.

######  Example 8.1.

As an example, consider the left-hand system in Figure 1 and consider the
function $\mathcal{W}$ from Section 2 whose least fixpoint corresponds to the
behavioural distance for a labeled Markov chain.

We now define a fixpoint of $\mathcal{W}$, which is not the least, namely
$d\colon Y\to[0,1]$ with $d(3,3)=0$, $d(1,1)=\nicefrac{{1}}{{2}}$,
$d(1,2)=d(2,1)=d(2,2)=\nicefrac{{2}}{{3}}$ and $1$ for all other pairs. Note
that $d$ is not a pseudo-metric, but is a fixpoint of $\mathcal{W}$. We give a
hint why $d$ is a fixpoint, by exemplarily considering the pair $(1,2)$. Due
to the labels, an optimal coupling for the successors of $1,2$ assigns
$(3,3)\mapsto\nicefrac{{1}}{{3}}$, $(4,4)\mapsto\nicefrac{{1}}{{2}}$,
$(3,4)\mapsto\nicefrac{{1}}{{6}}$. Hence, by the fixpoint equation, we have

$d(1,2)=\nicefrac{{1}}{{3}}\cdot d(3,3)+\nicefrac{{1}}{{2}}\cdot
d(4,4)+\nicefrac{{1}}{{6}}\cdot d(3,4)=\nicefrac{{1}}{{3}}\cdot
0+\nicefrac{{1}}{{2}}\cdot 1+\nicefrac{{1}}{{6}}\cdot
1=\nicefrac{{1}}{{2}}+\nicefrac{{1}}{{6}}=\nicefrac{{2}}{{3}}.$

A similar argument can be made for the remaining pairs.

By clicking Compute in the Testing-box, UDEfix displays that $d$ is a fixpoint
and tells us that $d$ is in fact not the least and not the greatest fixpoint.
It also computes the greatest fixpoints of the approximations step by step
(via Kleene iteration) and displays the results to the user. In this case $\nu
f_{\\#}^{a}=\\{(4,4)\\}$, indicating that the distance $d(4,4)=1$ over-
estimates the true value and can be decreased. The fact that also other pairs
over-estimate their value (but to a lesser degree), will be detected in later
steps in the iteration to the least fixpoint from above.

####  Content Area:

Here the user can create sets, mappings and relations which are used to
specify the basic functions. The user can create a variety of different types
of sets, such as $X=\\{1,2,3,4\\}$, which is a basic set of numbers, and the
set $D=\\{p_{1},p_{2},p_{3},p_{4}\\}$ which is a set of mappings representing
probability distributions. These objects are called Content.

Once Input and Output sets are created we can specify the required parameters
(cf. Table 3) for a function. Here, the created sets can be chosen as domain
and co-domain. Relations can be handled in a similar fashion: Given the two
sets one wants to relate, creating a relation can be easily achieved by
checking some boxes. Some useful in-built relations like“is-element-
of”-relation and projections to the $i$-th component are pre-defined.

By clicking on the icon “+” in a Function box, a new function with the chosen
Input and Output sets is created. The additional parameters (cf. Table 3) have
domains and co-domains which need to be created by the user or are provided by
the chosen MV-algebra.

The Testing function $a$ (i.e., the candidate (pre/post-)fixpoint) is a
mapping as well and can be created as all other functions.

In Figure 7 we give examples of how contents can be created: we show the
creation of a set ($Y=X\times X$), a distance function ($d$) and a relation
($\rho$).

Figure 7. Contents: Set $Y$, Mapping $d$, Relation $\rho$.

###  8.3. Tutorial

We now provide a small tutorial intended to clarify the use of the tool. It
deals with a simple example: a function whose least fixpoint provides the
termination probability of a Markov chain.

We continue Examples 3.5 and 4.8 and consider the Markov chain $(S,T,\eta)$ in
Figure 3.

Remember that the function $\mathcal{T}$, whose least fixpoint is the
termination probability, can be decomposed as follows:

$\mathcal{T}=(\eta^{*}\circ\tilde{\mathcal{D}})\otimes c_{k}$

In order to start, one first chooses the correct MV-algebra under Settings and
creates the sets $S,T,S\setminus T$ (Input and Output sets). The creation of
set $S$ is exemplified in Figure 8 (left-hand side). The tool supports several
types of sets and operators on sets (such as complement, which makes it easy
to create $S\backslash T$. Next, we create the set $D$ of probability
distributions, consisting of the mappings $p_{x},p_{y},p_{z}$. In Figure 8
(right-hand side) we show the creation of $p_{x}$.

Figure 8. Creation of set $S$ and probability distribution $p_{x}$ for the
example.

Now we create the basic function boxes and connect them in the correct way
(see Figure 9). The additional parameters according to Table 3 – in this case
the map $c_{k}$ and the reindexing $\eta^{*}$ based on the successor map – can
be created by clicking the icon “+” in the corresponding box (see Figure 10)
(left-hand side for $k$ and middle for $\eta$).

Figure 9. Assembling the function $\mathcal{T}$.

Figure 10. Creation of the parameters $k$ and $\eta^{*}$ and the greatest
fixpoint $a_{1}=\mu\mathcal{T}$.

We can also assemble several test functions (e.g., possible candidate
fixpoints), among them the greatest fixpoint $a_{1}=\nu\mathcal{T}$ (see
Figure 10, right-hand side).

When testing $a_{1}$ we obtain the results depicted in Figure 11. In fact
$\nu\mathcal{T}_{\\#}^{a_{1}}=\\{y,z\\}\neq\emptyset$, which tells us that
$a_{1}$ is not the least fixpoint.

Figure 11. Checking the candidate fixpoint $a_{1}$.

Similarly, one can test $a_{2}=\mu\mathcal{T}$, the least fixpoint, obtaining
$\nu\mathcal{T}_{\\#}^{a_{2}}=\emptyset$. This allows the user to deduce that
$a_{2}$ is indeed the least fixpoint. As mentioned before, one can also test
whether a pre-fixpoint is below the greatest fixpoint or a post-fixpoint above
the least fixpoint, although such tests are sound but not complete.

##  9\. Conclusion, Related and Future Work

We have shown that a framework originally introduced in [bekp:fixpoint-theory-
upside-down, BEKP:FTUD-journal] for analysing fixpoint of non-expansive
functions over MV-algebras can be naturally cast into a gs-monoidal setting.
The non-expansive functions of interest live in a so-called concrete gs-
monoidal category, their approximations in a gs-monoidal abstract category and
they are related by a gs-monoidal functor $\\#$. We also developed a general
theory for constructing approximations of predicate liftings, which find
natural application in the definition of behavioural metrics over coalgebras.

The compositionality properties arising from the gs-monoidal view of the
theory are at the basis of the development of a prototype tool UDEfix. The
tool allows one to build the concrete function of interest out of some basic
components. Then the approximation of the function can be obtained
compositionally from the approximations of the components and one can check
whether some fixpoint is the least or greatest fixpoint of the function of
interest. Additionally, one use the tool to show that some pre-fixpoint is
above the greatest fixpoint or some post-fixpoint is below the least fixpoint.

#### Related work:

This paper is based on fixpoint theory, coalgebras, as well as on the theory
of monoidal categories. Monoidal categories [ml:categories] are categories
equipped with a tensor. It has long been realized that monoidal categories can
have additional structure such as braiding or symmetries. Here we base our
work on so called gs-monoidal categories [cg:term-graphs-gs-monoidal,
gh:inductive-graph], called s-monoidal in [g:concurrent-term-rewriting]. These
are symmetric monoidal categories, equipped with a discharger and a
duplicator. Note that “gs” originally stood for “graph substitution” as such
categories were first used for modelling term graph rewriting.

We view gs-monoidal categories as a means to compositionally build monotone
non-expansive functions on complete lattices, for which we are interested in
the (least or greatest) fixpoint. Such fixpoints are ubiquitous in computer
science, here we are in particular interested in applications in concurrency
theory and games, such as bisimilarity [s:bisimulation-coinduction],
behavioural metrics [dgjp:metrics-labelled-markov, b:prob-bisimilarity-
distances, cbw:complexity-prob-bisimilarity, bbkk:coalgebraic-behavioral-
metrics] and simple stochastic games [c:algorithms-ssg]. In recent work we
have considered strategy iteration procedures inspired by games for solving
fixpoint equations [bekp:lattice-strategy-iteration].

Fixpoint equations also arise in the context of coalgebra [r:universal-
coalgebra], a general framework for investigating behavioural equivalences for
systems that are parameterized – via a functor – over their branching type
(labelled, non-deterministic, probabilistic, etc.). Here in particular we are
concerned with coalgebraic behavioural metrics [bbkk:coalgebraic-behavioral-
metrics], based on a generalization of the Wasserstein or Kantorovich lifting
[v:optimal-transport]. Such liftings require the notion of predicate liftings,
well-known in coalgebraic modal logics [s:coalg-logics-limits-beyond-journal],
lifted to a quantitative setting [bkp:up-to-behavioural-metrics-fibrations].

#### Future work:

One important question is still open: we defined an approximation $\\#$,
relating the concrete category $\mathbb{C}$ of functions of type
$\mathbb{M}^{Y}\to\mathbb{M}^{Z}$ – where $Y,Z$ might be infinite – to their
approximations, living in $\mathbb{A}$. It is unclear whether $\\#$ is a lax
or even proper functor, i.e., whether it (laxly) preserves composition. For
finite sets functoriality derives from a non-trivial result in [BEKP:FTUD-
journal] and it is unclear whether it can be extended to the infinite case. If
so, this would be a valuable step to extend the theory to infinite sets.

In this paper we illustrated the approximation for predicate liftings via the
powerset and the distribution functor. It would be interesting to study more
functors and hence broaden the applicability to other types of transition
systems.

Concerning UDEfix, we plan to extend the tool to compute fixpoints, either via
Kleene iteration or strategy iteration (strategy iteration from above and
below), as detailed in [bekp:lattice-strategy-iteration]. Furthermore for
convenience it would be useful to have support for generating fixpoint
functions directly from a given coalgebra respectively transition system.

_Acknowledgements:_ We want to thank Ciro Russo who helped us with a question
on the connection of MV-algebras and quantales.

## References

  * [1] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare.  On-the-fly exact computation of bisimilarity distances.  Logical Methods in Computer Science, 13(2:13):1–25, 2017.
  * [2] Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel.  Computing probabilistic bisimilarity distances for probabilistic automata.  Logical Methods in Computer Science, 17(1), 2021.
  * [3] Christel Baier and Joost-Pieter Katoen.  Principles of Model Checking.  MIT Press, 2008.
  * [4] Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König.  Coalgebraic behavioral metrics.  Logical Methods in Computer Science, 14(3), 2018.  Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015).
  * [5] Paolo Baldan, Richard Eggert, Barbara König, Timo Matt, and Tommaso Padoan.  A monoidal view on fixpoint checks.  In ICGT, volume 13961 of Lecture Notes in Computer Science, pages 3–21. Springer, 2023.
  * [6] Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan.  Fixpoint theory – upside down.  Logical Methods in Computer Science, 19(2), 2023.
  * [7] Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan.  A lattice-theoretical view of strategy iteration.  In Proc. of CSL ’23, volume 252 of LIPIcs, pages 7:1–7:19. Schloss Dagstuhl – Leibniz Center for Informatics, 2023.
  * [8] Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan.  Fixpoint theory – upside down.  In Proc. of FOSSACS ’21, pages 62–81. Springer, 2021.  LNCS/ARCoSS 12650.
  * [9] Michel Bauderon and Bruno Courcelle.  Graph expressions and graph rewritings.  Mathematical Systems Theory, 20(1):83–127, 1987.
  * [10] Filippo Bonchi, Barbara König, and Daniela Petrişan.  Up-to techniques for behavioural metrics via fibrations.  In Proc. of CONCUR ’18, volume 118 of LIPIcs, pages 17:1–17:17. Schloss Dagstuhl – Leibniz Center for Informatics, 2018.
  * [11] Symeon Bozapalidis and Antonios Kalampakas.  An axiomatization of graphs.  Acta Informatica, 41:19–61, 2004.
  * [12] Di Chen, Franck van Breugel, and James Worrell.  On the complexity of computing probabilistic bisimilarity.  In Proc. of FOSSACS ’12, pages 437–451. Springer, 2012.  LNCS/ARCoSS 7213.
  * [13] Anne Condon.  On algorithms for simple stochastic games.  In Advances In Computational Complexity Theory, volume 13 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 51–71, 1990.
  * [14] Andrea Corradini and Fabio Gadducci.  An algebraic presentation of term graphs, via gs-monoidal categories.  Appl. Categor. Struct., 7:299–331, 1999.
  * [15] Patrick Cousot and Radhia Cousot.  Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints.  In Proc. of POPL ’77, pages 238–252. ACM, 1977.
  * [16] Patrick Cousot and Radhia Cousot.  Temporal abstract interpretation.  In Mark N. Wegman and Thomas W. Reps, editors, Proc. of POPL ’00, pages 12–25. ACM, 2000.
  * [17] Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden.  Metrics for labelled Markov processes.  Theoretical Computer Science, 318:323–354, 2004.
  * [18] Antonio Di Nola and Brunella Gerla.  Algebras of Lukasiewicz’s logic and their semiring reducts.  In Idempotent Mathematics and Mathematical Physics, volume 377 of Proceedings of the AMS, pages 131–144, 2005.
  * [19] H. Ehrig, M. Pfender, and H. Schneider.  Graph grammars: An algebraic approach.  In Proc. 14th IEEE Symp. on Switching and Automata Theory, pages 167–180, 1973.
  * [20] Tobias Fritz, Fabio Gadducci, Davide Trotta, and Andrea Corradini.  From gs-monoidal to oplax cartesian categories: Constructions and functorial completeness.  Applied Categorical Structures (2023) 31:42, 31(42), 2023.
  * [21] Fabio Gadducci.  On The Algebraic Approach To Concurrent Term Rewriting.  PhD thesis, University of Pisa, 1996.
  * [22] Fabio Gadducci and Reiko Heckel.  An inductive view of graph transformation.  In Recent Trends in Algebraic Development Techniques, 12th International Workshop, WADT ’97, pages 223–237. Springer-Verlag, 1997.  LNCS 1376.
  * [23] Barbara König.  Hypergraph construction and its application to the static analysis of concurrent systems.  Mathematical Structures in Computer Science, 12(2):149–175, 2002\.
  * [24] Saunders Mac Lane.  Categories for the Working Mathematician.  Springer-Verlag, 1971.
  * [25] Daniele Mundici.  MV-algebras. A short tutorial.  Available at http://www.matematica.uns.edu.ar/IXCongresoMonteiro/Comunicaciones/Mundici_tutorial.pdf.
  * [26] Dirk Pattinson.  Coalgebraic modal logic: soundness, completeness and decidability of local consequence.  Theoretical Computer Science, 309(1):177–193, 2003.
  * [27] J.J.M.M. Rutten.  Universal coalgebra: a theory of systems.  Theoretical Computer Science, 249:3–80, 2000.
  * [28] Davide Sangiorgi.  Introduction to Bisimulation and Coinduction.  Cambridge University Press, 2011.
  * [29] Lutz Schröder.  Expressivity of coalgebraic modal logic: The limits and beyond.  Theoretical Computer Science, 390:230–247, 2008.
  * [30] Alfred Tarski.  A lattice-theoretical theorem and its applications.  Pacific Journal of Mathematics, 5:285–309, 1955.
  * [31] Franck van Breugel.  Probabilistic bisimilarity distances.  ACM SIGLOG News, 4(4):33–51, 2017.
  * [32] Cédric Villani.  Optimal Transport – Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics.  Springer, 2009.
  * [33] Paul Wild and Lutz Schröder.  Characteristic logics for behavioural hemimetrics via fuzzy lax extensions.  Logical Methods in Computer Science, 18(2), 2022.