text:
In this section, we present numerical results generated by simulating the data phase of the communication protocol explained in \secref{sys}. We plot the probabilities of outage, transmission error and time overflow as a function of payload size for different training sequence lengths, transmit power and backoff values. Additionally, we compare the outage probability of the proposed variable-rate method with that of benchmark schemes.

\subsection{Simulation setup}
\paragraph*{Latency and reliability parameters} The most stringent motion control applications require a transmission time in the 0.25-1 ms range, while more tolerable processes might only require response times of the order of 1 ms \cite{neumann2007}. A typical factory automation system with up to 30 devices has a 1-2 ms transmission time, and a typical process control system with up to 200 field devices has a 10-15 ms transmission time \cite{schickhuber1997}. For our simulation, we choose a moderate aggregate transmission time of 1 ms. As for reliability, we choose a target outage probability of 10$^{-5}$.

\paragraph*{Miscellaneous parameters} We choose a conservative payload size of 50 Bytes (400 bits) per actuator, a total of 50 actuators, and an available bandwidth of 20 MHz. Putting together the number of actuators, their payload sizes, the available bandwidth and the transmission time, this translates into a \gls{dl} throughput of 1 bps/Hz. We suppose that the actuators and \glspl{ap} are scattered uniformly and independently over a floor area of $100\times 100$ m$^2$, an area similar to common areas of factories that have been surveyed in measurement campaigns \cite{hampicke1999,nist1951}.

\paragraph*{Path loss and blockage model} We assume a power law path loss model that gives power attenuation as a function of the distance from the transmitter, and a function of the link type: \gls{los} or \gls{nlos}. Let $\clos$ and $\cnlos$ be the reference path loss coefficients \gls{los} and \gls{nlos} links, and $\alos$ and $\anlos$ the path loss exponents. For a distance $r$, the path loss corresponding to \gls{los} and \gls{nlos} is
\begin{align}\label{eq:power_law}
\ell_{\text{L}}(r)=\clos r^{-\alos}, \; \ell_{\text{N}}(r)=\cnlos r^{-\anlos},
\end{align}
These four parameters have their values given in \cite{rappaport91}, also summarized in \tabref{t:params} along with the rest of the simulation parameter values. To determine the link type, we assume a blockage probability parametrized by a cutoff distance $d_0$ beyond which the probability of a link being \gls{los} becomes $p_0$:
\begin{align}
\plos(r) = p_0 + \indic{r\leq d_0}\,\frac{1-p_0}{d_0^2}\,(r-d_0)^2.
\end{align}

\paragraph*{Frequency band}We choose a carrier frequency of 3.5 GHz, also known as the \gls{cbrs}, where broadband networks in industrial applications are expected to deployed. Note that 20 MHz of bandwidth is consistent with the choice of the CBRS band, which is at least 50 MHz wide.

\begin{table}[t]
\centering
\caption{Values for simulation parameters.}
\label{t:params}
\begin{tabular}{ l  l}
\hline
Parameter description & Value \\
\hline
Transmission period, $T$ & 1 ms  \\
Number of actuators, $D$ & 50  \\
Number of \glspl{ap}, $A$  & 5 \\
Data per actuator, $B$ & 50 Bytes \\
Bandwidth, $W$ & 20 MHz \\
Floor area & 100$\times$100 m$^2$  \\
Backoff parameter & 0.8 \\
\gls{bs} transmit power & 23 dBm \\
Field actuator transmit power & 23 dBm \\
Noise power & -174 dBm/Hz \\
Carrier frequency & 3.5 GHz ($\lambda=$8.57 cm) \\
Path loss exponent ($\leq 10\lambda$) & 2 \\
LOS path loss exponent ($> 10\lambda$) & 3.26 \\
NLOS path loss exponent ($> 10\lambda$) & 3.93 \\
Blockage model: probability parameter $p_0$ & 0.25 \\
Blockage model: cutoff parameter $d_0$ & 15 m \\
\hline
\end{tabular}
\end{table}

\subsection{Benchmark methods}\label{ss:bench}
\newcommand{\nomr}{\textsf{R}}

We compare the outage probability for the variable-rate method to that for 4 benchmark methods described below.

