# Influence of Dataset Parameters on the Performance of Direct UE Positioning
via Deep Learning

Baptiste Chatelier, Vincent Corlay, Cristina Ciochina, Fallou Coly, and Julien
Guillet  Mitsubishi Electric R&D Centre Europe, Rennes, France. E-mail:
<EMAIL_ADDRESS>
###### Abstract

User equipment (UE) positioning accuracy is of paramount importance in current
and future communications standard. However, traditional methods tend to
perform poorly in non line of sight (NLoS) scenarios. As a result, deep
learning is a candidate to enhance the UE positioning accuracy in NLoS
environments. In this paper, we study the efficiency of deep learning on the
3GPP indoor factory (InF) statistical channel. More specifically, we analyse
the impacts of several key elements on the positioning accuracy: the type of
radio data used, the number of base stations (BS), the size of the training
dataset, and the generalization ability of a trained model.

###### Index Terms:

UE positioning, deep learning, 3GPP indoor factory, 5G NR.

##  I Introduction

Recent advances in modern factories, such as the industrial internet of
things, have allowed the emergence of automated guided vehicles (AGV). Such
AGV require extremely precise positioning in real-time. However, indoor
scenarios, and particularly indoor factories, are challenging for positioning:
They are mainly NLoS scenarios.

Unfortunately, conventional positioning techniques used in the 5G NR releases
[2] perform poorly in NLoS scenarios: Typically, the 90$\%$ quantile of the
positioning error111Called the $Q(0.9)$ value in this paper, see Section III
for the definition. is greater than 15m, see Proposal 5.9-1 in [6]. To address
this issue, the radio acess nework working group 1 (RAN1) from 3GPP, the
standardisation body for 5G, opened a study item on the use of machine
learning techniques for UE positioning in InF scenarios [7]. A recent “summary
of evaluation on AI/ML for positioning accuracy enhancement” is available in
[6]. One can also refer to [4] for a survey on the use of AI/ML for Indoor
Positioning.

In this paper, we investigate the deep learning approach for direct UE
positioning in highly NLoS scenarios. On the one hand, the performance of a
deep learning model highly depends on the training dataset. On the other hand,
there may be strong constraints on the data available for the training in a 5G
context: sparse measurements in a given scene, specific or noisy radio signals
used, etc. As a result, it is critical to assess the sensitivity and
robustness of this positioning method to the dataset parameters.

Similarly to the 3GPP RAN1, data from statistical channels are considered to
assess the deep learning efficiency, namely the 3GPP InF channel[8]. This
framework is presented in Section II. In Section III, we then report
simulation results to highlight the influence on the positioning performance
of the four following aspects:

  * •

The type of radio signal: We consider both the path gain (PG) and the channel
impulse response (CIR) as input data to infer the associated position.

  * •

The number of BS: The baseline performance are presented with 18 BS as
described in the 3GPP statistical channel. We also investigate the positioning
performance of the PG and CIR with a reduced number of BS.

  * •

The dataset size: We analyse the influence of the dataset size on the
positioning accuracy.

  * •

The generalization abilities of the trained models: We show the positioning
performance of a model, trained with data from a specific factory, for a UE in
another factory. We consider two cases: without fine tuning on the new factory
and with fine tuning (in other words, transfer learning).

Some of these aspects have also been investigated in the scope of the 3GPP
study on this topic, such as the positioning performance based on the CIR and
a dataset of size of 80 000, as well as some aspects of the generalization
abilities [8]. However, to the best of the author’s knowledge, the performance
with the PG, the influence of the number of BS, the influence of the dataset
size, and the transfer learning abilities of the models have not yet been
investigated.

Note that some other works also consider alternative signals for UE
localization in the InF scenario, such as [5] where the authors consider the
carrier phase.

| Number of data available | Number of scenes available | Model Accuracy | Model specificity
---|---|---|---|---
True measurements | - | \- - | +++ | \- - -
Digital twin | + | + | ++ | -
Statistical channel | ++ | ++ | + | +
TABLE I: Assessment of the possible approaches to generate datasets in order
to train a neural network. The sign $+$ stands for strength and $-$ for
weakness.

##  II Presentation of the framework

###  II-A Direct UE positioning

We consider an uplink communication where a UE broadcasts a signal to several
base stations (BS). The devices have only one antenna. The horizontal
coordinates of a UE at position $k$ is denoted by
$\mathbf{p}_{k}=\left(x_{k},y_{k}\right)$.

The goal is to train a neural network at the network side to output an
estimate $\hat{\mathbf{p}}_{k}$ given the channel measurements made by the BS
as input. This approach is commonly called direct positioning or fingerprint
positioning.

###  II-B Possible approaches to model a radio channel

In order to train and assess the performance of a neural network, one needs to
create a dataset of channel measurements. Several approaches can be envisioned
for this dataset creation.

Firstly, measurements from true channels can be realized. These measurements
can be performed offline by engineers or online by BS with the use of 5G NR
positioning reference signals, collected e.g., via the location management
function (LMF) of the 5G core network.

A second approach consists in collecting measurements from a simulated radio
channel in a digital twin. This requires implementing a digital twin of the
considered scenario. The digital twin can be simplified or advanced.

Finally, statistical channels can be used to generate the datasets. In this
case, the channel parameters are random variables whose statistics are chosen
to represent one category of channels. For instance, the 3GPP InF channel
specifies specific probabilities, e.g., the LoS/NLoS status, which are
consistent with the probabilities encountered in true factories. Then, one
realization of this statistical channel represents one virtual factory. This
approach is used in the study item of 3GPP mentioned in the introduction.

In Table I, we rate the different approaches according to the following
criteria: the number of data available, the number of different scenes
available, the model accuracy, and the model specificity (whether the results
apply only to the considered scenario or if they allow to establish rules
valid for other scenarios). The choice of the model depends on the goal of the
study: studying the neural network in a specific scenario, or in a variety of
scenarios, pre-training a model, etc.

As an example, in [1] pre-training of a model is done on a very simplified
digital-twin (where only the path loss as a function of a distance is
implemented). Then, fine tuning is performed with real measurements. The
drawback of this approach is the following: It is difficult to state if the
results hold for any NLoS environment or just for the one used to collect the
measurements

In this study, we use the statistical approach. As reported in Table I, the
main strength of this approach is to provide a large number of scenes from one
category, with flexibility on the number of data per scene. It is thus suited
to a study of the influence of several dataset parameters on the deep
learning-based positioning accuracy. More specifically, the 3GPP InF scenario
is considered. This latter scenario is selected because of its highly NLoS
characteristics, see Figure 2 and related discussion in Section II-C2.

###  II-C Considered statistical channel

We consider the 3GPP InF-DH scenario as described in TR 38.901 [8]. This is a
highly NLoS scenario due to many (virtual) clutters.

####  II-C1 3GPP channel model

Similarly to standard approaches, the 3GPP statistical channel is modelled by
three main components: 1-The path loss, which represents the attenuation due
to the distance between the BS and UE. 2-The shadowing (large-scale) fading,
caused by long-term fluctuations of the received power due to partial
obstructions. 3-The fast (small-scale) fading due to multipath propagation.
Accordingly, the coefficients of the CIR are generated by three categories of
variables:

  * •

The LoS/NLoS propagation condition, modelled by a Bernoulli random variable.
Given a LoS or NLoS realization for a position, the path loss formula is then
a deterministic function of the distance and the frequency.

  * •

The large-scale parameters (LSP): They represent realizations of both the
shadow fading and parameters used to generate the small-scale parameters,
e.g., the delay spread, the angular spread, Ricean K factor. They can be
understood as general statistical properties of the channel.

  * •

The small-scale parameters (SSP): They are variables used to generate the
clusters and rays, e.g., the delays, the cluster power, the arrival and
departure angles. They represent detailed channel characteristics.

The clusters and rays (simulating a multipath propagation) are then used to
generate the CIR channel coefficients.

On the one hand, the LSP and SSP are slowly varying parameters (both in time
and space), e.g., order of the meter. On the other hand, theses parameters
induce fast fading, e.g., order of the wavelength. This is interesting in the
scope of the considered problem: If the resolution order of the positioning
system is higher than the wavelength, the fast fading induced by the SSP
parameters appears to be completely random. A positioning system based on the
channel coefficients (i.e, the CIR) should therefore learn to ignore (or
average) some of these variations.

An alternative would be to infer the position based on the LSP or SSP, which
(again) are more slowly varying. However, since the SSP are detailed channel
characteristics, it is difficult to deduce them from the channel coefficients.
The LSP are more general characteristics which should be easier to obtain by
averaging the channel coefficients over several dimensions.

As an example, let us define the the path gain (PG) as the shadowing minus the
path loss (in dB). While this quantity has no physical reality, it can be
understood as the average over the small-scale fading of the received power
(assuming ideal omni directional antennas and unit transmit power). As this
quantity is slowly varying, it should not appear as random to the system.
Nevertheless, the PG does not provide an information as rich as the CIR, which
may be required for very-accurate positioning. Consequently, it is interesting
to compare positioning performance based on the PG and the CIR.

Spatial consistency, as specified in TR 38.901 [8], is required for a
positioning study. This means, for instance, that the autocorrelation of the
shadow fading random variable should be an exponential random variable (see
Eq. 7.4-5 in TR 38.901). In our implementation, the spatial consistency is
enabled for the three categories of variables listed above. The model should
also respect spatial coherence meaning that a random variable realization at a
given position at two different instants should be the same or at least
statistically dependent.

####  II-C2 InF specificity

The topology of the considered factory in the 3GPP InF model is a rectangular
area of width $W=60$m, length $L=120$m and height $H=10$m. There are 18 BS at
specific locations with inter-BS spacing $D=20$m. The BS height is $8$m. The
UE height is fixed at $1.5$m. Figure 1 shows this topology.

Figure 1: 3GPP InF topology. BS are represented with red circles.

In order to simulate various (virtual) objects in a factory that could
interfere with the wireless propagation, the 3GPP InF model introduces clutter
parameters $\left(r,h,d\right)$. These meta-parameters represent respectively
the clutter density, height, and size. In practice, they influence the NLoS
probability. In this paper, two different clutter configurations are
considered: $\left(r,h,d\right)=\left(40\%,2m,2m\right)$ and
$\left(r,h,d\right)=\left(60\%,6m,2m\right)$.

The radio parameters are set as follows: carrier frequency $f_{c}=3.5$ GHz,
bandwidth $W=100$ MHz. The BS and the UE antennas are omnidirectional with
unitary gains.

As an example, Figure 2 shows a LoS/NLoS realization both for the 40$\%$ and
60$\%$ cases. Figure 3 illustrates one realization of the PG from the
perspective of one BS.

(a) 40$\%$

(b) 60$\%$

Figure 2: A LoS/NLoS realization for the 40$\%$ and 60$\%$ clutter density
scenarios, respectively. Figure 3: PG map from the perspective of the red BS.

###  II-D Training and testing dataset generation

Two categories of datasets are generated from from our system level simulator
implementing the 3GPP InF-DH channel model and topology: PG datasets and CIR
datasets.

For the PG datasets, for each position $k$, the PG at each of the 18 BS,
$\mathbf{a}_{k}\in\mathbb{R}^{1\times 18}$, is computed and the horizontal
coordinate of the position $\mathbf{p}_{k}\in\mathbb{R}^{1\times 2}$ is
associated as the label.

The CIR datasets are generated in a similar manner, but where the data for
each position is now $\mathbf{b}_{k}\in\mathbb{C}^{256\times 18}$ instead of
$\mathbf{a}_{k}$, where 256 is the length of the CIR.

If a dataset with a reduced number of BS is required, we simply down-sample
these datasets and keep a reduced number of columns per sample, where a column
of a sample represent one BS.

Regarding the positions in the dataset, the scene is uniformly sampled. For
instance, to have a dataset of size 28 800, the inter-position spacing in both
axes is 0.5m.

Once trained, the neural network is tested on positions not used for the
training. In Sections III-A and III-C signals from randomly sampled positions
of the same factory are used: It means that the spatial consistency with the
data in the training dataset is respected. In Section III-D, where we study
the generalization, signals from another factory are used: The spatial
consistency with the training data is not respected.

###  II-E Neural network architectures

The PG and CIR datasets are evaluated on neural networks with different
architectures. For the PG datasets, a customized residual network (ResNet)
architecture is used, presented in Figure 4. Each fully connected layer is
composed of $120$ neurons. The neural network has 104.1k parameters. For the
CIR datasets, the ResNet18 architecture [3] (with untrained weights) is
considered. It has 11.1M parameters.

For the PG datasets, we choose a ResNet rather than a standard feed-forward
neural network. Indeed, empirical results show that they perform better with
the same number of parameters. For the CIR dataset, as the input has the
structure of an image, a convolutional neural network (CNN) is adapted. The
ResNet18 architecture, a CNN with a residual structure, offers good
positioning performance for a relatively low number of parameters in
comparison to other CNN such as ResNet50.

For both neural networks, the output is an estimated horizontal coordinate
vector $\hat{\mathbf{p}}_{k}$. The loss function for the training is the mean
squared error
$\mathcal{L}=\frac{1}{2}\left\lVert\hat{\mathbf{p}}_{k}-\mathbf{p}_{k}\right\rVert_{2}^{2}$.

##  III Simulation results

The main evaluation metric is the $90\%$ quantile of the cumulative
distributive function (CDF) of the horizontal positioning error
$Q\left(0.9\right)$, i.e., the value $Q\left(0.9\right)$ (in meters) such that
$90\%$ of the errors are under $Q\left(0.9\right)$.

###  III-A Type of radio signal

We first compare the positioning performance using the PG and the CIR as input
of the neural networks. We use the baseline InF channel with 18 BS. For both
radio signals, the neural networks are trained with a dataset of 28 800
positions uniformly placed in the scene.

The results are provided in Figure 5. There is no clear difference on the
positioning accuracy when the inference is based on the PG or CIR. The
observed differences may depend on more or less efficient hyper-parameter
optimization. Indeed, for some dataset, the hyper-parameter optimization
enabled to enhance the accuracy by 2m. Similarly, changing the density of
clutters does impact significantly the results.

