QuantumInfo.Regularized

Let $T$ be a conditionally complete linear order (typically $\mathbb{R}$ or $\overline{\mathbb{R}}$). Given a sequence of values $f: \mathbb{N} \to T$, and assuming the sequence is bounded such that there exist constants $lb$ and $ub$ satisfying $lb \leq f(n) \leq ub$ for all $n \in \mathbb{N}$, the inf-regularized value is defined as the limit inferior of the sequence as $n$ approaches infinity: $$\liminf_{n \to \infty} f(n)$$ In the context of information theory, this is often used to derive asymptotic rates from one-shot quantities.

Let $T$ be a type equipped with a complete lattice structure (such as the extended real numbers). For a sequence $f: \mathbb{N} \to T$ and given lower and upper bounds $lb, ub \in T$ such that $lb \leq f(n) \leq ub$ for all $n \in \mathbb{N}$, the `SupRegularized` value is defined as the limit superior of the sequence as $n$ approaches infinity: $$\limsup_{n \to \infty} f(n)$$ This definition is typically used in information theory to regularize "one-shot" quantities into asymptotic rates.

Let $f: \mathbb{N} \to T$ be a sequence of quantities in a type $T$ equipped with a partial order. If there exists a lower bound $lb$ such that $lb \leq f(n)$ for all $n \in \mathbb{N}$ (and an upper bound to ensure the existence of the regularized value), then $lb$ is also a lower bound for the regularized quantity $\text{InfRegularized}(f)$, i.e., $lb \leq \text{InfRegularized}(f)$.

Given a sequence $\{f_n\}_{n \in \mathbb{N}}$ such that each term is bounded below by $lb$ and above by $ub$, the regularized infimum (denoted $\text{InfRegularized}$) of the sequence is less than or equal to the upper bound $ub$.

Let $f: \mathbb{N} \to T$ be a sequence of values in a complete lattice $T$ that is bounded below by $lb$ and above by $ub$. If the function $f$ is antitone (i.e., $n \le m$ implies $f(n) \ge f(m)$), then its regularized limit $\text{InfRegularized}(f)$ is equal to the infimum of the range of the function, denoted by $\inf_{n \in \mathbb{N}} f(n)$.

Let $fn: \mathbb{N} \to T$ be a function such that it is bounded below by $lb$ and above by $ub$. If $fn$ is an antitone function, then for every $n \in \mathbb{N}$, the regularized quantity $\text{InfRegularized}(fn)$ is less than or equal to $fn(n)$.

Let $f: \mathbb{N} \to T$ be a sequence in a partially ordered set $T$ that is bounded below by $lb$ (i.e., $\forall n, lb \le f(n)$) and bounded above by $ub$ (i.e., $\forall n, f(n) \le ub$). Then the regularized supremum of the sequence, denoted as $\text{SupRegularized}(f)$, is lower bounded by $lb$. That is, $lb \le \text{SupRegularized}(f)$.

Let $f: \mathbb{N} \to T$ be a sequence of values in a partially ordered type $T$. If the sequence is bounded below by $lb$ and above by $ub$, then the regularized supremum of the sequence, denoted as $\text{SupRegularized}(f)$, is less than or equal to the upper bound $ub$.

Let $f: \mathbb{N} \to T$ be a sequence of values in a type $T$ equipped with a complete lattice structure (or a structure where the supremum exists). If the sequence $f$ is monotone, then its regularized supremum, denoted as $\text{SupRegularized}(f, h_l, h_u)$, is equal to the supremum of the set of all values in the sequence, i.e., $\sup \{ f(n) \mid n \in \mathbb{N} \}$. Here, $h_l$ and $h_u$ are the respective proofs that the sequence is bounded below and above.

Let $f: \mathbb{N} \to T$ be a sequence of values in a type $T$ equipped with a partial order. If $f$ is a monotone function, then for every $n \in \mathbb{N}$, the value $f(n)$ is less than or equal to the regularized supremum of the sequence, denoted as $\text{SupRegularized}(f)$. Here, $h_l$ and $h_u$ are proofs that the sequence is bounded below and above, respectively.

The regularized infimum of a sequence $f_n$ with lower bound $lb$ and upper bound $ub$ is equal to the negative of the regularized supremum of the sequence $-f_n$ (with substituted bounds $-ub$ and $-lb$). Specifically, $$\text{InfRegularized}(f_n, lb, ub) = -\text{SupRegularized}(-f_n, -ub, -lb)$$ where the bounds are valid since $lb \leq f_n \leq ub$ implies $-ub \leq -f_n \leq -lb$.

For a sequence $f: \mathbb{N} \to T$ that is bounded below by $lb$ (with proof $h_l$) and bounded above by $ub$ (with proof $h_u$), the regularized supremum $\text{SupRegularized}(f)$ is equal to the negative of the regularized infimum of the negated sequence $-f$ (with bounds $-ub$ and $-lb$). Mathematically, $$\text{SupRegularized}(f, lb, ub) = -\text{InfRegularized}(-f, -ub, -lb)$$ where the validity of the new bounds follows from the fact that $lb \leq f_n \leq ub$ implies $-ub \leq -f_n \leq -lb$.

Let $f_n$ be a sequence of values indexed by natural numbers $n \in \mathbb{N}$ that is bounded by $lb \le f_n \le ub$ for all $n$. If the sequence $f_n$ is antitone (monotonically non-increasing), then the sequence converges to its regularized infimum as $n$ tends to infinity. That is, $$\lim_{n \to \infty} f_n = \text{InfRegularized}(f_n, lb, ub)$$ where the limit is taken with respect to the filter of neighborhoods of the $\text{InfRegularized}$ value.

Let $f_n$ be a sequence of values indexed by natural numbers $n \in \mathbb{N}$, and let $lb$ and $ub$ be lower and upper bounds such that $lb \leq f_n \leq ub$ for all $n$. If the function $g(n) = f_n \cdot n$ is subadditive (i.e., $g(n+m) \leq g(n) + g(m)$ for all $n, m$), then the subadditive limit of $g$ (defined by Fekete's Lemma as $\lim_{n \to \infty} \frac{g(n)}{n}$) is equal to the regularized value $\text{InfRegularized}(f_n)$.