\paragraph*{Cellular}\label{Sec:cellmodel}
Every \gls{ap} acts as a \gls{bs} in a cellular network with universal frequency reuse. Assuming equal cell sizes, every \gls{bs} is loaded with $D/B$ actuators, so every \gls{bs} broadcasts at a fixed rate $DB/AT$ bps.

\paragraph*{Fixed-rate} \label{Sec:wired_mbs}
According to the fixed-rate method, the \glspl{ap} use a single predetermined rate $DB/T$ bps to transmit to all of the actuators, one after another. An actuator fails to receive its data if its channel cannot support the predetermined rate (see our discussion of actuator failure in \secref{out}).

\paragraph*{Two-hop with cooperative relaying}
This method takes place in two rounds. In the first round, one \gls{ap} uses a single predetermined rate $2DB/T$ bps to broadcast a packet with the data of all actuators; actuators who are able to decode the packet are deemed \textit{successful}. Should any actuators fail to receive the packet (suppose there are $D-k$ of those), the \gls{ap} cooperates with successful actuators to broadcast the original packet a second time at a reduced rate $2(D-k)B/T$ bps.

\subsection{Simulation Results}

\paragraph*{Training has opposite effects on the probabilities of transmission error and time overflow} With high quality channel estimation using long training sequences and an appropriate rate backoff, the probability that the chosen rate exceeds channel capacity decreases. This explains why the probability of transmission error decreases monotonically with the number of pilots as can be seen in \figref{fig:te_to}. Longer training sequences, however, increases channel sounding overhead, leaving less time for data transmission and increasing the chances of time overflow. This explains why the probability of time overflow monotonically increases with the number of pilots as can be seen in \figref{fig:te_to}. Since the probability of transmission error and the probability of time overflow have an opposite sense of variation with respect to length of training sequence, an optimal point corresponding to the minimal outage probability is expected to exist and does in fact exist as observed in \figref{fig:outage_vs_l}.

\begin{figure}[t]
\centering
\subfloat[$\prob{\evso}$]{
\includegraphics[width=0.4\textwidth]{figs/out_closed_pout_ll.pdf}\label{fig:outage_vs_l}
}
\hfill
\subfloat[$\prob{\evte}$ and $\prob{\evto}$]{
\includegraphics[width=0.4\textwidth]{figs/plot_t1_tops_t2.pdf}\label{fig:te_to}
}
\caption{\figref{fig:outage_vs_l} shows $\prob{\evso}$ as a function of the length of the training sequence per actuator for a range of payload sizes. This probability decreases till the number of pilots reach a \textit{training crossover point} after which it increases sharply. \figref{fig:te_to} shows $\prob{\evte}$ and $\prob{\evto}$. $\prob{\evte}$ decreases as the length of the training sequence increases. The probability curve for a payload of $50$ B only is included because curves for other payload sizes are almost identical. On the contrary, $\prob{\evto}$ increases as training becomes longer, suggesting that there is little time left for data transmission.}
\vspace{-20pt}
\end{figure}

\paragraph*{Outage is dominated by different events for different ranges of payload size} We can draw two further conclusions by jointly looking at \figref{fig:outage_vs_l}  and \figref{fig:te_to}, showing the probabilities of outage, transmission errors, and time overflow as a function of the length of the training sequence per actuator. Comparing \figref{fig:te_to} with \figref{fig:outage_vs_l}, we observe that outage is dominated by transmission error events for small payloads. Comparing \figref{fig:te_to} with \figref{fig:outage_vs_l}, we see that outage is dominated by time overflow for large payloads.

\begin{figure}[h]
\begin{minipage}[t]{0.4\textwidth}
\includegraphics[width=\linewidth,keepaspectratio=true]{figs/out_closed_pout_bb.pdf}
\caption{The outage probability as a function of payload size per actuator for a range of training sequence lengths. This probability remains flat until the payload size reaches a \textit{payload crossover point}, beyond which the outage probability increases sharply.}
\label{fig:outage_vs_b}
\end{minipage}
\hspace*{\fill}
\begin{minipage}[t]{0.4\textwidth}
\includegraphics[width=\linewidth,keepaspectratio=true]{figs/comp_backoff.pdf}
\caption{The lowest outage probability as a function of payload size per actuator for different values of backoff.}
\label{fig:comp_backoff}
\end{minipage}
\end{figure}