Figure 4: ResNet architecture for the PG datasets. Figure 5: Training results
for the PG and CIR datasets. The dataset size is 28 800. The $Q(0.9)$ values
are: 2.4, 2.6, 2.6, and 3.0.

###  III-B Influence of the number of BS

We also investigate the positioning performance based on the PG and CIR with a
reduced number of BS. As the CIR is richer (256 values per position and BS)
than the PG (only 1 value per position and BS) we expect the former radio
signal to be more robust to a reduced number of BS.

The performance is provided on Figure 6. This is consistent with what is
expected. The positioning based on the PG requires at least 8 BS to get
reasonable performance while only 1 BS is required for the CIR. Increasing the
number of BS beyond these values only brings a marginal improvement.

Figure 6: Influence of the number of BS on the positioning performance.

###  III-C Influence of dataset size

Figure 7: Influence of training dataset size on UE positioning performance.

To study the influence of the dataset size on the UE positioning accuracy, we
generate training datasets of sizes going from 1700 to 80 000 for the PG and
1700 to 28 000 for the CIR, by changing the inter-position spacing. Results
are presented in Figure 7. As already observed with Figure 5, there is not
clear performance difference using the CIR or the PG with 18 BS. Then,
unsurprisingly, increasing the number of positions allows to obtain better UE
positioning performance. The $Q\left(0.9\right)$ value goes down from around
10m with a dataset of size 1700 to less than 1m with a dataset of size 80 000.
This latter result is consistent with the one reported in [6], where companies
report $Q(0.9)$ values slightly below 1m or slightly higher for CIR-based
positioning with a training dataset of size 80 000. Again, small differences
compared to [6] could be attributed to more or less efficient fine tuning of
the hyper parameters but do not impact the following main observation on the
dataset characteristics.

In the considered range, we have the following rule of thumb: The error is
divided by 2 each time the size of the training dataset is multiplied by 4.
This is not surprising as reducing the 2D inter-position spacing by a factor 2
induces multiplying the dataset size by a factor 4.

###  III-D Generalization

We analyse the generalization performance, i.e., how a network trained on a
specific factory (i.e., a channel realization) performs on another one. As
explained before, we consider two cases: without and with fine tuning.

Figure 8: Influence of the training dataset size on UE generalization
positioning performance.

The generalization performance without fine tuning and as a function of the
training dataset size is shown on Figure 8. In this experiment, the neural
networks are trained on a specific factory with a dataset of a given size and
then tested on another factory. Obviously, the CIR offers much better
performance compared to the PG: The $Q(0.9)$ value is divided by two when the
dataset is large enough. Moreover, we observe that the dataset size has no
significant influence on the PG generalization ability.

We now consider fine tuning for the PG. A first PG dataset with 80 000
positions is used to train the network. Then, a second PG generalization
dataset, representing PG from another factory, is generated. This dataset has
a limited number of positions, $1000$, chosen randomly in the scene. This
allows to mimic a random measurement process in a factory. The pre-trained
network is then trained on this light generalization dataset.

Results are provided in Figure 9. The fine tuning approach allows to obtain
better results than:

  * •

Using the neural network trained on the first dataset without fine tuning: The
$Q\left(0.9\right)$ value goes down from $19.1$m to $5.1$m. Note that the red
curve on the figure presents the same data as the one on Figure 8 for the PG
(60$\%$).

  * •

Training a neural network only on the second light dataset: The
$Q\left(0.9\right)$ value goes down from more than $10$m (see Figure 7) to
$5.1$m. Moreover, obtaining a $Q\left(0.9\right)=5.1$m with an untrained
network requires a dataset of size around 8000 (see Figure 8).

Figure 9: Transfer learning for the PG dataset in the $60\%$ clutter density
scenario. The $Q(0.9)$ values are 5.1 and 19.1.

The latter aspect highlights that there is a clear advantage in using a
network trained on another factory compared to an untrained network. This is
an instance of transfer learning which enables to save 7000 measurement data.

One should also note that with fine tuning on PG data, we obtain better
performance than the generalization performance of the CIR reported on Figure
8.

##  IV Conclusions

In this paper, we considered the deep learning approach for indoor positioning
in a NLoS environment. We first presented and discussed the 3GPP InF
statistical channel used to generate the datasets. We then reported simulation
results to assess the influence of some characteristics of the datasets on the
positioning performance. The five main takeaways are the following: 1-There is
no clear performance difference between the PG and CIR datasets when tested on
data from the same factory used to generate the training dataset, in the case
of 18 BS. 2-Unsurprisingly, the positioning accuracy obtained with the CIR is
significantly more robust to a reduced number of BS than the PG. 3-The
positioning error is approximately divided by two when the size of the
training dataset is increased by a factor 4. 4-Regarding the generalization
performance, meaning that the testing data is from a different factory than
the one used for the training, the CIR performs much better than the PG in the
case without fine tuning. 5-If fine tuning with a limited number of data from
the target factory is allowed, significant performance improvement (for the
PG) is observed. It means that transfer learning works with statistical
channels.

We emphasize that the light PG datasets offer competitive results compared to
the CIR datasets with a high enough number of BS, and also require lighter
neural network models (and therefore training time). This means that simpler
radio signal than the CIR, which is the main radio signal considered in the
3GPP study, could be used for the positioning task. If only a limited number
of BS is available, positioning based on the CIR is a good option.

## References

  * [1] M. Arnold, S. Dorner, S. Cammerer, and S. Ten Brink, “On Deep Learning-Based Massive MIMO Indoor User Localization,” 2018 IEEE 19th International Workshop on Signal Processing Advances in Wireless Communications (SPAWC), pp. 25-28, June 2018.
  * [2] S. Dwivedi et al., “Positioning in 5G networks,” IEEE Communications Magazine, vol 59, no. 11, pp. 38-44, Nov. 2021.
  * [3] K. He, X. Zhang, S. Ren, and J. Sun, “Deep Residual Learning for Image Recognition,” 2016 IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 770-778, 2016.
  * [4] A. Nessa, B. Adhikari, F. Hussain and X. N. Fernando, “A Survey of Machine Learning for Indoor Positioning,” IEEE Access, vol. 8, pp. 214945-214965, 2020.
  * [5] J. Nikonowicz et al., “Indoor Positioning Trends in 5G-Advanced: Challenges and Solution towards Centimeter-level Accuracy,” ArXiv:2209.01183, Sep. 2022.
  * [6] 3GPP R1-2210652, “Final Summary of Evaluation on AI/ML for positioning accuracy enhancement,” Meeting number 110bis-e, e-Meeting, Oct. 2022.
  * [7] 3GPP RP-213599, “New SI: Study on Artificial Intelligence (AI)/Machine Learning (ML) for NR Air Interface,” Meeting number 94e, e-Meeting, Dec. 2021.
  * [8] 3GPP TR 38.901, “Study on channel model for frequencies from 0.5 to 100 GHz,” V16.1.0, 2019.


# On the Within-Perfect Numbers

Chung-Hang Kwan<EMAIL_ADDRESS>Department of Mathematics, University
College London  and  Steven J. Miller<EMAIL_ADDRESS><EMAIL_ADDRESS>Department of Mathematics and Statistics,
Williams College, Williamstown, MA 01267

###### Abstract.

Motivated by the works of Erdös, Pomerance, Wolke and Harman on the sum-of-
divisor function $\sigma(n)$, we study the distribution of a special class of
natural numbers closely related to (multiply) perfect numbers which we term
‘$(\ell;k)$-within-perfect numbers’, where $\ell>1$ is a real number and
$k:[1,\infty)\rightarrow(0,\infty)$ is an increasing and unbounded function.

###### Key words and phrases:

Perfect numbers, Multiply perfect numbers, Within perfect numbers, Almost
perfect numbers, Pseudoperfect numbers, Diophantine equations, Diophantine
inequalities, Sum of divisors function, Arithmetic functions

###### 2010 Mathematics Subject Classification:

11A25 (primary), 11N25, 11B83 (secondary)

##  1\. Introduction

A natural number $n$ is said to be _perfect_ if $\sigma(n)=2n$, _$\ell$
-perfect_ if $\sigma(n)=\ell n$ (with $\ell>1$ being rational), and _multiply
perfect_ if $n\ |\ \sigma(n)$, where $\sigma(n)$ represents the sum of all
positive divisors of $n$. An outstanding conjecture, originating from the
ancient Greeks (300 BC), asserts that there are infinitely many even perfect
numbers but no odd perfect numbers (see Euclid [Eu, Book VII, IX], Dickson
[Di, Chapter I], Guy [Gu, Chapter B1]). This conjecture is well-supported by
probabilistic heuristics due to Pomerance [Pol, pp. 249, 258-259]. For
$\ell\in\\{2,3,\ldots,11\\}$, there are known examples of $\ell$-perfect
numbers (see [Gu, Chapter B1]); however, for other values of $\ell$, the
(non)existence of $\ell$-perfect numbers remains entirely open.

Starting in the mid-20th century, considerable interest emerged in
understanding the statistical distribution of perfect numbers. These numbers
are particularly rare, as demonstrated by the works of Erdös [Er56], Volkmann
[Vo56], Kanold [Ka54, Ka57], Hornfeck [Ho55] and Hornfeck-Wirsing [HW57],
culminating in the sharpest known upper bound for the number of perfect
numbers up to $x$ due to Wirsing [Wi59]. The bound obtained in [Wi59] is of
the order $\exp(O(\frac{\log x}{\log\log x})$ as $x\to\infty$, which possesses
the pleasant feature of _uniform_ applicability to $\ell$-perfect numbers for
any rational $\ell$. When restricting to the class of odd perfect numbers,
there is the celebrated Dickson’s finiteness theorem [Di13] which asserts the
following: given a natural number $k$, there are only finitely many odd
perfect numbers with exactly $k$ distinct prime divisors. This was later
refined by Pomerance [Pom77] and Heath-Brown [HB94].

Subsequently, it evolved into an active research area to investigate special
classes of natural numbers closely linked to perfect numbers, see [Gu, Chapter
B2-B3]. For instance, Sierpiński [Si65] introduced the notion of _‘pseudo-
perfect numbers.’_ In a companion article [CC+20], we studied a subclass of
these numbers known as _‘near-perfect numbers’_ , proposed by Pollack-Shevelev
[PS12]. In [CC+20], we strengthened the results and analysis of [PS12] by
employing recursive partitions and sieve-theoretic techniques.

In this article, we investigate another type of ‘approximate’ perfect numbers
of a somewhat different flavour which we term the $(\ell;k)$-_within-perfect_
numbers, where $\ell>1$ is a real number and $k=k(y)$ is a certain threshold
function. More precisely, a natural number $n$ is said to be
$(\ell;k)$-_within-perfect_ if the Diophantine inequality

$\displaystyle|\sigma(n)-\ell n|\ <\ k(n)$ (1.1)

holds. There are two distinct origins of these numbers. On one hand, Erdös
([Gu, pp. 46]) and Makowski [Ma79] were interested in the case when $\ell=2$
and $k$ is a constant. On the other hand, the inequality (1.1) arises
naturally in the field of Diophantine approximations for arithmetic functions.
Wolke [Wo77] studied (1.1) for any real $\ell>1$ and function $k(y)$ of the
form $y^{c}$. His result was improved by Harman [Ha10] and very recently by
Järviniemi [Ja22+]. In [Ja22+], it was shown that for any real $\ell>1$ and
any $c\in(0.45,1)$, there exist infinitely many $(\ell;y^{c})$-within-perfect
numbers. The range of $c$ can be extended to $(0.39,1)$ under the Riemann
Hypothesis as indicated in [Ha10]. The results of [Ha10, Ja22+] rely on deep
inputs from the distributions of primes in short intervals as well as that of
the differences of consecutive primes, see [BHP01, HB21, St22+, Ja22+].
Interested readers are also referred to Alkan-Ford-Zaharescu [AFZ09a, AFZ09b]
for settings more general than (1.1) and the related questions in Diophantine
approximations.

The main results of this article concern the class of threshold functions
$k=k(y)$ which are complementary to those considered in [Wo77, Ha10, Ja22+].
Moreover, we are also interested in estimating the size of the set

$\displaystyle W(\ell;k;x)\ :=\ \left\\{n\leq x:|\sigma(n)-\ell n|\ <\
k(n)\right\\}.$ (1.2)

Consequently, our work employs a different set of techniques compared to the
earlier mentioned works.

######  Theorem 1.1.

Let $c\in(0,1/3)$ be given. Suppose $k:[1,\infty)\rightarrow(0,\infty)$ is an
increasing and unbounded function satisfying $k(y)\leq y^{c}$ for $y\geq 1$.
Let $\Sigma$ be the set $\left\\{\sigma(m)/m:\,m\geq 1\right\\}$. Then

  1. (a)

If $\ell=a/b\in(\mathbb{Q}\cap(1,\infty))\setminus\Sigma$ with $(a,b)=1$, then

$\\#W(\ell;k;x)\ =\ O\left(ab^{3}x^{2/3+c+o(1)}\right)$ (1.3)

for $1<\ell\leq x^{c}$ and $x\geq 1$, where the implicit constants are
absolute.

  2. (b)

If $\ell=a/b\in\Sigma$ with $(a,b)=1$, and there exists $\delta>0$ such that
$k(y)\geq y^{\delta}$ for $y\geq 1$, then

$\lim_{x\to\infty}\,\frac{\\#W(\ell;k;x)}{x/\log x}\ \ =\ \
\sum_{\sigma(m)\,=\,\ell m}\frac{1}{m}.$ (1.4)

######  Remark 1.2.

We also have an analogous result for $c=0$ and its proof is actually simpler,
see Proposition 2.7 and Remark 3.1.

######  Remark 1.3.

Firstly, the infinite series of (1.4) converges by Wirsing’s Theorem ([Wi59]),
which will be applied in various ways throughout the course of proving Theorem
1.1.

Secondly, a key strength of our theorem is that all dependencies in (1.3) are
made entirely explicit. Our bound remains non-trivial even if the numerator or
denominator of $\ell$ grows with $x$ at a controlled rate, though this
necessitates appropriately shrinking the admissible range for $c$.

Thirdly, while it is possible that the dependence on $\ell$ (i.e., the factor
$ab^{3}$) in (1.3) can be improved, it does not appear that this dependence
can be removed. This is in constrast to Wirsing’s Theorem.

###  1.1. Notations

We use the following notations throughout this article:

  * •

$f(x)\asymp g(x)$ if there exist constants $c_{1},c_{2}>0$ such that
$c_{1}g(x)<f(x)<c_{2}g(x)$ for sufficiently large $x$,

  * •

$f(x)\sim g(x)$ if $\lim_{x\to\infty}f(x)/g(x)=1$,

  * •

$f(x)=O(g(x))$ or $f(x)\ll g(x)$ if there exists a constant $C>0$ such that
$f(x)<Cg(x)$ for sufficiently large $x$,

  * •

$f(x)=o(g(x))$ if $\lim_{x\to\infty}f(x)/g(x)=0$,

  * •

subscripts indicate dependence of implied constants on other parameters, and

  * •

$p$ always denotes a prime number.

###  1.2. Acknowledgments

This material is based upon work supported by the EPSRC grant: EP/W009838/1,
the Williams SMALL REU Program under the NSF grants DMS2341670, DMS1265673,
DMS1561945 and DMS1347804, as well as the Swedish Research Council under grant
no. 2021-06594 while the first author was in residence at Institut Mittag-
Leffler in Djursholm, Sweden during the year of 2024. Both of the authors
would like to express their gratitude to the participants of the SMALL REU
(2015-16) for their constant encouragement, and also for the generous
hospitality in Williamstown and Djursholm.

##  2\. Preliminary Discussions and Preparations

###  2.1. Distribution Function and Phase Transition

We begin by briefly explaining why the sublinear regime for $k=k(y)$ is of the
greatest interest in the study of within-perfectness. For this, we recall the
definition of a distribution function.

######  Definition 2.1.

Let $-\infty\leq a<b\leq\infty$.

  1. (1)

A function $F:(a,b)\rightarrow\mathbb{R}$ is a distribution function if $F$ is
increasing, right continuous, $F(a+)=0$, and $F(b-)=1$.

  2. (2)

An arithmetic function $f:\mathbb{N}\rightarrow\mathbb{R}$ has a distribution
function if there exists a distribution function $F$ such that

$\lim_{x\to\infty}\frac{1}{x}\,\\#\\{n\leq x:f(n)\leq u\\}\ =\ F(u)$

at all points of continuity of $F$.

A celebrated theorem of Davenport [Da33] asserts that $\sigma(n)/n$ possesses
a continuous and strictly increasing distribution function on $[1,\infty)$.
Denote by $D(\,\cdot\,)$ the distribution function of $\sigma(n)/n$ and extend
its definition to $\mathbb{R}$ by setting $D(u)=0$ for $u<1$. More generally,
a necessary and sufficient criterion for the existence of distribution
functions for additive functions was established by Erdős-Wintner [EW39], see
[Te, Chapter I.5, III.4] for further details.

The following result describes the phase transition for the asymptotic density
for the set of all $(\ell;k)$-within-perfect numbers which we denote by
$W(\ell;k)$.

######  Proposition 2.2.

Let $D(\cdot)$ be the distribution function of $\sigma(n)/n$. Then

  1. (a)

If $k(n)=o(n)$, then $W(\ell;k)$ has asymptotic density 0.

  2. (b)

If $k(n)\sim cn$ for some $c>0$, then $W(\ell;k)$ has asymptotic density equal
to $D(\ell+c)-D(\ell-c)$.

  3. (c)

If $k(n)\asymp n$, then $W(\ell;k)$ has positive lower density and upper
density strictly less than $1$.

  4. (d)

If $n=o(k(n))$, then $W(\ell;k)$ has asymptotic density 1.

###### Sketch.

The proof is elementary and we will only indicate certain details for part
(d). Let’s label the elements of $W(\ell;k)$ by $n_{j}$ in increasing order.
For any $j\in\mathbb{N}$, there exists $n_{j}\in\mathbb{N}$ such that
$n/k(n)<1/j$ for any $n\geq n_{j}$. Whenever $x\geq n_{j}$, we have

$\displaystyle\frac{1}{x}\,\\#\\{n\leq x:\lvert\sigma(n)-\ell n\rvert<jn\\}\
\leq\ \frac{n_{j}}{x}\ +\ \frac{1}{x}\,\\#\\{n\leq x:\lvert\sigma(n)-\ell
n\rvert<k(n)\\}.$

Upon taking liminf to both sides, it follows that $D(\ell+j)\ \leq\ 1$. By
Davenport’s theorem, $D(\,\cdot\,)$ is continuous and $D(\infty)=1$. Letting
$j\to\infty$ yields

$\liminf_{x\to\infty}\,\frac{\\#W(\ell;k;x)}{x}\ =\ 1.$

∎

###  2.2. On Congruences involving $\sigma(n)$

Henceforth, our focus shifts to the sublinear thresholds, where we crucially
make use of the techniques developed by Pomerance and his co-authors over the
years. In 1975, Pomerance [Pom75] initiated the study of the equation

$\displaystyle\sigma(n)\ =\ \ell n\ +\ k$ (2.1)

with $\ell$, $k$ being integers and $\ell>1$. Central to [Pom75] is the
following important concept, which proves very useful in many Erdös-style
problems (see [PP16]):

######  Definition 2.3 (Regular/ Sporadic).

The solutions to the congruence $\sigma(n)\equiv k\ (\bmod\,n)$ of the form

$n=pm,\hskip 10.0pt\text{ where }\hskip 10.0pt\ p\mathchar 13613\relax
m,\hskip 5.0ptm\mid\sigma(m),\hskip 5.0pt\sigma(m)\ =\ k,$ (2.2)

are called _regular_. All other solutions are called _sporadic_.

The main observation is that sporadic solutions occur much less frequently
than regular solutions. In a series of works [Pom75, Pom76a, Pom76b, PS12,
APP12, PP13], this was quantified with various degrees of precision and
uniformity. We summarize the progress made in this direction.

Let $\operatorname{Spor}_{k}(x)$ be the set of sporadic solutions of
$\sigma(n)\equiv k\ (\bmod\ n)$ up to $x$. In [Pom75], [PS12], [APP12] and
[PP13], it was shown, respectively, that the following bounds hold as
$x\to\infty$:

  * •

$\\#\operatorname{Spor}_{k}(x)=O_{\beta,k}(x\exp(-\beta\sqrt{\log x\log\log
x}))$ for _fixed_ $k$ and _fixed_ $\beta<1/\sqrt{2}$,

  * •

$\\#\operatorname{Spor}_{k}(x)=O(x^{2/3+o(1)})$ _uniformly_ in $\lvert
k|<x^{2/3}$,

  * •

$\\#\operatorname{Spor}_{k}(x)=O(x^{1/2+o(1)})$ _uniformly_ in $\lvert
k|<x^{1/4}$, and

  * •

$\\#\operatorname{Spor}_{k}(x)\cap\\{\sigma(n)\ \text{is
odd}\\}=O(|k|x^{1/4+o(1)})$ uniformly in $0<\lvert k|\leq x^{1/4}$.

When $k=0$, we have a much stronger bound for (2.1) due to Wirsing ([Wi59]).

Unfortunately, the aforementioned results are not sufficient for our study of
within-perfect numbers. We must consider a more general congruence

$b\sigma(n)\ \equiv\ k\ (\bmod\,n)$ (2.3)

where $b$ and $k$ are integers with $b\geq 1$. Accordingly, the definitions of
regular and sporadic solutions should be extended as follows:

######  Definition 2.4.

Suppose $b\mid k$. Then $n$ is said to be a _regular solution_ to (2.3) if

$n\ =\ pm,\hskip 10.0pt\text{ where }\hskip 5.0ptp\mathchar 13613\relax
m,\hskip 5.0ptm\mid b\sigma(m),\hskip 5.0pt\sigma(m)\ =\ \frac{k}{b}.$ (2.4)

All other solutions are called _sporadic_. In the case when $b\mathchar
13613\relax k$, all solutions to (2.3) are considered _sporadic_.

We record the following generalization of [PS12, Lemma 8], which will be used
in the proof of Theorem 1.1 and may also be of independent interest. For the
convenience of the readers, we include a sketch of proof of this proposition
here.

######  Proposition 2.5.

The number of sporadic solutions $n\leq x$ to the congruence $b\sigma(n)\equiv
k\,(\bmod\,n)$ is $O(b^{2}x^{2/3+o(1)})$ for any $x\geq 1$ and integer $k$
satisfying $|k|<bx^{2/3}$. The implicit constants are absolute.

Our intended applications take into account of the uniformity of the range and
the strength of the upper bound in counting sporadic solutions. In light of
Wirsing’s Theorem ([Wi59]) and Remark 1.3, it is also desriable to maintain
all implicit constants absolute but this can be somewhat subtle, see [APP12,
Remark 1] and [PP13]. After a careful examination of existing strategies, the
authors believe that the approach of [PS12] is the most suitable for attaining
our desired generalization (e.g., $\ell$ can be rational), incorporating all
the favourable features mentioned above. Their method softly utilizes the
unique factorization of a natural number into its square-free and square-full
parts, the anatomy of unitary divisors 111Note: $m$ is a unitary divisor of
$n$ if $n$ has a decomposition of the form $n=mm^{\prime}$, where
$(m,m^{\prime})=1$., and the following result from [Pol11, Theorem 1.3]:

$\sum_{x^{1/3}<m\leq x^{2/3}}\ \frac{(m,\sigma(m))}{m^{2}}\ \leq\
3x^{-1/3+o(1)},$ (2.5)

which turns out to be a nice application of Wirsing’s Theorem!

###### Proof of Proposition 2.5.

We can certainly assume that $x\geq b$, otherwise the count is trivially
bounded by $b$, which is acceptable in view of Theorem 1.1. Let
$|k|<bx^{2/3}$. Suppose $n\leq x$ is a sporadic solution to the congruence
$b\sigma(n)\equiv k\,(\bmod\,n)$. One can simultaneously assume that
$n>x^{2/3}$ and the square-full part of $n$ is bounded by $x^{2/3}$. Indeed,
the contribution from the complement can easily seen to be $O(x^{2/3})$. We
then consider the following two cases.

  1. (1)

Suppose $p:=P^{+}(n)>x^{1/3}$. By the assumption made, we have $n=pm$ with $p\
\mathchar 13613\relax\ m$ and $m<x^{2/3}$. The congruence can be written as
$b\sigma(n)\ =\ qn+k$ for some integer $q\geq 0$. It follows that

$\displaystyle b(p+1)\sigma(m)\ =\ b\sigma(n)\ =\ qpm+k,$

and

$p(b\sigma(m)-qm)\ =\ k-b\sigma(m).$

If $k-b\sigma(m)=0$, then $n$ is a regular solution, which is a contradiction!
So, $k-b\sigma(m)\neq 0$. For each $m$, the number of such $p$ is
$O(\log|k-b\sigma(m)|)\,=\,O(\log(bx^{2/3}\log\log x))\,=\,O(\log bx)$ because
of $p\mid(k-b\sigma(m))$. Therefore, the number of such $n$ is $O(x^{2/3}\log
bx)=O(x^{2/3}\log x)$, which is acceptable.

  2. (2)

Suppose $p:=P^{+}(n)\leq x^{1/3}$. Such $n$ must have a _unitary divisor_ $m$
in the interval $(x^{1/3},x^{2/3}]$, see [PS12]. We have
$\sigma(n)\,\equiv\,0\ (\bmod\,\sigma(m))$ and $b\sigma(n)\,\equiv\,k\
(\bmod\,m)$. By the Chinese Remainder Theorem, we have $b\sigma(n)\equiv
a_{n}\ (\bmod\ [m,\sigma(m)])$ for some unique $0\leq a_{n}<[m,\sigma(m)]$.
Given $m\in(x^{1/3},x^{2/3}]$, the number of possible values for $b\sigma(n)$
is $\leq 1+(2bx\log x)/[m,\sigma(m)]$. Summing over $m\in(x^{1/3},x^{2/3}]$,
the total number of possible values of $b\sigma(n)$ is

$\displaystyle\leq\ \sum_{x^{1/3}<m\leq x^{2/3}}\ \left(\frac{2bx\log
x}{[m,\sigma(m)]}\ +\ 1\right)$ $\displaystyle\leq\ x^{2/3}\ +\ (2bx\log
x)(3x^{-1/3+o(1)})\ \leq\ 7bx^{2/3+o(1)}$

from Lemma 2.5. Moreover, the size of $q=(b\sigma(n)-k)/n$ is clearly

$\displaystyle\hskip 25.0pt\ \ll\ b\log\log x\ +\ \frac{|k|}{n}\ <\ b\log\log
x+b\ \ll\ b\log\log x$

by the assumptions $n>x^{2/3}$ and $|k|<bx^{2/3}$. Since $b\sigma(n)=qn+k$,
the number of possible values of $n$ is at most

$(7bx^{2/3+o(1)})(b\log\log x)\ \leq\ 7b^{2}x^{2/3+o(1)}.$

The desired result follows by putting the conclusions of the two cases
together. ∎

###  2.3. A simple application

Let $k,a,b$ be integers such that $k\neq 0$, $a>b\geq 1$, and $(a,b)=1$.
Denote by $S(a,b;k)$ the set of all solutions to the Diophantine equation
$b\sigma(n)=an+k$ that generalizes (2.1). Let
$S(a,b;k;x):=S(a,b;k)\,\cap\,[1,x]$. The main result of [Pom75] is stated as
follows.

######  Theorem 2.6.

As $x\to\infty$, we have

$\\#S(a,1;k;x)\ \ll_{k,a}\ \frac{x}{\log x}.$ (2.6)

Motivated by Pomerance’s theorem, Davis-Klyve-Kraght [DKK13] recently
performed an extensive numerical investigation on the true size of
$S(a,1;k;x)$. As a first application of Proposition 2.5, we sharpen
Pomerance’s theorem and confirm some of the observations and speculations made
in [DKK13]. This will also serve as the base case for Theorem 1.1, see Section
3.2.

######  Proposition 2.7.

  1. (a)

If $k\geq 1$, $ab\mid k$, and $\sigma(k/a)=k/b$, then

$\\#S(a,b;k;x)\ \sim\ \frac{a}{k}\,\frac{x}{\log(ax/k)}$ (2.7)

as $x\to\infty$.

  2. (b)