\paragraph*{The main cause of outage sharply changes} Looking at \figref{fig:outage_vs_b} we observe that training decreases the outage probability for low payloads. However, we observe that training increases outage for high payloads. In relation to both \figref{fig:outage_vs_b} and \figref{fig:outage_vs_l}, we make the following observations. First, for a fixed training duration, the main cause of outage sharply transitions from transmission error to time overflow at a payload crossover point. Similarly, for a fixed payload size, the cause of outage sharply transitions from transmission error to time overflow at a training crossover point.

\paragraph*{There is an optimal backoff value for every payload size} \figref{fig:comp_backoff} shows the lowest outage probability as a function of payload size per actuator for the following values of backoff: 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, and 0.9. For this plot, we considered 3 \glspl{ap} instead of the default 5 \glspl{ap}. The reason is that the lowest outage probability for some backoff-payload size pairs was exactly zero, i.e. there was not a single realization that produced an outage. In our simulations, we observe that for every payload size, there exists an optimal backoff value that minimizes the lowest outage probability. Put differently, for a particular payload size, the backoff parameter and the number of pilots can be chosen to reduce the outage probability.

\begin{figure}[h]
\centering
\includegraphics[width=0.4\textwidth]{figs/comp_bench_smart.pdf}
\caption{Comparison of outage probabilities: simple variable-rate (VR), modified VR, fixed-rate (FR), cellular, and two-hop. In agreement with \secref{ss:reduce}, modified variable-rate has a lower outage probability than simple variable-rate.}
\vspace{-20pt}
\label{fig:comp1}
\end{figure}

\begin{figure}[h]
\centering
\subfloat[Comparison against SNR]{
\includegraphics[width=0.4\textwidth]{figs/out_txpower.pdf}\label{fig:comp3}
}
\hfill
\subfloat[Finite-SNR diversity order]{
\includegraphics[width=0.4\textwidth]{figs/div_order.pdf}\label{fig:comp4}
}
\caption{\figref{fig:comp3} compares the outage probability of the variable-rate method, with that of the two-hop and fixed-rate schemes. The comparison is shown for two values of effective throughput, namely 1 and 2.5 bpcu. \figref{fig:comp4} compares the finite-SNR diversity order, derived based on the curves in \figref{fig:comp3}.}
\vspace{-20pt}
\end{figure}

\paragraph*{Modified variable-rate considerably outperforms simple variable-rate}
In agreement with \secref{ss:reduce}, modified variable-rate has lower outage probability than simple variable-rate as seen in \figref{fig:comp1}. Additionally, the spread of these probabilities widens as the payloads get smaller and shrinks as the payloads get bigger. For 3 \glspl{ap}, the spread is about 3 orders of magnitude for 20 B payloads. For 5 \glspl{ap}, the spread appears to be significantly wider.

\paragraph*{The adaptive-rate method outperforms benchmark methods}
\figref{fig:comp1} shows the outage probability as a function of effective throughput for the VR methods in comparison to benchmark methods introduced in \secref{ss:bench}. The effective throughput is defined as the total number of bytes transmitted by the \glspl{ap} divided by the total transmission duration.
For VR, we plot the outage probability for 3 \glspl{ap} and 5 \glspl{ap}. For the cellular and FR we plot the outage probability for $A=5$. We observe that modified VR for $A=5$ outperforms all benchmarks and comes within the 10$^{-5}$ target outage probability.

\paragraph*{The adaptive-rate method has a larger diversity gain}
To focus on diversity gain of the transmission schemes, we adopt a simulation setup where all actuators exhibit a single nominal average \gls{snr}. \figref{fig:comp3} shows the outage probability against nominal \gls{snr}. We compare the outage probabilities between modified VR and benchmarks for an effective throughput of 1 and 2.5 bpcu, corresponding to $50$ B and $125$ B payloads. The corresponding empirical diversity orders, defined as the local negative slope of outage curves in log-log scale, are plotted in \figref{fig:comp4} against the outage probability. Modified VR requires considerably smaller transmit power to reach the target outage probability.  The comparison shows that regardless of packet size, the VR achieves a larger diversity gain compared to the two-hop method. This is an interesting observation given that in the two-hop method, all successful actuators help increase the cooperative diversity gain in the relaying phase whereas in VR has the cooperative diversity gain from only 5 \glspl{ap} and it is mainly reliant on multi-user scheduling to achieve a large diversity order. Comparing the diversity order of VR to that of FR is also insightful. Relying on cooperation of 5 \glspl{ap}, the diversity order of FR method quickly saturates at 5 while VR reaches a significantly higher diversity order.


text:
/-
Copyright (c) 2019 Rohan Mitta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rohan Mitta, Kevin Buzzard, Alistair Tucker, Johannes Hölzl, Yury Kudryashov
-/
import analysis.specific_limits.basic
import data.setoid.basic
import dynamics.fixed_points.topology

/-!
# Contracting maps

A Lipschitz continuous self-map with Lipschitz constant `K < 1` is called a *contracting map*.
In this file we prove the Banach fixed point theorem, some explicit estimates on the rate
of convergence, and some properties of the map sending a contracting map to its fixed point.

## Main definitions

* `contracting_with K f` : a Lipschitz continuous self-map with `K < 1`;
* `efixed_point` : given a contracting map `f` on a complete emetric space and a point `x`
  such that `edist x (f x) ≠ ∞`, `efixed_point f hf x hx` is the unique fixed point of `f`
  in `emetric.ball x ∞`;
* `fixed_point` : the unique fixed point of a contracting map on a complete nonempty metric space.

## Tags

contracting map, fixed point, Banach fixed point theorem
-/

open_locale nnreal topological_space classical ennreal
open filter function

variables {α : Type*}

/-- A map is said to be `contracting_with K`, if `K < 1` and `f` is `lipschitz_with K`. -/
def contracting_with [emetric_space α] (K : ℝ≥0) (f : α → α) :=
(K < 1) ∧ lipschitz_with K f

namespace contracting_with

variables [emetric_space α] [cs : complete_space α] {K : ℝ≥0} {f : α → α}

open emetric set

lemma to_lipschitz_with (hf : contracting_with K f) : lipschitz_with K f := hf.2

lemma one_sub_K_pos' (hf : contracting_with K f) : (0:ℝ≥0∞) < 1 - K := by simp [hf.1]

lemma one_sub_K_ne_zero (hf : contracting_with K f) : (1:ℝ≥0∞) - K ≠ 0 :=
ne_of_gt hf.one_sub_K_pos'

lemma one_sub_K_ne_top : (1:ℝ≥0∞) - K ≠ ∞ :=
by { norm_cast, exact ennreal.coe_ne_top }

lemma edist_inequality (hf : contracting_with K f) {x y} (h : edist x y ≠ ∞) :
  edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - K) :=
suffices edist x y ≤ edist x (f x) + edist y (f y) + K * edist x y,
  by rwa [ennreal.le_div_iff_mul_le (or.inl hf.one_sub_K_ne_zero) (or.inl one_sub_K_ne_top),
    mul_comm, ennreal.sub_mul (λ _ _, h), one_mul, tsub_le_iff_right],
calc edist x y ≤ edist x (f x) + edist (f x) (f y) + edist (f y) y : edist_triangle4 _ _ _ _
  ... = edist x (f x) + edist y (f y) + edist (f x) (f y) : by rw [edist_comm y, add_right_comm]
  ... ≤ edist x (f x) + edist y (f y) + K * edist x y : add_le_add le_rfl (hf.2 _ _)

lemma edist_le_of_fixed_point (hf : contracting_with K f) {x y}
  (h : edist x y ≠ ∞) (hy : is_fixed_pt f y) :
  edist x y ≤ (edist x (f x)) / (1 - K) :=
by simpa only [hy.eq, edist_self, add_zero] using hf.edist_inequality h

lemma eq_or_edist_eq_top_of_fixed_points (hf : contracting_with K f) {x y}
  (hx : is_fixed_pt f x) (hy : is_fixed_pt f y) :
  x = y ∨ edist x y = ∞ :=
begin
  refine or_iff_not_imp_right.2 (λ h, edist_le_zero.1 _),
  simpa only [hx.eq, edist_self, add_zero, ennreal.zero_div]
    using hf.edist_le_of_fixed_point h hy
end