Otherwise, we have

$\\#S(a,b;k;x)\ =\ O(b^{2}x^{2/3+o(1)})$ (2.8)

for any $x\geq 1$, where the implicit constants are absolute. In particular,
the bound (2.8) is uniform in $a$.

###### Proof.

Suppose $n\in S(a,b;k)$. Then $b\sigma(n)\equiv k\,(\bmod\,n)$. If $b\mathchar
13613\relax k$, then all solutions are sporadic by Definition 2.4 and (2.8)
follows at once from Proposition 2.5.

Suppose $b\mid k$ and $n$ is a regular solution. Then
$k(1+p)=b(1+p)\sigma(m)=apm+k$. Hence, $b\sigma(m)=k=am$ and in particular, we
have

$\displaystyle a\mid k\hskip 10.0pt\text{ and }\hskip 10.0pt\sigma(k/a)\ =\
k/b\hskip 5.0pt(=\ \sigma(m)).$ (2.9)

In other words, if (2.9) is violated, then all solutions are sporadic and once
again (2.8) holds. This proves part (b) of Proposition 2.7.

Suppose $ab\mid k$ and $\sigma(k/a)\ =\ k/b$. Then the set
$\\{n\in\mathbb{N}:n=p(k/a),\,p\mathchar 13613\relax(k/a)\\}$ consists of all
regular solutions and is contained in $S(a,b;k)$. Using Proposition 2.5, the
Prime Number Theorem, and the bound $\omega(n)=O(\log n)$ 222 Denote by
$\omega(n)$ the number of distinct prime factors of $n$. , it follows that

$\displaystyle\\#S(a,b;k;x)\ $ $\displaystyle=\ \pi(ax/k)\ +\ O(\log|k|)\ +\
O(b^{2}x^{2/3+o(1)})$ $\displaystyle\sim\ \frac{a}{k}\frac{x}{\log(ax/k)}$

as $x\to\infty$. Hence, part (a) follows and this completes the proof of
Proposition 2.7. ∎

##  3\. Proof of Theorem 1.1

###  3.1. Upper Bound

We begin by proving the harder part of Theorem 1.1, i.e., the upper bounds for
$W(\ell;k;x)$. Fix $c\in(0,1/3)$. Let $k_{c}(y):=y^{c}$ and $k(y)\leq
k_{c}(y)$ for $y\geq 1$. Given a function $f$, we write $\mathaccent
869{W}(\ell;f;x):=\\{n\leq x:|\sigma(n)-\ell n|<f(x)\\}$. The following
inequality is apparent:

$\\#W(\ell;k;x)\ \leq\ \\#\mathaccent 869{W}(\ell;k;x)\ \leq\ \\#\mathaccent
869{W}(\ell;k_{c};x).$ (3.1)

Let $\ell=a/b>1$ be in the lowest term. For $n\in\mathaccent
869{W}(\ell;k_{c};x)$, we have $b\sigma(n)-an=k$ for some integer $k$ such
that $|k|<bx^{c}$. In particular, we have

$b\sigma(n)\,\equiv\,k\ (\bmod\,n)\hskip 10.0pt\text{ for }\hskip
10.0pt|k|<bx^{c}.$ (3.2)

By Proposition 2.5, the number of $n\in\mathaccent 869{W}(\ell;k_{c};x)$ which
is a sporadic solution (see Definition 2.4) is
$O(bx^{c})\,\cdot\,O(b^{2}x^{2/3+o(1)})=O(b^{3}x^{2/3+c+o(1)})$, which is
acceptable in view of Theorem 1.1. On the other hand, the number of regular
solutions $n=pm\in\mathaccent 869{W}(\ell;k_{c};x)$ with $p\leq bx^{c}$ is
$O(bx^{c+o(1)})$ by Wirsing’s Theorem ([Wi59] or see Section 1). The
contribution is clearly negligibly small.

Suppose $p>bx^{c}$ and $b\sigma(m)=rm$ for some integer $r\geq a+1$. Then

$\displaystyle\hskip 10.0pt|b\sigma(n)-an|$
$\displaystyle=|b(1+p)\sigma(m)-apm|=|(1+p)rm-apm|=m|r+p(r-a)|$
$\displaystyle\geq m(r+p)>bx^{c}.$

This contradicts with (3.2)!

Suppose $p>bx^{c}$ and $b\sigma(m)=rm$ for some integer $r\leq a-1$. Then

  * •

If $r+p(r-a)\geq 0$ (which implies $p<a$), then a contradiction with
$p>bx^{c}$ arises whenever $x^{c}>\ell$.

  * •

If $r+p(r-a)<0$, then $|b\sigma(n)-an|<bx^{c}\iff m[(a-r)p-r]<bx^{c}$. By
Merten’s Theorem, the number of such $n$ is at most

$\displaystyle\sum_{2\leq r\leq a-1}\sum_{bx^{c}<p\leq
x}\frac{bx^{c}}{(a-r)p-r}\ $ $\displaystyle\ \leq abx^{c}\sum_{bx^{c}<p\leq
x}\frac{1}{p-(a-1)}$ $\displaystyle\leq 2abx^{c}\,\sum_{p\leq x}\frac{1}{p}\
\ll\ abx^{c}\log\log x$

whenever $x^{c}\geq 2\ell$. The contribution is once again negligible.

Hence, we are left to consider the case when $r=a$, i.e.,

$\displaystyle n\ =\ pm\ \in\ \mathaccent 869{W}(\ell;k_{c};x)\hskip
10.0pt\text{ such that}\hskip 10.0ptp\ >\ bx^{c}\hskip 5.0pt\text{ and }\hskip
5.0pt\sigma(m)\ =\ \ell m.$ (3.3)

If $\ell\not\in\Sigma$, there is clearly no such $n$ and thus
$\\#W(\ell;k;x)=O(ab^{3}x^{2/3+c+o(1)})$ by taking into account the paragraphs
right above. This proves part (a) of Theorem 1.1.

Suppose $\ell\in\Sigma$. Firstly, observe from partial summation and Wirsing’s
Theorem that

$\displaystyle\sum_{\begin{subarray}{c}\sigma(m)\,=\,\ell
m\end{subarray}}\,\frac{\log m}{m}\ =\ \int_{1}^{\infty}\frac{\log
t}{t}\,dP_{\ell}(t)\ =\ \lim_{t\to\infty}\,\frac{\log
t}{t^{1-o(1)}}\,+\,\int_{1}^{\infty}\,\frac{\log t}{t^{2-o(1)}}\ dt\ \ll\ 1,$
(3.4)

where $P_{\ell}(t):=\\#\\{m\leq t:\sigma(m)\,=\,\ell m\\}$. As a result, both
of the series

$\sum_{\sigma(m)\,=\,\ell m}\,\frac{\log m}{m}\hskip 10.0pt\text{ and }\hskip
10.0pt\sum_{\sigma(m)\,=\,\ell m}\,\frac{1}{m}$ (3.5)

can readily seen to be convergent. Notice that the bound (3.4) is uniform in
$\ell$.

Secondly, we have $m<x^{1-c}$ since $x\geq n=pm>x^{c}m$. 333 Actually, $m\leq
x^{\min\\{c,1-c\\}}$.  It follows that

$0\ <\ \frac{\log m}{\log x}\ \leq\ 1-c\ <\ 1,$

and

$\bigg{(}1-\frac{\log m}{\log x}\bigg{)}^{-1}\ =\ 1+O_{c}\bigg{(}\frac{\log
m}{\log x}\bigg{)}.$ (3.6)

Let $\beta>1$ be given. The Prime Number Theorem asserts the existence of a
constant $X_{0}=X_{0}(\beta)>0$ such that $\pi(x)<\beta x/\log x$ whenever
$x\geq X_{0}$. For $x\geq X_{0}^{1/c}$, the number of $n$ satisfying (3.3) is
at most

$\displaystyle\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{1-c}\end{subarray}}\pi(x/m)\ $ $\displaystyle<\ \beta\
\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{1-c}\end{subarray}}\frac{x/m}{\log(x/m)}$ $\displaystyle<\ \frac{\beta
x}{\log x}\sum_{\sigma(m)=\ell m}\frac{1}{m}\,+\,O_{c}\bigg{(}\frac{\beta
x}{(\log x)^{2}}\sum_{\begin{subarray}{c}\sigma(m)=\ell
m\end{subarray}}\frac{\log m}{m}\bigg{)}$ $\displaystyle<\ \frac{\beta x}{\log
x}\sum_{\sigma(m)=\ell m}\frac{1}{m}\,+\,O_{c}\bigg{(}\frac{\beta x}{(\log
x)^{2}}\bigg{)}$

with the help of (3.6) and the convergence of the series in (3.5). Therefore,
we have

$\limsup_{x\to\infty}\,\frac{\\#W(\ell;k;x)}{x/\log x}\ \leq\
\beta\sum_{\sigma(m)=\ell m}\frac{1}{m}$ (3.7)

for any $\beta>1$. Let $\beta\to 1+$ in (3.7), it follows that

$\limsup_{x\to\infty}\frac{\\#W(\ell;k;x)}{x/\log x}\ \leq\
\sum_{\sigma(m)=\ell m}\frac{1}{m}.$

This proves the upper bound of Theorem 1.1.(b).

###  3.2. Lower Bound

The proof of the lower bound for Theorem 1.1.(b) is relatively straight-
forward. Suppose $\ell\in\Sigma$. Based on the experience of Pomerance et. al.
(see Section 2.2), a lower bound for $\\#W(\ell;k;x)$ can be obtained by
estimating the size of the set

$\displaystyle\mathcal{L}_{\ell}(\delta)\ :=\ \left\\{n\leq x:\,n\,=\,pm,\
p\mathchar 13613\relax m,\ \sigma(m)=\ell m,\ \ell
m\,<\,(pm)^{\delta}\right\\}$ (3.8)

provided that $k(y)\geq y^{\delta}$ for any $y\geq 1$, where $\delta\in(0,1)$.
We have

$\displaystyle\\#\mathcal{L}_{\ell}(\delta)\ =\
\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{\delta}/\ell\end{subarray}}\ \sum_{\begin{subarray}{c}(\ell
m)^{1/\delta}/m<p\leq x/m\\\ p\,\mathchar 13613\relax\,m\end{subarray}}\,1.$

Using the bound $\omega(m)=O(\log m)$, Wirsing’s theorem and partial
summation, it follows that

$\displaystyle\\#\mathcal{L}_{\ell}(\delta)\ =\
\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{\delta}/\ell\end{subarray}}\ \sum_{\begin{subarray}{c}(\ell
m)^{1/\delta}/m<p\leq x/m\end{subarray}}\,1\ \ +\ \ O_{\delta}(x^{o(1)}),$

and

$\displaystyle\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{\delta}/\ell\end{subarray}}\ \sum_{\begin{subarray}{c}p\leq(\ell
m)^{1/\delta}/m\end{subarray}}\,1\ \ll\
\ell^{1/\delta}\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{\delta}\end{subarray}}\ m^{1/\delta-1}\ \ll\
\ell^{1/\delta}x^{1-\delta+o(1)}.$

Hence,

$\displaystyle\\#\mathcal{L}_{\ell}(\delta)\ =\
\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{\delta}/\ell\end{subarray}}\ \pi(x/m)\ \ +\ \
O_{\delta}\left(\ell^{1/\delta}x^{1-\delta+o(1)}\right).$ (3.9)

Let $\alpha<1$. By the Prime Number Theorem, there exists
$x_{0}=x_{0}(\alpha)>0$ such that $\pi(x)>\alpha x/\log x$ whenever $x\geq
x_{0}$. Thus, if $x>(x_{0})^{1/(1-\delta)}$, then

$\displaystyle\\#\mathcal{L}_{\ell}(\delta)\ $ $\displaystyle>\ \frac{\alpha
x}{\log x}\sum_{\begin{subarray}{c}\sigma(m)=\ell m\\\ m\leq
x^{\delta}/\ell\end{subarray}}\ \frac{1}{m}\ \ +\ \
O_{\delta}\left(\ell^{1/\delta}x^{1-\delta+o(1)}\right)$ $\displaystyle=\
\frac{\alpha x}{\log x}\left(\sum_{\begin{subarray}{c}\sigma(m)=\ell
m\end{subarray}}\
\frac{1}{m}\,+\,O\left((\ell/x^{\delta})^{1+o(1)}\right)\right)\ +\
O_{\delta}\left(\ell^{1/\delta}x^{1-\delta+o(1)}\right).$

From this, we may deduce that

$\displaystyle\liminf_{x\to\infty}\ \frac{\\#W(\ell;k;x)}{x/\log x}\ >\
\alpha\sum_{\begin{subarray}{c}\sigma(m)=\ell m\end{subarray}}\ \frac{1}{m}.$
(3.10)

Since this holds for any $\alpha<1$, the lower bound for Theorem 1.1.(b)
follows.

######  Remark 3.1.

Suppose $\ell\in\Sigma$. Proposition 2.7 implies that when $k\equiv k_{0}\geq
1$ is a _constant_ function, we have

$\displaystyle\frac{\\#W(\ell;k_{0};x)}{x/\log x}\ $ $\displaystyle=\
\sum_{|k|<bk_{0}}\,\frac{\\#S(a,b;k;x)}{x/\log x}\ \sim\ \
\sum_{\begin{subarray}{c}0<m<k_{0}/\ell\\\ b\mid m\\\ \sigma(m)=\ell
m\end{subarray}}\ \frac{1}{m}$ (3.11)

as $x\to\infty$. The rightmost quantity of (3.11) converges to
$\sum\limits_{\begin{subarray}{c}\sigma(m)=\ell m\\\ b\mid
m\end{subarray}}\,1/m$ as $k_{0}\to\infty$. In particular, when
$\ell\in\mathbb{Z}$ and $k$ is an increasing unbounded function, one reaily
observes that

$\displaystyle\frac{\\#W(\ell;k;x)}{x/\log x}\ \sim\ \lim_{k_{0}\to\infty}\
\frac{\\#W(\ell;k_{0};x)}{x/\log x}$ (3.12)

as $x\to\infty$. However, the asymptotic (3.12) is not necessarily true when
$\ell\not\in\mathbb{Z}$ because of the restriction $b\mid m$ present in
(3.11)!

##  4\. Concluding Discussions, Numerics, & Further Directions

Building upon the method of [APP12], Pollack-Pomerance-Thompson [PPT18]
recently proved a variant of the main result of [APP12], albeit with a weaker
error term and uniformity. Specifically, they proved that if
$\ell\in\mathbb{Z}$ is _kept fixed_ , the number of sporadic solutions to the
_equation_ $\sigma(n)=\ell n+k$ up to $x$ is $O(x^{3/5+o_{\ell}(1)})$ as
$x\to\infty$ and for any integer $k$. To the best of the authors’ knowledge,
there seems to be a number of subtlties in generalizaing the method of [PPT18]
to the equation $b\sigma(n)=an+k$. Additionally, as noted in [APP12], it
appears that obtaining an estimate that is fully uniform in all of $a,b,k$
would require considerable effort.

If $\ell$ is restricted to be an _integer_ and is kept _fixed_ , the same
argument from Theorem 1.1 along with the main theorem of [PPT18], should yield
the slightly improved admissible range $c\in(0,2/5)$. However, the barrier of
our method seems to be $c\in(0,1/2)$, see [PPT18, Conjecture 4.3]. When $\ell$
is _not_ an integer, it is unclear what the barrier should be and likley
somewhat smaller than $(0,1/2)$.

Theorem 1.1 leads to several interesting consequences which are stated as
follows. As usual, $k:[1,\infty)\rightarrow(0,\infty)$ is an increasing
function such that

$\displaystyle\hskip 20.0pty^{\delta}\ \leq\ k(y)\ \leq\ y^{c}\hskip
20.0pt\text{ for }\hskip 20.0pty\ \geq\ 1.$ (4.1)

Firstly, it is natural to consider the following quantity

$\mathcal{D}_{c}(\ell)\ :=\ \lim_{x\to\infty}\
\frac{\\#W(\ell;y^{c};x)}{x/\log x}\ =:\ \lim_{x\to\infty}\
\mathcal{D}_{c}(\ell;x)$ (4.2)

for $\ell\in[1,\infty)$ and $c\in(0,1)$. In view of Proposition 2.2, this new
‘distribution function’ is arguably well-suited to study the within-perfect
numbers with respect to sublinear threshold. However, this distribution
function behaves quite differently from the ones described in Definition 2.1.

######  Proposition 4.1.

The function $\ell\mapsto\mathcal{D}_{c}(\ell)$ is discontinuous on a dense
subset of $[1,\infty)$, for any $c\in(0,1/3)$.

###### Proof.

It follows from a theorem of Anderson (see [Pol, pp. 270]) that
$(\mathbb{Q}\cap[1,\infty))\setminus\Sigma$ is dense in $[1,\infty)$. Observe
that $\mathcal{D}_{c}$ takes the value $0$ on
$(\mathbb{Q}\cap[1,\infty))\setminus\Sigma$ but it takes positive values on
$\Sigma$ by Theorem 1.1. So, $\mathcal{D}_{c}$ is discontinuous on $\Sigma$.
It is a well-known theorem that $\Sigma$ is again dense in $[1,\infty)$ (see
[Pol, pp. 275]). This completes the proof. ∎

Secondly, a real number $\ell>1$ is said to be _$\Sigma$ -approximable_ if
there exists a function $f(x)\to\infty$ and a sequence of positive integers
$(m_{i})_{i\geq 1}$ such that $|\ell-\sigma(m_{i})/m_{i}|<1/f(m_{i})$ for any
$i\geq 1$. It is clear that

######  Proposition 4.2.

If $\ell>1$ is $\Sigma$-approximable, then $\\#W(\ell;k;x)\gg x/\log x$ on an
unbounded set of $x$.

In fact, for any function $f(x)\to\infty$, there are _irrational_ numbers
$\ell>1$ that are $\Sigma$-approximable by $f$. This follows from the standard
nested interval argument and the theorems of Anderson used in the proof of
Proposition 4.1.

We conclude this article with some numerics and open problems for further
investigation.

We calculate the quotient of $D_{c}(2;x)$ for various values of $c\in(0,1)$
and at $x=1,000,000$, $x=10,000,000$, and $x=20,000,000$. Note:
$\sum\limits_{\sigma(m)=2m}\frac{1}{m}\approx 0.2045$.

$k(y)$ | $x=1,000,000$ | $x=10,000,000$ | $x=20,000,000$
---|---|---|---
$y^{0.9}$ | 3.661860 | 3.305180 | 3.196040
$y^{0.8}$ | 1.141480 | 0.945623 | 0.908751
$y^{0.7}$ | 0.494278 | 0.435395 | 0.426470
$y^{0.6}$ | 0.311567 | 0.274586 | 0.267904
$y^{0.5}$ | 0.276559 | 0.259482 | 0.255962
$y^{0.4}$ | 0.264968 | 0.252956 | 0.250063
$y^{0.3}$ | 0.225980 | 0.247837 | 0.247299
$y^{0.2}$ | 0.151238 | 0.195911 | 0.197430
Table 1. $\mathcal{D}_{c}(2;x)$ for various values of $x$ and $c$.

It is natural to ask the following.

######  Problem 4.3.

When $c\in(1/2,1)$, does the correct order of magnitude for $\\#W(\ell;k;x)$,
with $\ell\in\Sigma$ and $k$ satisfying (4.1), continue to be $x/\log x$ as
$x\to\infty$?

In between the sublinear and linear regime, e.g., $k(y)=y/\log y$, Proposition
2.2 gives no conclusion. Consider the plot of $x\mapsto\\#W(2;k;x)/(x/\log x)$
for such $k$ from $x=2$ to $x=10,000$:

Figure 1. This plot shows the quantity $\\#W(2;k;x)/(x/\log x)$ with
$k(y)=y/\log y$ for $x=2$ to $10,000$.

######  Problem 4.4.

What is the order of magnitude of $\\#W(\ell;k;x)$ if the function $k$
satisfies $y^{c}=o(k(y))$ _for any_ $c\in(0,1)$?

######  Problem 4.5.

What is the order of magnitude for $\\#W(\ell;k;x)$ for _irrational_ $\ell$?

######  Problem 4.6.

Determine set of points of continuity for the distribution function
$\ell\mapsto\mathcal{D}_{c}(\ell)$.

## References

  * [AFZ09a] Alkan, Emre; Ford, Kevin; Zaharescu, Alexandru. _Diophantine approximation with arithmetic functions. I._ Trans. Amer. Math. Soc. 361 (2009), no. 5, 2263-2275.
  * [AFZ09b] Alkan, Emre; Ford, Kevin; Zaharescu, Alexandru. _Diophantine approximation with arithmetic functions. II._ Bull. Lond. Math. Soc. 41 (2009), no. 4, 676-682.
  * [APP12] Anavi, Aria; Pollack, Paul; Pomerance, Carl. _On congruences of the form $\sigma(n)\equiv a\,(\bmod\,n)$_. Int. J. Number Theory 9 (2013), no. 1, 115-124.
  * [BHP01] Baker, R. C.; Harman, G.; Pintz, J. _The difference between consecutive primes. II._ Proc. London Math. Soc. (3) 83 (2001), no. 3, 532-562.
  * [CC+20] Cohen, Peter; Cordwell, Katherine; Epstein, Alyssa; Kwan, Chung-Hang; Lott, Adam; Miller, Steven J. _On near-perfect numbers_. Acta Arith. 194 (2020), no. 4, 341-366.
  * [Da33] Davenport, H. _Über numeri abundantes_ , S.-Ber. Preuß. Akad. Wiss., math.-nat. Kl. (1933), 830-837.
  * [Di] Dickson, Leonard Eugene. History of the theory of numbers. Vol. I: Divisibility and primality. Chelsea Publishing Co., New York, 1966. xii+486 pp.
  * [Di13] Dickson, Leonard Eugene. _Finiteness of the Odd Perfect and Primitive Abundant Numbers with $n$ Distinct Prime Factors._ Amer. J. Math. 35 (1913), no. 4, 413-422.
  * [DKK13] Davis, Nichole; Klyve, Dominic; Kraght, Nicole. _On the difference between an integer and the sum of its proper divisors._ Involve 6 (2013), no. 4, 493-504.
  * [Er56] Erdös, P. _On perfect and multiply perfect numbers_ , Annali di Matematica Pura ed Applicata 42 (1956), no. 1, 253-258.
  * [EW39] Erdös, Paul; Wintner, Aurel. _Additive arithmetical functions and statistical independence._ Amer. J. Math. 61 (1939), 713-721.
  * [Eu] Euclid of Alexandria. _The Elements._ Book VII & IX.
  * [Gu] Guy, Richard K. Unsolved problems in number theory. Second edition. Problem Books in Mathematics. Unsolved Problems in Intuitive Mathematics, I. Springer-Verlag, New York, 1994. xvi+285 pp. ISBN: 0-387-94289-0.
  * [Ha10] Harman, Glyn. _Diophantine approximation with multiplicative functions_ , Montash. Math. 160 (2010), 51-57.
  * [HB94] Heath-Brown, D. R. _Odd perfect numbers_. Math. Proc. Cambridge Philos. Soc. 115 (1994), no. 2, 191-196.
  * [HB21] Heath-Brown, D. R. _The differences between consecutive primes, V._ Int. Math. Res. Not. IMRN 2021, no. 22, 17514-17562.
  * [Ho55] Hornfeck, Bernhard. _Zur Dichte der Menge der vollkommenen Zahlen._ Arch. Math. (Basel) 6 (1955), 442-443.
  * [HW57] Hornfeck, B.; Wirsing E. _Über die Häufigkeit vollkommener Zahlen_ , Math. Ann. 133 (1957), 431-438.
  * [Ja22+] Järviniemi, Olli. _On large differences between consecutive primes_. 2022. arXiv: 2212.10965 [math.NT]. https://arxiv.org/abs/2212.10965
  * [Ka54] Kanold, Hans-Joachim. Über die Dichten der Mengen der vollkommenen und der befreundeten Zahlen. Math. Z. 61 (1954), 180-185.
  * [Ka57] Kanold, Hans-Joachim. _Über die Verteilung der vollkommene Zahlen und allgemeinerer Zahlenmengen_ , Math Ann. 132 (1957), 442-450.
  * [Ma79] Makowski, A. _Some equations involving the sum of divisors_ , Elem. Math. 34 (1979), 82.
  * [Pom75] Pomerance, Carl. _On the congruences $\sigma(n)\equiv a\,(\bmod\,n)$ and $n\equiv a\,(\bmod\,\phi(n))$_, Acta Arith. 26 (1975), 265-272.
  * [Pom76a] Pomerance, Carl. _On composite $n$ for which $\phi(n)|n-1$. _ Acta Arith. 28 (1976), 387-389.
  * [Pom76b] Pomerance, Carl. _On composite $n$ for which $\phi(n)|n-1$, II. _ Pacific J. Math. 69 (1977), 177-186.
  * [Pom77] Pomerance, Carl. _Multiply perfect numbers, Mersenne primes, and effective computability._ Math. Ann. 226 (1977), no. 3, 195-206.
  * [Pol] Pollack, Paul. _Not always buried deep. A second course in elementary number theory_. American Mathematical Society, Providence, RI, 2009. xvi+303 pp. ISBN: 978-0-8218-4880-7
  * [Pol11] Pollack, Paul. _On the greatest common divisor of a number and its sum of divisors_. Michigan Math. J. 60 (2011), no. 1, 199-214.
  * [PP13] Pollack, Paul; Pomerance, Carl. _On the distribution of some integers related to perfect and amicable numbers_ , Colloq. Math. 30 (2013), 169-182.
  * [PP16] Pollack, Paul; Pomerance, Carl. Some problems of Erdös on the sum-of-divisors function. Trans. Amer. Math. Soc. Ser. B 3 (2016), 1-26.
  * [PPT18] Pollack, Paul; Pomerance, Carl; Thompson, Lola. _Divisor-sum fibres_ , Mathematika 64 (2018), 330-342.
  * [PS12] Pollack, Paul; Shevelev, Vladimir _On perfect and near-perfect numbers_. J. Number Theory 132 (2012), no. 12, 3037-3046.
  * [Sc55] Schinzel, A. _On functions $\phi(n)$ and $\sigma(n)$_, Bull. Acad. Pol. Sci. Cl. III 3 (1955), 415-419.
  * [Si65] Sierpiński, W. _Sur les nombres pseudoparfaits._ Mat. Vesnik 2(17) (1965), 212-213.
  * [St22+] Stadlmann, Julia. _On the mean square gap between primes_. 2022. arXiv: 2212. 10867 [math.NT]. https://arxiv.org/abs/2212.10867
  * [Te] Tenenbaum, G. _Introduction to analytic and probabilistic number theory_ , English ed., Cambridge University Press, Cambridge (1995).
  * [Vo56] Volkmann, Bodo. _Ein Satz über die Menge der vollkommenen Zahlen._ J. Reine Angew. Math. 195 (1955), 152-155 (1956).
  * [Wi59] Wirsing, Eduard. _Bemerkung zu der Arbeit über vollkommene Zahlen_. Math. Ann. 137 (1959), 316-318.
  * [Wo77] Wolke, Dieter. Eine Bemerkung über die Werte der Funktion $\sigma(n)$. Monatsh. Math. 83 (1977), no. 2, 163-166.


Each iteration, the \inline{mwem} algorithm selects a query from the query workload privately using the exponential mechanism. The query selected is selected by virtue of a scoring function which determines that the result of the query on the synthetic dataset greatly differs from its result on the real dataset (more so than other queries in the workload, with some amount of error). The algorithm updates the synthetic dataset using the multiplicative weights update rule, based on the query result on the real dataset with some noise added. This process continues over several iterations until the synthetic dataset reaches some some level of accuracy relative to the real dataset.

\begin{figure}
\vspace{1em}
\begin{minted}{haskell}

-- exponential mechanism
expmech :: [(Double,Double)]
-> NatS #$\epsilon $#
-> SDict #$\sigma $# LInf SDouble SDouble
-> EpsPrivacyMonad (TruncateSens #$\epsilon $# #$\sigma $#) Int

-- exponential mechanism + laplace loop
expnloop :: NatS k
-> NatS #$\epsilon $#
-> [(Double,Double)]
-> SDict #$\sigma $# LInf SDouble SDouble
-> Map.Map Double Double
-> EpsPrivacyMonad (ScalePriv (2 TL.* k) (TruncateSens #$\epsilon $# #$\sigma $#)) (Map.Map Double Double)

-- multiplicative-weights exponential mechanism
mwem :: NatS k
-> NatS #$\epsilon $#
-> [(Double,Double)]
-> SDict #$\sigma $# LInf SDouble SDouble
-> Map Double Double
-> EpsPrivacyMonad (ScalePriv (2 TL.* k) (TruncateSens #$\epsilon $# #$\sigma $#)) (Map Double Double)
mwem k #$\epsilon $# queries real_data syn_data =
expnloop k #$\epsilon $# queries real_data syn_data
\end{minted}
\caption{Multiplicative Weights Exponential Mechanism.}
\label{fig:mwem}
\end{figure}

\section{Lemmas,  Theorems \& Proofs}
\label{sec:proof}

\begingroup
\setlength{\parindent}{0pt}

% {-{ LEMMA - Plus Respects - thm:plus-respects
\begin{lemma}[Plus Respects]\label{thm:plus-respects}\ \\
If {{\color{\colorMATH}\ensuremath{r_{1} \sim ^{r} r_{2}}}} then {{\color{\colorMATH}\ensuremath{r_{1} + r_{3} \sim ^{r} r_{2} + r_{3}}}}.
\end{lemma}
\begin{proof}\ \\
By {{\color{\colorMATH}\ensuremath{|r_{1} - r_{2}| \leq  r \implies  |(r_{1} + r_{3}) - (r_{2} + r_{3})| \leq  r}}}.
\end{proof}
% }-}

% {-{ LEMMA - Times Respects - thm:times-respects
\begin{lemma}[Times Respects]\label{thm:times-respects}\ \\
If {{\color{\colorMATH}\ensuremath{r_{1} \sim ^{r} r_{2}}}} then {{\color{\colorMATH}\ensuremath{r_{3}r_{1} \sim ^{r_{3}r} r_{3}r_{2}}}}.
\end{lemma}
\begin{proof}\ \\
By {{\color{\colorMATH}\ensuremath{|r_{1} - r_{2}| \leq  r \implies  |r_{3}r_{1} - r_{3}r_{2}| \leq  r}}}.
\end{proof}
% }-}

% {-{ LEMMA - Triangle - thm:triangle
\begin{lemma}[Triangle]\label{thm:triangle}\ \\
If {{\color{\colorMATH}\ensuremath{r_{1} \sim ^{r_{A}} r_{2}}}} and {{\color{\colorMATH}\ensuremath{r_{2} \sim ^{r_{B}} r_{3}}}} then {{\color{\colorMATH}\ensuremath{r_{1} \sim ^{r_{A} + r_{B}} r_{3}}}}.
\end{lemma}
\begin{proof}\ \\
By the classic triangle inequality lemma for real numbers.
\end{proof}
% }-}

% {-{ LEMMA - Step-index Weakening - thm:step-index-weakening
\begin{lemma}[Step-index Weakening]\label{thm:step-index-weakening}\ \\
For {{\color{\colorMATH}\ensuremath{n' \leq  n}}}: (1) If {{\color{\colorMATH}\ensuremath{\gamma _{1} \sim  \gamma _{2} \in  {\mathcal{G}}_{n}^{\Sigma }\llbracket \Gamma \rrbracket }}} then {{\color{\colorMATH}\ensuremath{\gamma _{1} \sim  \gamma _{2} \in  {\mathcal{G}}_{n^{\prime}}^{\Sigma }\llbracket \Gamma \rrbracket }}}; and
(2) If {{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n}^{\Sigma }\llbracket \tau \rrbracket }}} then {{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n^{\prime}}^{\Sigma }\llbracket \tau \rrbracket }}}; and (3) If {{\color{\colorMATH}\ensuremath{\gamma _{1},e_{1} \sim
\gamma _{2},e_{2} \in  {\mathcal{E}}_{n}^{\Sigma }\llbracket \tau \rrbracket }}} then {{\color{\colorMATH}\ensuremath{\gamma _{1},e_{1} \sim  \gamma _{2},e_{2} \in  {\mathcal{E}}_{n}^{\Sigma }\llbracket \tau \rrbracket }}}.
\end{lemma}
\begin{proof}\ \\
By induction on {{\color{\colorMATH}\ensuremath{n}}} mutually for all properties; case analysis on {{\color{\colorMATH}\ensuremath{v_{1}}}} and
{{\color{\colorMATH}\ensuremath{v_{2}}}} for property (2), and case analysis on {{\color{\colorMATH}\ensuremath{e_{1}}}} and {{\color{\colorMATH}\ensuremath{e_{2}}}} for property (3).
\end{proof}
% }-}

% {-{ THEOREM - Metric Preservation - thm:metric-preservation
\begin{theorem}[Metric Preservation]\label{thm:metric-preservation}\ \\
\begin{itemize}[label={},leftmargin=0pt]\item  \begin{tabular}{r<EMAIL_ADDRESS>} If:      & {{\color{\colorMATH}\ensuremath{\gamma _{1} \sim  \gamma _{2} \in  {\mathcal{G}}_{n}^{\Sigma }\llbracket \Gamma \rrbracket }}}     & {{\color{\colorTEXT}\textnormal{{\mtextit{(H1)}}}}}
\cr  And:     & {{\color{\colorMATH}\ensuremath{ \Gamma  \vdash  e \mathrel{:} \tau }}}             & {{\color{\colorTEXT}\textnormal{{\mtextit{(H2)}}}}}
\cr  Then:    & {{\color{\colorMATH}\ensuremath{\gamma _{1},e \sim  \gamma _{2},e \in  {\mathcal{E}}_{n}^{\Sigma }\llbracket \tau \rrbracket }}} &
\end{tabular}
\item
\item  That is, either {{\color{\colorMATH}\ensuremath{n=0}}}, or {{\color{\colorMATH}\ensuremath{n = n^{\prime}+1}}} and\ldots
\item
\item  \begin{tabular}{r<EMAIL_ADDRESS>} If:      & {{\color{\colorMATH}\ensuremath{n^{\prime \prime} \leq  n^{\prime}}}}                   & {{\color{\colorTEXT}\textnormal{{\mtextit{(H3)}}}}}
\cr  And:     & {{\color{\colorMATH}\ensuremath{\gamma _{1} \vdash  e \Downarrow _{n^{\prime \prime}} v_{1}}}}           & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4)}}}}}
\cr  Then:    & {{\color{\colorMATH}\ensuremath{\exists !v_{2}.\hspace*{0.33em} \gamma _{2} \vdash  e \Downarrow _{n^{\prime \prime}} v_{2}}}}     & {{\color{\colorTEXT}\textnormal{{\mtextit{(C1)}}}}}
\cr  And:     & {{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n^{\prime}-n^{\prime \prime}}^{\Sigma }\llbracket \tau \rrbracket }}}  & {{\color{\colorTEXT}\textnormal{{\mtextit{(C2)}}}}}
\end{tabular}
\end{itemize}
\end{theorem}
% {-{ PROOF - Fundamental Property
\begin{proof}\ \\
By strong induction on {{\color{\colorMATH}\ensuremath{n}}} and case analysis on {{\color{\colorMATH}\ensuremath{e}}} and {{\color{\colorMATH}\ensuremath{\tau }}}:
\begin{itemize}[label=\textbf{-},leftmargin=*]\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=0}}}: % {-{
Trivial by definition.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=x}}}: % {-{
\item  By inversion on {\mtextit{(H4)}} we have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = 0}}} and
{{\color{\colorMATH}\ensuremath{v_{1} = \gamma _{1}(x)}}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = \gamma _{2}(x)}}} in the conclusion.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  x \Downarrow _{0} \gamma _{2}(x)}}} unique; and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{\gamma _{1}(x) \sim  \gamma _{2}(x) \in  {\mathcal{V}}_{n^{\prime}}^{\Sigma }\llbracket \tau \rrbracket }}}.
{\mtextit{(C1)}} is by {\mtextsc{ e-var}} application and inversion.
{\mtextit{(C2)}} is by {\mtextit{(H1)}} and \nameref{thm:step-index-weakening}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=r}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{real}}}}}}: % {-{
\item  By inversion on {\mtextit{(H4)}} we have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = 0}}} and
{{\color{\colorMATH}\ensuremath{v_{1} = r}}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = r}}} in the conclusion.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  r \Downarrow _{0} r}}} unique; and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{r = r}}}.
{\mtextit{(C1)}} is by {\mtextsc{ e-real}} application and inversion.
{\mtextit{(C2)}} is trivial.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=r}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{sreal}}}@\varnothing }}}: % {-{
\item  By inversion on {\mtextit{(H4)}} we have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = 0}}} and
{{\color{\colorMATH}\ensuremath{v_{1} = r}}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = r}}} in the conclusion.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  r \Downarrow _{0} r}}} unique; and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{r \sim ^{0} r}}}.
{\mtextit{(C1)}} is by {\mtextsc{ e-sreal}} application and inversion.
{\mtextit{(C2)}} is immediate by {{\color{\colorMATH}\ensuremath{|r-r| = 0 \leq  0}}}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e={\mtext{sing}}(r)}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{real}}}[r]}}}: % {-{
\item  By inversion on {\mtextit{(H4)}} we have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = 0}}} and
{{\color{\colorMATH}\ensuremath{v_{1} = r}}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = r}}} in the conclusion.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  {\mtext{sing}}(r) \Downarrow _{0} r}}} unique; and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{r = r}}}.
{\mtextit{(C1)}} is by {\mtextsc{ e-sing}} application and inversion.
{\mtextit{(C2)}} is immediate.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=e_{1}+e_{2}}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau ={{\color{\colorSYNTAX}\mtexttt{real}}}}}}: % {-{
\item  By inversion on {\mtextit{(H4)}}:
\item  \<EMAIL_ADDRESS>} \gamma _{1} &{}\vdash {}& e_{1} &{}\Downarrow _{n_{1}}{}& r_{1 1} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.1)}}}}}
\cr  \gamma _{1} &{}\vdash {}& e_{2} &{}\Downarrow _{n_{2}}{}& r_{1 2} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.2)}}}}}
\end{array}}}}
\item  and we also have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = n_{1} + n_{2}}}},
{{\color{\colorMATH}\ensuremath{v_{1} = r_{1 1}+r_{1 2}}}} and
By IH ({{\color{\colorMATH}\ensuremath{n = n_{i}}}} decreasing), {\mtextit{(H1)}}, {\mtextit{(H2)}}, {\mtextit{(H3)}}, {\mtextit{(H4.1)}} and {\mtextit{(H4.2)}} we have:
{{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{1} \Downarrow _{n_{1}} r_{2 1}}}} (unique) {\mtextit{(IH.C1.1)}};
{{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{2} \Downarrow _{n_{2}} r_{2 2}}}} (unique) {\mtextit{(IH.C1.2)}};
{{\color{\colorMATH}\ensuremath{r_{1 1} = r_{2 1}}}} {\mtextit{(IH.C2.1)}} ; and
{{\color{\colorMATH}\ensuremath{r_{1 2} = r_{2 2}}}} {\mtextit{(IH.C2.2)}} .
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = r_{2 1} + r_{2 2}}}}.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{1} + e_{2} \Downarrow _{n_{1}+n_{2}} r_{2 1} + r_{2 2}}}} (unique); and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{r_{1 1} + r_{1 2} = r_{2 1} + r_{2 2}}}}.
{\mtextit{(C1)}} is by {{\color{\colorMATH}\ensuremath{(IH.C1.1)}}}, {{\color{\colorMATH}\ensuremath{(IH.C1.2)}}}, and {\mtextsc{ e-plus}} application and inversion.
{\mtextit{(C2)}} is by {\mtextit{(IH.C2.1)}} and {\mtextit{(IH.C2.2)}}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=e_{1}+e_{2}}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma ^{\prime}}}}: % {-{
\item  By inversion on {\mtextit{(H2)}} and {\mtextit{(H4)}} we have:
\item  \<EMAIL_ADDRESS>} \Gamma   &{}\vdash {}& e_{1} &{}\mathrel{:}{}& {{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma _{1} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H2.1)}}}}}
\cr  \Gamma   &{}\vdash {}& e_{2} &{}\mathrel{:}{}& {{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma _{2} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H2.2)}}}}}
\end{array}}}}
\item  \<EMAIL_ADDRESS>} \gamma _{1} &{}\vdash {}& e_{1} &{}\Downarrow _{n_{1}}{}& r_{1 1}    & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.1)}}}}}
\cr  \gamma _{1} &{}\vdash {}& e_{2} &{}\Downarrow _{n_{2}}{}& r_{1 2}    & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.2)}}}}}
\end{array}}}}
\item  and we also have:
{{\color{\colorMATH}\ensuremath{\Sigma ^{\prime} = \Sigma _{1} + \Sigma _{2}}}},
{{\color{\colorMATH}\ensuremath{n^{\prime} = n_{1} + n_{2}}}},
{{\color{\colorMATH}\ensuremath{v_{1} = r_{1 1}+r_{1 2}}}} and
By IH ({{\color{\colorMATH}\ensuremath{n = n_{i}}}} decreasing), {\mtextit{(H1)}}, {\mtextit{(H2)}}, {\mtextit{(H3)}}, {\mtextit{(H4.1)}} and {\mtextit{(H4.2)}} we have:
{{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{1} \Downarrow _{n_{1}} r_{2 1}}}} (unique) {\mtextit{(IH.C1.1)}};
{{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{2} \Downarrow _{n_{2}} r_{2 2}}}} (unique) {\mtextit{(IH.C1.2)}};
{{\color{\colorMATH}\ensuremath{r_{1 1} \sim ^{\Sigma \mathord{\cdotp }\Sigma _{1}} r_{2 1}}}} {\mtextit{(IH.C2.1)}}; and
{{\color{\colorMATH}\ensuremath{r_{2 1} \sim ^{\Sigma \mathord{\cdotp }\Sigma _{2}} r_{2 2}}}} {\mtextit{(IH.C2.2)}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = r_{2 1} + r_{2 2}}}}.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{1} + e_{2} \Downarrow _{n_{1}+n_{2}} r_{2 1} + r_{2 2}}}} (unique); and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{r_{1 1} + r_{1 2} \sim ^{\Sigma \mathord{\cdotp }(\Sigma _{1} + \Sigma _{2})} r_{2 1} + r_{2 2}}}}.
{\mtextit{(C1)}} is by {\mtextit{(IH.C1.1)}}, {\mtextit{(IH.C1.2)}}, and {\mtextsc{ e-plus}} application and inversion.
{\mtextit{(C2)}} is by {\mtextit{(IH.C2.1)}}, {\mtextit{(IH.C2.2)}}, \nameref{thm:plus-respects} and \nameref{thm:triangle}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=e_{1}\ltimes e_{2}}}} {\mtextbf{and}} either {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{real}}}}}} {\mtextbf{or}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma ^{\prime}}}}: % {-{
\item  Similar to previous two cases, using \nameref{thm:times-respects}
instead of \nameref{thm:plus-respects}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e = {{\color{\colorSYNTAX}\mtexttt{if0}}}(e_{1})\{ e_{2}\} \{ e_{3}\} }}}: % {-{
\item  By inversion on {\mtextit{(H4)}} we have 2 subcases, each which induce:
\item  \<EMAIL_ADDRESS>} \gamma _{1} &{}\vdash {}& e_{1} &{}\Downarrow _{n_{1}}{}& b_{1} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.1)}}}}}
\end{array}}}}
\item  By IH ({{\color{\colorMATH}\ensuremath{n = n_{1}}}} decreasing), {\mtextit{(H1)}}, {\mtextit{(H2)}}, {\mtextit{(H3)}} and {\mtextit{(H4.1)}} we have:
{{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{1} \Downarrow _{n_{1}} b_{2}}}} (unique) {\mtextit{(IH.1.C1)}}; and
{{\color{\colorMATH}\ensuremath{b_{1} = b_{2}}}} {\mtextit{(IH.1.C2)}}.
\item  \begin{itemize}[label=\textbf{-},leftmargin=*]\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Subcase}} {{\color{\colorMATH}\ensuremath{b_{1} = b_{2} = {\mtext{true}}}}}:
\item  From prior inversion on {\mtextit{(H4)}} we also have:
\item  \<EMAIL_ADDRESS>} \gamma _{1} &{}\vdash {}& e_{2} &{}\Downarrow _{n_{2}}{}& v_{1}             & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.2)}}}}}
\end{array}}}}
\item  By IH ({{\color{\colorMATH}\ensuremath{n = n_{2}}}} decreasing), {\mtextit{(H1)}}, {\mtextit{(H2)}}, {\mtextit{(H3)}} and {\mtextit{(H4.2)}} we have:
{{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{2} \Downarrow _{n_{2}} v_{2}}}} (unique) {\mtextit{(IH.2.C1)}}; and
{{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n_{1}^{\Sigma } + n_{2}}\llbracket \tau \rrbracket }}} {\mtextit{(IH.2.C2)}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = v_{2}}}}.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  {{\color{\colorSYNTAX}\mtexttt{if}}}(e_{1})\{ e_{2}\} \{ e_{3}\}  \Downarrow _{n_{1}+n_{2}} v_{2}}}}; and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n_{1}^{\Sigma } + n_{2}}\llbracket \tau \rrbracket }}}.
{\mtextit{(C1)}} is by {\mtextit{(IH.1.C1)}}, {\mtextit{(IH.2.C2)}} and {\mtextsc{ e-if-true}} application and inversion.
{\mtextit{(C2)}} is by {\mtextit{(IH.2.C2)}}.
\end{itemize}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Subcase}} {{\color{\colorMATH}\ensuremath{b_{1} = b_{2} = {\mtext{false}}}}}:
\item  Analogous to case {{\color{\colorMATH}\ensuremath{b_{1} = b_{2} = {\mtext{true}}}}}.
\end{itemize}
\end{itemize}
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} either {{\color{\colorMATH}\ensuremath{e=\langle e_{1},e_{2}\rangle }}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = \tau _{1} \times  \tau _{2}}}} {\mtextbf{or}} % {-{
{{\color{\colorMATH}\ensuremath{e = \hat \langle e_{1},e_{2}\hat \rangle }}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = (\sigma _{1} \otimes  \sigma _{2})@\Sigma ^{\prime}}}}:
\item  Analogous to cases for {{\color{\colorMATH}\ensuremath{e = e_{1} + e_{2}}}} where {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{real}}}}}} or {{\color{\colorMATH}\ensuremath{\tau  =
{{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma ^{\prime}}}}, and instead of appealing to \nameref{thm:triangle},
appealing to the definition of the logical relation.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} either {{\color{\colorMATH}\ensuremath{e=\pi _{i}(e)}}} {\mtextbf{or}} {{\color{\colorMATH}\ensuremath{e=\hat \pi _{i}(e)}}}): % {-{
\item  Analogous to cases for {{\color{\colorMATH}\ensuremath{e = e_{1} + e_{2}}}} where {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{real}}}}}} or {{\color{\colorMATH}\ensuremath{\tau  =
{{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma ^{\prime}}}}, and instead of appealing to \nameref{thm:triangle},
appealing to the definition of the logical relation.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} either {{\color{\colorMATH}\ensuremath{e=e_{1}\mathrel{:: }e_{2}}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{list}}}(\tau )}}} {\mtextbf{or}} % {-{
{{\color{\colorMATH}\ensuremath{e = e_{1}\mathrel{\hat {\mathrel{:: }}}e_{2}}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{slist}}}(\sigma )@\Sigma ^{\prime}}}}:
\item  Analogous to cases for {{\color{\colorMATH}\ensuremath{e = e_{1} + e_{2}}}} where {{\color{\colorMATH}\ensuremath{\tau  = {{\color{\colorSYNTAX}\mtexttt{real}}}}}} or {{\color{\colorMATH}\ensuremath{\tau  =
{{\color{\colorSYNTAX}\mtexttt{sreal}}}@\Sigma ^{\prime}}}}, and instead of appealing to \nameref{thm:triangle},
appealing to the definition of the logical relation.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} either {{\color{\colorMATH}\ensuremath{e={{\color{\colorSYNTAX}\mtexttt{case}}}(e_{1})\{ [].e_{2}\} \{ x_{1}\mathrel{:: }x_{2}.e_{3}\} }}} {\mtextbf{or}} % {-{
{{\color{\colorMATH}\ensuremath{e = {{\color{\colorSYNTAX}\mtexttt{case}}}(e_{1})\{ \hat {[}\hat {]}.e_{2}\} \{ x_{1}\mathrel{\hat {\mathrel{:: }}}x_{2}.e_{3}\} }}}:
\item  Analogous to cases for {{\color{\colorMATH}\ensuremath{e = {{\color{\colorSYNTAX}\mtexttt{if}}}(e_{1})\{ e_{2}\} \{ e_{3}\} }}}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=\lambda _{z}x.\hspace*{0.33em}e}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{\tau  = \tau _{1} \rightarrow  \tau _{2}}}}: % {-{
By inversion on {\mtextit{(H4)}} we have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = 0}}}, and
{{\color{\colorMATH}\ensuremath{v_{1} = \langle \lambda x_{z}.\hspace*{0.33em}e\mathrel{|}\gamma _{1}\rangle }}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = \langle \lambda _{z}x.\hspace*{0.33em}e\mathrel{|}\gamma _{2}\rangle }}}.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  \lambda _{z}x.\hspace*{0.33em} e \Downarrow  \langle \lambda _{z}x.\hspace*{0.33em}e\mathrel{|}\gamma _{2}\rangle }}} unique; and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{\langle \lambda _{z}x.\hspace*{0.33em}e\mathrel{|}\gamma _{1}\rangle  \sim  \langle \lambda _{z}x.\hspace*{0.33em}e\mathrel{|}\gamma _{2}\rangle  \in  {\mathcal{V}}_{n^{\prime}}^{\Sigma }\llbracket \tau _{1} \rightarrow  \tau _{2}\rrbracket }}}.
Unfolding the definition, we must show: {{\color{\colorMATH}\ensuremath{\forall  n^{\prime \prime}\leq n^{\prime},v_{1},v_{2},.\hspace*{0.33em} v_{1} \sim  v_{2} \in
{\mathcal{V}}_{n^{\prime \prime}}^{\Sigma }\llbracket \tau _{1}\rrbracket  \Rightarrow \{ x\mapsto v_{1},z\mapsto \langle \lambda _{z}x.\hspace*{0.33em}e\mathrel{|}\gamma _{1}\rangle \} \uplus \gamma _{1},e \sim  \{ x\mapsto v_{2},z\mapsto \langle \lambda _{z}x.\hspace*{0.33em}e\mathrel{|}\gamma _{2}\rangle \} \uplus \gamma _{2},e \in
{\mathcal{E}}_{n^{\prime \prime}}^{\Sigma }\llbracket \tau _{2}\rrbracket }}}.
To show, we assume:
{{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n^{\prime}}^{\Sigma }\llbracket \tau _{1}\rrbracket }}} {\mtextit{(C2.H1)}}.
Note the following facts:
{{\color{\colorMATH}\ensuremath{\gamma _{1} \sim  \gamma _{2} \in  {\mathcal{G}}_{n^{\prime}}^{\Sigma }\llbracket \Gamma \rrbracket }}}                             {\mtextit{(F1)}}; and
{{\color{\colorMATH}\ensuremath{\{ x\mapsto v_{1}\} \uplus \gamma _{1} \sim  \{ x\mapsto v_{2}\} \uplus \gamma _{2} \in  {\mathcal{G}}_{n^{\prime}}^{\Sigma }\llbracket \{ x\mapsto \tau _{1},z\mapsto \tau _{1}\rightarrow \tau _{2}\} \uplus \Gamma \rrbracket }}} {\mtextit{(F2)}}.
{\mtextit{(F1)}} holds from {\mtextit{H1}} and {\nameref{thm:step-index-weakening}.1}.
{\mtextit{(F2)}} holds from {\mtextit{(F1)}}, {\mtextit{(C2.H1)}} and the definition of {{\color{\colorMATH}\ensuremath{\gamma  \sim  \gamma  \in  {\mathcal{G}}_{n}^{\Sigma }\llbracket \Gamma \rrbracket }}}.
Conclusion holds by IH ({{\color{\colorMATH}\ensuremath{n = n^{\prime}}}} decreasing), {{\color{\colorMATH}\ensuremath{F2}}} and {{\color{\colorMATH}\ensuremath{C2.H1}}}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} {{\color{\colorMATH}\ensuremath{e=e_{1}(e_{2})}}}: % {-{
\item  By inversion on {\mtextit{(H4)}} we have:
\item  \<EMAIL_ADDRESS>} \gamma _{1}         &{}\vdash {}& e_{1}  &{}\Downarrow _{n_{1}}{}& \langle \lambda _{z}x.\hspace*{0.33em}e_{1}^{\prime}\mathrel{|}\gamma _{1}^{\prime}\rangle        & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.1)}}}}}
\cr  \gamma _{1}         &{}\vdash {}& e_{2}  &{}\Downarrow _{n_{2}}{}& v_{1}                    & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.2)}}}}}
\cr  \{ x\mapsto v_{1},z\mapsto \langle \lambda _{z}x.\hspace*{0.33em}e_{1}^{\prime}\mathrel{|}\gamma _{1}^{\prime}\rangle \} \uplus \gamma _{1}^{\prime} &{}\vdash {}& e_{1}^{\prime} &{}\Downarrow _{n_{3}}{}& v_{1}^{\prime} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.3)}}}}}
\end{array}}}}
\item  and we also have:
{{\color{\colorMATH}\ensuremath{n^{\prime} = n_{1} + n_{2} + n_{3} + 1}}}, and
{{\color{\colorMATH}\ensuremath{v_{1} = v_{1}^{\prime}}}}.
By IH ({{\color{\colorMATH}\ensuremath{n = n^{\prime}}}} decreasing), {\mtextit{(H1)}}, {\mtextit{(H2)}}, {\mtextit{(H3)}}, {\mtextit{(H4.1)}} and {\mtextit{(H4.2)}} we have:
{{\color{\colorMATH}\ensuremath{\gamma _{2}         \vdash  e_{1}  \Downarrow _{n_{1}} \langle \lambda _{z}x.\hspace*{0.33em}e_{2}^{\prime}\mathrel{|}\gamma _{2}^{\prime}\rangle }}} {\mtextit{(IH.1.C1)}},
{{\color{\colorMATH}\ensuremath{\gamma _{2}         \vdash  e_{2}  \Downarrow _{n_{2}} v_{2}}}}              {\mtextit{(IH.2.C1)}},
{{\color{\colorMATH}\ensuremath{\langle \lambda _{z}x.\hspace*{0.33em}e_{1}^{\prime}\mathrel{|}\gamma _{1}^{\prime}\rangle  \sim  \langle \lambda _{z}x.\hspace*{0.33em}e_{2}^{\prime}\mathrel{|}\gamma _{2}^{\prime}\rangle  \in  {\mathcal{V}}_{n^{\prime}-n_{1}^{\Sigma }}\llbracket \tau _{1} \rightarrow  \tau _{2}\rrbracket }}}  {\mtextit{(IH.1.C2)}}, and
{{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n^{\prime}-n_{2}^{\Sigma }}\llbracket \tau _{1}\rrbracket }}} {\mtextit{(IH.2.C2)}}.
Note the following facts:
{{\color{\colorMATH}\ensuremath{n_{3} \leq  n^{\prime}-n_{1}-n_{2}}}}  {\mtextit{(F1)}};
{{\color{\colorMATH}\ensuremath{\gamma _{1} \sim  \gamma _{2} \in  {\mathcal{G}}_{n-n_{1}^{\Sigma }-n_{2}}\llbracket \Gamma \rrbracket }}} {\mtextit{(F2)}}; and
{{\color{\colorMATH}\ensuremath{v_{1} \sim  v_{2} \in  {\mathcal{V}}_{n-n_{1}^{\Sigma }-n_{2}}\llbracket \tau _{2}\rrbracket }}} {\mtextit{(F3)}}.
{\mtextit{(F1)}} follows from {\mtextit{(H3)}} and {{\color{\colorMATH}\ensuremath{n^{\prime} = n_{1} + n_{2} + n_{3} + 1}}}.
{\mtextit{(F2)}} and {\mtextit{(F3)}} follow from {\mtextit{(H1)}}, {\mtextit{(IH.2.C2)}} and \nameref{thm:step-index-weakening}.
By IH ({{\color{\colorMATH}\ensuremath{n = n^{\prime}-n_{1}-n_{2}}}} decreasing), {\mtextit{(H2)}}, {\mtextit{(IH.1.C2)}}, {\mtextit{(IH.2.C2)}}, {\mtextit{(F1)}}, {\mtextit{(F2)}},
{\mtextit{(F3)}} and {\mtextit{(H4.3)}} we have:
{{\color{\colorMATH}\ensuremath{\{ x\mapsto v_{2},z\mapsto \langle \lambda _{z}x.\hspace*{0.33em}e_{2}^{\prime}\mathrel{|}\gamma _{2}^{\prime}\rangle \} \uplus \gamma _{2}^{\prime} \vdash  e_{2}^{\prime} \Downarrow _{n_{3}} v_{2}^{\prime}}}}  ({\mtextit{(IH.3.C1)}}) and
{{\color{\colorMATH}\ensuremath{v_{1}^{\prime} \sim  v_{2}^{\prime} \in  {\mathcal{V}}_{n-n_{1}^{\Sigma }-n_{2}-n_{3}}\llbracket \tau _{2}\rrbracket }}}   {\mtextit{(IH.3.C2)}}.
Instantiate {{\color{\colorMATH}\ensuremath{v_{2} = v_{2}^{\prime}}}}.
To show:
{\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{\gamma _{2} \vdash  e_{1}(e_{2}) \Downarrow _{n_{1}+n_{2}+n_{3}+1} v_{2}^{\prime}}}} (unique); and
{\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{v_{1}^{\prime} \sim  v_{2}^{\prime} \in  {\mathcal{V}}_{n-n_{1 1}^{\Sigma }-n_{1 2}-n_{1 3}-1}\llbracket \tau _{2}\rrbracket }}}.
{\mtextit{(C1)}} is immediate from {\mtextit{(IH.1.C1)}}, {\mtextit{(IH.2.C1)}} and {\mtextit{(IH.3.C1)}}.
{\mtextit{(C2)}} is immediate from {\mtextit{(IH.3.C2)}} and {\nameref{thm:step-index-weakening}.2}.
\end{itemize} % }-}
\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=n^{\prime}+1}}} {\mtextbf{and}} either {{\color{\colorMATH}\ensuremath{e = {{\color{\colorSYNTAX}\mtexttt{reveal}}}(e^{\prime})}}} {\mtextbf{or}} {{\color{\colorMATH}\ensuremath{e = % {-{
{{\color{\colorSYNTAX}\mtexttt{return}}}(e^{\prime})}}} {\mtextbf{or}} {{\color{\colorMATH}\ensuremath{e = {{\color{\colorSYNTAX}\mtexttt{laplace}}}[e_{1},e_{2}](e_{3})}}} {\mtextbf{or}} {{\color{\colorMATH}\ensuremath{e = x \leftarrow  e_{1} \mathrel{;} e_{2}}}}:
\item  Follows from inductive hypothesis, post processing (for {{\color{\colorMATH}\ensuremath{{{\color{\colorSYNTAX}\mtexttt{laplace}}}}}}) and
sequential composition (for {{\color{\colorMATH}\ensuremath{x \leftarrow  e_{1} \mathrel{;} e_{2}}}}) theorems from the
differential privacy literature~\cite{privacybook}.
\end{itemize}
% }-}
\end{itemize}
\end{proof}
% }-}
% }-}