/-- If a map `f` is `contracting_with K`, and `s` is a forward-invariant set, then
restriction of `f` to `s` is `contracting_with K` as well. -/
lemma restrict (hf : contracting_with K f) {s : set α} (hs : maps_to f s s) :
  contracting_with K (hs.restrict f s s) :=
⟨hf.1, λ x y, hf.2 x y⟩

include cs

/-- Banach fixed-point theorem, contraction mapping theorem, `emetric_space` version.
A contracting map on a complete metric space has a fixed point.
We include more conclusions in this theorem to avoid proving them again later.

The main API for this theorem are the functions `efixed_point` and `fixed_point`,
and lemmas about these functions. -/
theorem exists_fixed_point (hf : contracting_with K f) (x : α) (hx : edist x (f x) ≠ ∞) :
  ∃ y, is_fixed_pt f y ∧ tendsto (λ n, f^[n] x) at_top (𝓝 y) ∧
    ∀ n:ℕ, edist (f^[n] x) y ≤ (edist x (f x)) * K^n / (1 - K) :=
have cauchy_seq (λ n, f^[n] x),
from cauchy_seq_of_edist_le_geometric K (edist x (f x)) (ennreal.coe_lt_one_iff.2 hf.1)
  hx (hf.to_lipschitz_with.edist_iterate_succ_le_geometric x),
let ⟨y, hy⟩ := cauchy_seq_tendsto_of_complete this in
⟨y, is_fixed_pt_of_tendsto_iterate hy hf.2.continuous.continuous_at, hy,
  edist_le_of_edist_le_geometric_of_tendsto K (edist x (f x))
    (hf.to_lipschitz_with.edist_iterate_succ_le_geometric x) hy⟩

variable (f) -- avoid `efixed_point _` in pretty printer

/-- Let `x` be a point of a complete emetric space. Suppose that `f` is a contracting map,
and `edist x (f x) ≠ ∞`. Then `efixed_point` is the unique fixed point of `f`
in `emetric.ball x ∞`. -/
noncomputable def efixed_point (hf : contracting_with K f) (x : α) (hx : edist x (f x) ≠ ∞) :
  α :=
classical.some $ hf.exists_fixed_point x hx

variables {f}

lemma efixed_point_is_fixed_pt (hf : contracting_with K f) {x : α} (hx : edist x (f x) ≠ ∞) :
  is_fixed_pt f (efixed_point f hf x hx) :=
(classical.some_spec $ hf.exists_fixed_point x hx).1

lemma tendsto_iterate_efixed_point (hf : contracting_with K f) {x : α} (hx : edist x (f x) ≠ ∞) :
  tendsto (λn, f^[n] x) at_top (𝓝 $ efixed_point f hf x hx) :=
(classical.some_spec $ hf.exists_fixed_point x hx).2.1

lemma apriori_edist_iterate_efixed_point_le (hf : contracting_with K f)
  {x : α} (hx : edist x (f x) ≠ ∞) (n : ℕ) :
  edist (f^[n] x) (efixed_point f hf x hx) ≤ (edist x (f x)) * K^n / (1 - K) :=
(classical.some_spec $ hf.exists_fixed_point x hx).2.2 n

lemma edist_efixed_point_le (hf : contracting_with K f) {x : α} (hx : edist x (f x) ≠ ∞) :
  edist x (efixed_point f hf x hx) ≤ (edist x (f x)) / (1 - K) :=
by { convert hf.apriori_edist_iterate_efixed_point_le hx 0, simp only [pow_zero, mul_one] }

lemma edist_efixed_point_lt_top (hf : contracting_with K f) {x : α} (hx : edist x (f x) ≠ ∞) :
  edist x (efixed_point f hf x hx) < ∞ :=
(hf.edist_efixed_point_le hx).trans_lt (ennreal.mul_lt_top hx $
  ennreal.inv_ne_top.2 hf.one_sub_K_ne_zero)

lemma efixed_point_eq_of_edist_lt_top (hf : contracting_with K f) {x : α} (hx : edist x (f x) ≠ ∞)
  {y : α} (hy : edist y (f y) ≠ ∞) (h : edist x y ≠ ∞) :
  efixed_point f hf x hx = efixed_point f hf y hy :=
begin
  refine (hf.eq_or_edist_eq_top_of_fixed_points _ _).elim id (λ h', false.elim (ne_of_lt _ h'));
    try { apply efixed_point_is_fixed_pt },
  change edist_lt_top_setoid.rel _ _,
  transitivity x, by { symmetry, exact hf.edist_efixed_point_lt_top hx },
  transitivity y,
  exacts [lt_top_iff_ne_top.2 h, hf.edist_efixed_point_lt_top hy]
end

omit cs

/-- Banach fixed-point theorem for maps contracting on a complete subset. -/
theorem exists_fixed_point' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  ∃ y ∈ s, is_fixed_pt f y ∧ tendsto (λ n, f^[n] x) at_top (𝓝 y) ∧
    ∀ n:ℕ, edist (f^[n] x) y ≤ (edist x (f x)) * K^n / (1 - K) :=
begin
  haveI := hsc.complete_space_coe,
  rcases hf.exists_fixed_point ⟨x, hxs⟩ hx with ⟨y, hfy, h_tendsto, hle⟩,
  refine ⟨y, y.2, subtype.ext_iff_val.1 hfy, _, λ n, _⟩,
  { convert (continuous_subtype_coe.tendsto _).comp h_tendsto, ext n,
    simp only [(∘), maps_to.iterate_restrict, maps_to.coe_restrict_apply, subtype.coe_mk] },
  { convert hle n,
    rw [maps_to.iterate_restrict, eq_comm, maps_to.coe_restrict_apply, subtype.coe_mk] }
end

variable (f) -- avoid `efixed_point _` in pretty printer

/-- Let `s` be a complete forward-invariant set of a self-map `f`. If `f` contracts on `s`
and `x ∈ s` satisfies `edist x (f x) ≠ ∞`, then `efixed_point'` is the unique fixed point
of the restriction of `f` to `s ∩ emetric.ball x ∞`. -/
noncomputable def efixed_point' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) (x : α) (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  α :=
classical.some $ hf.exists_fixed_point' hsc hsf hxs hx

variables {f}