\endgroup

% % {-{ PROOF - Fundamental Property
% \begin{proof}[Proof of \nameref{thm:metric-preservation}]\ \\
%   By strong induction on {{\color{\colorMATH}\ensuremath{\tau }}} and case analysis on {{\color{\colorMATH}\ensuremath{e}}}:
%   \begin{itemize}[label=\textbf{-},leftmargin=*]\item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{n=0}}}: % {-{
%         \jn{we get rid of this case, right?}
%         Trivial by definition.
%      \end{itemize} % }-}
%   \item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{e=r}}}: % {-{
%      \item  By inversion on {\mtextit{(H3)}} and {\mtextit{(H4)}} we have
%      \item    {{\color{\colorMATH}\ensuremath{v_{1} = v_{2} = r}}},
%      \item    To show: {\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{v_{1} \sim ^{\Sigma } v_{2}}}}.
%      \item    {\mtextit{(C1)}} is immediate by definition of relation {{\color{\colorMATH}\ensuremath{\sim ^{r}}}}.
%      \end{itemize} % }-}
%   \item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{e=x}}}: % {-{
%      \item  By inversion on {\mtextit{(H3)}} and {\mtextit{(H4)}} we have:
%      \item  {{\color{\colorMATH}\ensuremath{v_{1} = \gamma _{1}(x)}}} and
%      \item  {{\color{\colorMATH}\ensuremath{v_{2} = \gamma _{2}(x)}}}.
%      \item  To show: {\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{v_{1} \sim ^{\Sigma } v_{2}}}}.
%      \item  {\mtextit{(C1)}} is immediate by {\mtextit{(H1)}}.
%      \end{itemize} % }-}
%   \item  \begin{itemize}[label={},leftmargin=0pt]\item  {\mtextbf{Case}} {{\color{\colorMATH}\ensuremath{e=e_{1}+e_{2}}}}: % {-{
%      \item  By inversion on {\mtextit{(H3)}} and {\mtextit{(H4)}} we have:
%      \item  \<EMAIL_ADDRESS>%            } \gamma _{1} &{}\vdash {}& e_{1} &{}\Downarrow {}& r_{1 1} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H3.1)}}}}}
%            \cr  \gamma _{1} &{}\vdash {}& e_{2} &{}\Downarrow {}& r_{1 2} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H3.2)}}}}}
%            \cr  \gamma _{2} &{}\vdash {}& e_{1} &{}\Downarrow {}& r_{2 1} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.1)}}}}}
%            \cr  \gamma _{2} &{}\vdash {}& e_{2} &{}\Downarrow {}& r_{2 2} & {{\color{\colorTEXT}\textnormal{{\mtextit{(H4.2)}}}}}
%            \end{array}}}}
%      \item  and we also have:
%      \item  {{\color{\colorMATH}\ensuremath{v_{1} = r_{1 1}+r_{1 2}}}} and
%      \item  {{\color{\colorMATH}\ensuremath{v_{2} = r_{2 1}+r_{2 2}}}}.
%      \item  By IH ({{\color{\colorMATH}\ensuremath{\tau }}} decreasing), {\mtextit{(H1)}}, {\mtextit{(H2)}}, {\mtextit{(H3.1)}}, and {\mtextit{(H4.1)}}, we have:
%      \item  {{\color{\colorMATH}\ensuremath{r_{1 1} \sim ^{\Sigma } r_{2 1}}}} {\mtextit{(IH.1.C3)}}. \jn{got to here...not sure}
%      \item  By unfolding the definition in {\mtextit{(IH.1.C3)}}, we have:
%      \item  {{\color{\colorMATH}\ensuremath{\Sigma _{1 1} = \Sigma _{2 1}}}}             {\mtextit{(IH.1.C3.1)}};
%      \item  {{\color{\colorMATH}\ensuremath{m_{1 1} = m_{2 1}}}}             {\mtextit{(IH.1.C3.2)}}; and
%      \item  {{\color{\colorMATH}\ensuremath{r_{1 1} \sim _{m_{1 1}^{\Sigma \mathord{\cdotp }\Sigma _{1 1}}} r_{2 1}}}} {\mtextit{(IH.1.C3.3)}}.
%      \item  Note the following facts:
%      \item  {{\color{\colorMATH}\ensuremath{n_{1 2} \leq  n-n_{1 1}}}}    {\mtextit{(F1)}}; and
%      \item  {{\color{\colorMATH}\ensuremath{\gamma _{1} \sim _{n-n_{1 1}^{\Sigma }}}}} {\mtextit{(F2)}}.
%      \item  {\mtextit{(F1)}} follows from {\mtextit{(H3)}} and {{\color{\colorMATH}\ensuremath{n_{1} = n_{1 1} + n_{1 2}}}}.
%      \item  {\mtextit{(F2)}} follows from {\mtextit{(H1)}} and {\nameref{thm:step-index-weakening}.1}.
%      \item  By IH ({{\color{\colorMATH}\ensuremath{n = n-n_{1 1}}}} decreasing), {\mtextit{(F2)}}, {\mtextit{(IH.1.C2)}}, {\mtextit{(F1)}}, {\mtextit{(H4.2)}} and {\mtextit{(H5.2)}} we have:
%      \item  {{\color{\colorMATH}\ensuremath{n_{1 2} = n_{2 2}}}}                                   {\mtextit{(IH.2.C1)}};
%      \item  {{\color{\colorMATH}\ensuremath{\sigma _{1}^{\prime \prime} \sim _{n-n_{1 1}^{\Sigma }-n_{1 2}} \sigma _{2}^{\prime \prime}}}}                     {\mtextit{(IH.2.C2)}}; and
%      \item  {{\color{\colorMATH}\ensuremath{r_{1 2}@_{m_{1 2}^{\Sigma _{1 2}}} \sim _{n_{1 1}^{\Sigma }-n_{1 2}} r_{2 2}@_{m_{2 2}^{\Sigma _{2 2}}}}}} {\mtextit{(IH.2.C3)}}.
%      \item  By unfolding the definition in {\mtextit{(IH.2.C3)}}, we have:
%      \item  {{\color{\colorMATH}\ensuremath{\Sigma _{1 2} = \Sigma _{2 2}}}}             {\mtextit{(IH.2.C3.1)}};
%      \item  {{\color{\colorMATH}\ensuremath{m_{1 2} = m_{2 2}}}}             {\mtextit{(IH.2.C3.2)}}; and
%      \item  {{\color{\colorMATH}\ensuremath{r_{1 2} \sim _{m_{1 2}^{\Sigma \mathord{\cdotp }\Sigma _{1 2}}} r_{2 2}}}} {\mtextit{(IH.2.C3.3)}}.
%      \item  To show:
%      \item  {\mtextit{(C1)}}: {{\color{\colorMATH}\ensuremath{n_{1 1} + n_{1 2} = n_{2 1} + n_{2 2}}}};
%      \item  {\mtextit{(C2)}}: {{\color{\colorMATH}\ensuremath{\sigma _{1}^{\prime \prime} \sim _{n-n_{1 1}^{\Sigma }-n_{1 2}} \sigma _{2}^{\prime \prime}}}}; and
%      \item  {\mtextit{(C3)}}:
%      \item  {{\color{\colorMATH}\ensuremath{(r_{1 1}+r_{1 2})@_{m_{1 1}^{\Sigma _{1 1}+\Sigma _{1 2}}\sqcup m_{1 2}}
%       \sim _{n-n_{1 1}^{\Sigma }-n_{1 2}}
%       (r_{2 1}+r_{2 2})@_{m_{2 1}^{\Sigma _{2 1}+\Sigma _{2 2}}\sqcup m_{2 2}}}}}.
%      \item  {\mtextit{(C1)}} is immediate from {\mtextit{(IH.1.C1)}} and {\mtextit{(IH.2.C1)}}.
%      \item  {\mtextit{(C2)}} is immediate from {\mtextit{(IH.2.C2)}}.
%      \item  To show {\mtextit{(C3)}} we must show:
%      \item  {\mtextit{(C3.1)}}: {{\color{\colorMATH}\ensuremath{\Sigma _{1 1} + \Sigma _{1 2} = \Sigma _{2 1} + \Sigma _{2 2}}}};
%      \item  {\mtextit{(C3.2)}}: {{\color{\colorMATH}\ensuremath{m_{1 1} \sqcup  m_{1 2} = m_{2 1} \sqcup  m_{2 2}}}}; and
%      \item  {\mtextit{(C3.3)}}: {{\color{\colorMATH}\ensuremath{(r_{1 1}+r_{1 2}) \sim _{m_{1 1}^{\Sigma \mathord{\cdotp }(\Sigma _{1 1}+\Sigma _{1 2})}\sqcup m_{1 2}} (r_{2 1} + r_{2 2})}}}.
%      \item  {\mtextit{(C3.1)}} is immediate from {\mtextit{(IH.1.C3.1)}} and {\mtextit{(IH.2.C3.1)}}.
%      \item  {\mtextit{(C3.2)}} is immediate from {\mtextit{(IH.1.C3.2)}} and {\mtextit{(IH.2.C3.2)}}.
%      \item  {\mtextit{(C3.3)}} holds as follows:
%      \item  By \nameref{thm:plus-respects}, {\mtextit{(IH.1.C3.3)}} and {\mtextit{(IH.2.C3.3)}}:
%      \item  {{\color{\colorMATH}\ensuremath{(r_{1 1}+r_{1 2}) \sim _{m_{1 1}^{\Sigma \mathord{\cdotp }\Sigma _{1 1}}} (r_{2 1} + r_{1 2}) \sim _{m_{1 2}^{\Sigma \mathord{\cdotp }\Sigma _{1 2}}} (r_{2 1} + r_{2 2})}}}.
%      \item  By \nameref{thm:triangle}:
%      \item  {{\color{\colorMATH}\ensuremath{(r_{1 1}+r_{1 2}) \sim _{m_{1 1}^{\Sigma \mathord{\cdotp }\Sigma _{1 1} + \Sigma \mathord{\cdotp }\Sigma _{1 2}}\sqcup m_{1 2}} (r_{2 1} + r_{2 2})}}}.
%      \item  By basic algebra:
%      \item  {{\color{\colorMATH}\ensuremath{(r_{1 1}+r_{1 2})
%       \sim _{m_{1 1}^{\Sigma \mathord{\cdotp }(\Sigma _{1 1}+\Sigma _{1 2})}\sqcup m_{1 2}}
%       (r_{2 1} + r_{2 2})}}}
%      \item  We have shown the goal.
%      \end{itemize} % }-}
%   \end{itemize}
% \end{proof}
% % }-}
\end{document}
\endinput