lemma efixed_point_mem' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  efixed_point' f hsc hsf hf x hxs hx ∈ s :=
(classical.some_spec $ hf.exists_fixed_point' hsc hsf hxs hx).fst

lemma efixed_point_is_fixed_pt' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  is_fixed_pt f (efixed_point' f hsc hsf hf x hxs hx) :=
(classical.some_spec $ hf.exists_fixed_point' hsc hsf hxs hx).snd.1

lemma tendsto_iterate_efixed_point' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  tendsto (λn, f^[n] x) at_top (𝓝 $ efixed_point' f hsc hsf hf x hxs hx) :=
(classical.some_spec $ hf.exists_fixed_point' hsc hsf hxs hx).snd.2.1

lemma apriori_edist_iterate_efixed_point_le' {s : set α} (hsc : is_complete s)
  (hsf : maps_to f s s) (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s)
  (hx : edist x (f x) ≠ ∞) (n : ℕ) :
  edist (f^[n] x) (efixed_point' f hsc hsf hf x hxs hx) ≤ (edist x (f x)) * K^n / (1 - K) :=
(classical.some_spec $ hf.exists_fixed_point' hsc hsf hxs hx).snd.2.2 n

lemma edist_efixed_point_le' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  edist x (efixed_point' f hsc hsf hf x hxs hx) ≤ (edist x (f x)) / (1 - K) :=
by { convert hf.apriori_edist_iterate_efixed_point_le' hsc hsf hxs hx 0,
  rw [pow_zero, mul_one] }

lemma edist_efixed_point_lt_top' {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hf : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
  edist x (efixed_point' f hsc hsf hf x hxs hx) < ∞ :=
(hf.edist_efixed_point_le' hsc hsf hxs hx).trans_lt (ennreal.mul_lt_top hx $
  ennreal.inv_ne_top.2 hf.one_sub_K_ne_zero)

/-- If a globally contracting map `f` has two complete forward-invariant sets `s`, `t`,
and `x ∈ s` is at a finite distance from `y ∈ t`, then the `efixed_point'` constructed by `x`
is the same as the `efixed_point'` constructed by `y`.

This lemma takes additional arguments stating that `f` contracts on `s` and `t` because this way
it can be used to prove the desired equality with non-trivial proofs of these facts. -/
lemma efixed_point_eq_of_edist_lt_top' (hf : contracting_with K f)
  {s : set α} (hsc : is_complete s) (hsf : maps_to f s s)
  (hfs : contracting_with K $ hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞)
  {t : set α} (htc : is_complete t) (htf : maps_to f t t)
  (hft : contracting_with K $ htf.restrict f t t) {y : α} (hyt : y ∈ t) (hy : edist y (f y) ≠ ∞)
  (hxy : edist x y ≠ ∞) :
  efixed_point' f hsc hsf hfs x hxs hx = efixed_point' f htc htf hft y hyt hy :=
begin
  refine (hf.eq_or_edist_eq_top_of_fixed_points _ _).elim id (λ h', false.elim (ne_of_lt _ h'));
    try { apply efixed_point_is_fixed_pt' },
  change edist_lt_top_setoid.rel _ _,
  transitivity x, by { symmetry, apply edist_efixed_point_lt_top' },
  transitivity y,
  exact lt_top_iff_ne_top.2 hxy,
  apply edist_efixed_point_lt_top'
end

end contracting_with

namespace contracting_with

variables [metric_space α] {K : ℝ≥0} {f : α → α} (hf : contracting_with K f)
include hf

lemma one_sub_K_pos (hf : contracting_with K f) : (0:ℝ) < 1 - K := sub_pos.2 hf.1

lemma dist_le_mul (x y : α) : dist (f x) (f y) ≤ K * dist x y :=
hf.to_lipschitz_with.dist_le_mul x y

lemma dist_inequality (x y) : dist x y ≤ (dist x (f x) + dist y (f y)) / (1 - K) :=
suffices dist x y ≤ dist x (f x) + dist y (f y) + K * dist x y,
  by rwa [le_div_iff hf.one_sub_K_pos, mul_comm, sub_mul, one_mul, sub_le_iff_le_add],
calc dist x y ≤ dist x (f x) + dist y (f y) + dist (f x) (f y) : dist_triangle4_right _ _ _ _
          ... ≤ dist x (f x) + dist y (f y) + K * dist x y :
  add_le_add_left (hf.dist_le_mul _ _) _

lemma dist_le_of_fixed_point (x) {y} (hy : is_fixed_pt f y) :
  dist x y ≤ (dist x (f x)) / (1 - K) :=
by simpa only [hy.eq, dist_self, add_zero] using hf.dist_inequality x y

theorem fixed_point_unique' {x y} (hx : is_fixed_pt f x) (hy : is_fixed_pt f y) : x = y :=
(hf.eq_or_edist_eq_top_of_fixed_points hx hy).resolve_right (edist_ne_top _ _)

/-- Let `f` be a contracting map with constant `K`; let `g` be another map uniformly
`C`-close to `f`. If `x` and `y` are their fixed points, then `dist x y ≤ C / (1 - K)`. -/
lemma dist_fixed_point_fixed_point_of_dist_le' (g : α → α)
  {x y} (hx : is_fixed_pt f x) (hy : is_fixed_pt g y) {C} (hfg : ∀ z, dist (f z) (g z) ≤ C) :
  dist x y ≤ C / (1 - K) :=
calc dist x y = dist y x                     : dist_comm x y
          ... ≤ (dist y (f y)) / (1 - K)     : hf.dist_le_of_fixed_point y hx
          ... = (dist (f y) (g y)) / (1 - K) : by rw [hy.eq, dist_comm]
          ... ≤ C / (1 - K)                  : (div_le_div_right hf.one_sub_K_pos).2 (hfg y)

noncomputable theory

variables [nonempty α] [complete_space α]

variable (f)
/-- The unique fixed point of a contracting map in a nonempty complete metric space. -/
def fixed_point : α :=
efixed_point f hf _ (edist_ne_top (classical.choice ‹nonempty α›) _)
variable {f}

/-- The point provided by `contracting_with.fixed_point` is actually a fixed point. -/
lemma fixed_point_is_fixed_pt : is_fixed_pt f (fixed_point f hf) :=
hf.efixed_point_is_fixed_pt _

lemma fixed_point_unique {x} (hx : is_fixed_pt f x) : x = fixed_point f hf :=
hf.fixed_point_unique' hx hf.fixed_point_is_fixed_pt

lemma dist_fixed_point_le (x) : dist x (fixed_point f hf) ≤ (dist x (f x)) / (1 - K) :=
hf.dist_le_of_fixed_point x hf.fixed_point_is_fixed_pt

/-- Aposteriori estimates on the convergence of iterates to the fixed point. -/
lemma aposteriori_dist_iterate_fixed_point_le (x n) :
  dist (f^[n] x) (fixed_point f hf) ≤ (dist (f^[n] x) (f^[n+1] x)) / (1 - K) :=
by { rw [iterate_succ'], apply hf.dist_fixed_point_le }

lemma apriori_dist_iterate_fixed_point_le (x n) :
  dist (f^[n] x) (fixed_point f hf) ≤ (dist x (f x)) * K^n / (1 - K) :=
le_trans (hf.aposteriori_dist_iterate_fixed_point_le x n) $
  (div_le_div_right hf.one_sub_K_pos).2 $
    hf.to_lipschitz_with.dist_iterate_succ_le_geometric x n

lemma tendsto_iterate_fixed_point (x) :
  tendsto (λn, f^[n] x) at_top (𝓝 $ fixed_point f hf) :=
begin
  convert tendsto_iterate_efixed_point hf (edist_ne_top x _),
  refine (fixed_point_unique _ _).symm,
  apply efixed_point_is_fixed_pt
end

lemma fixed_point_lipschitz_in_map {g : α → α} (hg : contracting_with K g)
  {C} (hfg : ∀ z, dist (f z) (g z) ≤ C) :
  dist (fixed_point f hf) (fixed_point g hg) ≤ C / (1 - K) :=
hf.dist_fixed_point_fixed_point_of_dist_le' g hf.fixed_point_is_fixed_pt
  hg.fixed_point_is_fixed_pt hfg

omit hf

/-- If a map `f` has a contracting iterate `f^[n]`, then the fixed point of `f^[n]` is also a fixed
point of `f`. -/
lemma is_fixed_pt_fixed_point_iterate {n : ℕ} (hf : contracting_with K (f^[n])) :
  is_fixed_pt f (hf.fixed_point (f^[n])) :=
begin
  set x := hf.fixed_point (f^[n]),
  have hx : (f^[n] x) = x := hf.fixed_point_is_fixed_pt,
  have := hf.to_lipschitz_with.dist_le_mul x (f x),
  rw [← iterate_succ_apply, iterate_succ_apply', hx] at this,
  contrapose! this,
  have := dist_pos.2 (ne.symm this),
  simpa only [nnreal.coe_one, one_mul, nnreal.val_eq_coe] using (mul_lt_mul_right this).mpr hf.left
end

end contracting_with

subset_name: curated


TITLE: Smallest pairs to be added to a set to make it an equivalence relation
QUESTION [0 upvotes]: $$R = \{(1,1), (1,3), (1,5), (4,4),(4,6)\}, \quad A = \{1,2,3,4,5,6\}$$

Determine the smallest set of pairs of elements which needs to be added to $R$ so that the resulting relation $\Bbb{R}^*$ is an equivalance relation.

My atttempt:
In order for it to equivalent relation it needs to be reflective, symmetric and transitive.
This would mean that the lowest reflective pair is $(1,1)$ which is already in $\Bbb{R}$.
There seem to be no transitive pairs within $\Bbb{R}$ and no symmetric pairs either.
Question: I am wondering how would this solved as I assumed you would write out all the other pairs that are not in $\Bbb{R}$ which would make up $\Bbb{R}^*$.

REPLY [0 votes]: This would mean that the lowest reflective pair is $(1,1)$ which is already in
  R.

You need to add the least amount of pairs needed to make $R^\ast$ reflexive.   Merely having $(1,1)$ will not make $R^\ast$ reflexive, on its own.   Some new pairs will need to be added.
To be reflexive will require that $\forall x\in A: (x,x)\in R^\ast$, what is, for every element $x$ in $\{1,2,3,4,5,6\}$ the pair $(x,x)$ needs to be in $R^\ast$.   So what pairs need to be added to make this so?

There seem to be no transitive pairs within $R$ and no symmetric pairs either.

Indeed, that is why they need to be added.   Your task is to add the fewest necessary pairs to make $R^\ast$ transitive and symmetric.   (PS: remember the pairs added above will still be needed to be in $R^\ast$.)
Start with symmetry.