QuantumInfo.ForMathlib.LimSupInf

Let $y \in \mathbb{R}_{\ge 0}$ be a non-negative real number and $f: \mathbb{R}_{\ge 0} \to \mathbb{N} \to \mathbb{R}_{\ge 0} \cup \{\infty\}$ be a function. If for every $x > 0$, the limit inferior of the sequence $f(x, n)$ as $n \to \infty$ is less than or equal to $y$ (i.e., $\liminf_{n \to \infty} f(x, n) \le y$), then there exists a strictly monotone sequence of natural numbers $(n_k)_{k \in \mathbb{N}}$ such that for all $k \in \mathbb{N}$, $$f\left(\frac{1}{k+1}, n_k\right) \le y + \frac{1}{k+1}$$ where the values are considered in the extended non-negative real numbers $\overline{\mathbb{R}}_{\ge 0}$.

Let $y \in \mathbb{R}_{\geq 0}$ be a non-negative real number and $f: \mathbb{R}_{\geq 0} \to \mathbb{N} \to \overline{\mathbb{R}}_{\geq 0}$ be a function. Suppose that for every $x > 0$, the limit superior of the sequence $f(x, n)$ as $n \to \infty$ is at most $y$: $$\forall x > 0, \limsup_{n \to \infty} f(x, n) \leq y.$$ Then there exists a strictly monotone sequence of natural numbers $M: \mathbb{N} \to \mathbb{N}$ such that for every $k \in \mathbb{N}$ and every $n \geq M(k)$, the value of the function at $x = (k+1)^{-1}$ satisfies: $$f((k+1)^{-1}, n) \leq y + (k+1)^{-1}.$$

Let $y \in [0, \infty)$ and $f: \mathbb{R}_{\ge 0} \times \mathbb{N} \to [0, \infty]$ be a function. Suppose that for every $x > 0$, the limit inferior of the sequence $n \mapsto f(x, n)$ satisfies $$\liminf_{n \to \infty} f(x, n) \le y.$$ Then there exists a sequence of positive real numbers $(g_n)_{n \in \mathbb{N}}$ such that $g_n \to 0$ as $n \to \infty$, and the limit inferior of the diagonal sequence satisfies $$\liminf_{n \to \infty} f(g_n, n) \le y.$$

Let $y \in \mathbb{R}_{\ge 0}$ and let $f : \mathbb{R}_{\ge 0} \times \mathbb{N} \to [0, \infty]$ be a function. Let $z \in \mathbb{R}_{\ge 0}$ be a positive upper bound ($z > 0$). Suppose that for every $x > 0$, the limit inferior of the sequence $n \mapsto f(x, n)$ satisfies $$\liminf_{n \to \infty} f(x, n) \le y.$$ Then there exists a sequence of real numbers $(g_n)_{n \in \mathbb{N}}$ such that for all $n$, $0 < g_n < z$, the sequence converges to zero ($g_n \to 0$ as $n \to \infty$), and the limit inferior of the diagonal sequence satisfies $$\liminf_{n \to \infty} f(g_n, n) \le y.$$

Let $y \in [0, \infty)$ be a non-negative real number and $f: \mathbb{R}_{\ge 0} \to \mathbb{N} \to [0, \infty \rbrack$ be a function mapping a non-negative real $x$ and a natural number $n$ to an extended non-negative real. Suppose that for every $x > 0$, the limit superior of the sequence $n \mapsto f(x, n)$ satisfies $$\limsup_{n \to \infty} f(x, n) \le y.$$ Then there exists a sequence of positive real numbers $(g_n)_{n \in \mathbb{N}}$ such that $g_n \to 0$ as $n \to \infty$, and the limit superior of the diagonal sequence satisfies $$\limsup_{n \to \infty} f(g_n, n) \le y.$$

Let $X$ be a topological space, $(x_k)_{k \in \mathbb{N}}$ be a sequence in $X$, and $L \in X$. Let $T: \mathbb{N} \to \mathbb{N}$ be a strictly increasing sequence of natural numbers. Suppose that the sequence $(x_k)$ converges to $L$ as $k \to \infty$. If a sequence $(g_n)_{n \in \mathbb{N}}$ is defined such that for every $k \in \mathbb{N}$ and every $n$ in the interval $[T_k, T_{k+1})$, the value $g_n$ is constant and equal to $x_k$, then $(g_n)$ also converges to $L$ as $n \to \infty$.

Let $M: \mathbb{N} \to \mathbb{N}$ be a function and $P(k, n)$ be a binary predicate on natural numbers. Suppose that for every $k$ and every $L$, there exists some $n \ge L$ such that $P(k, n)$ holds. Then there exists a strictly increasing sequence of natural numbers $(T_k)_{k \in \mathbb{N}}$ such that for all $k$: 1. $T_k \ge M(k)$, and 2. there exists some $n$ in the half-open interval $[T_k, T_{k+1})$ such that $P(k, n)$ holds.

Let $\alpha$ be a type and $y \in \mathbb{R}_{\ge 0}$ be a non-negative real number. Let $f : \alpha \to \mathbb{N} \to \overline{\mathbb{R}}_{\ge 0}$ be a function into the extended non-negative reals. Suppose we have a strictly monotone sequence of natural numbers $T : \mathbb{N} \to \mathbb{N}$ and sequences $x, g : \mathbb{N} \to \alpha$ such that for every $k \in \mathbb{N}$, the sequence $g$ is constant on the interval $[T(k), T(k+1))$ with value $x_k$. If for every $k$ there exists at least one index $n$ in the block $[T(k), T(k+1))$ such that $f(x_k, n) \le y + \frac{1}{k+1}$, then the limit inferior of the sequence $f(g_n, n)$ as $n \to \infty$ is less than or equal to $y$.

Let $\alpha$ be a type, and let $y \in \mathbb{R}_{\ge 0}$ be a non-negative real number. Let $f : \alpha \to \mathbb{N} \to \mathbb{R}_{\ge 0 \infty}$ be a function mapping to the extended non-negative real numbers. Let $T : \mathbb{N} \to \mathbb{N}$ be a strictly monotone sequence representing block boundaries, and let $x : \mathbb{N} \to \alpha$ and $g : \mathbb{N} \to \alpha$ be sequences such that for every block index $k$, $g_n = x_k$ for all $n$ in the semi-open interval $[T_k, T_{k+1})$. If for every block $k$, the function values are bounded such that $f(x_k, n) \le y + (k+1)^{-1}$ for all $n \in [T_k, T_{k+1})$, then the limit superior of the sequence $f(g_n, n)$ as $n \to \infty$ is at most $y$.

Let $y_1, y_2$ be non-negative real numbers and $z$ be a positive real number ($z > 0$). Let $f_1, f_2: \mathbb{R}_{\geq 0} \times \mathbb{N} \to [0, \infty]$ be functions such that for every $x > 0$, the limit inferior of $f_1(x, n)$ as $n \to \infty$ is at most $y_1$, and the limit superior of $f_2(x, n)$ as $n \to \infty$ is at most $y_2$. Then there exists a sequence $g: \mathbb{N} \to \mathbb{R}_{\geq 0}$ such that: 1. $g(n) > 0$ for all $n \in \mathbb{N}$; 2. $g(n) < z$ for all $n \in \mathbb{N}$; 3. The sequence $g(n)$ converges to $0$ as $n \to \infty$; 4. $\liminf_{n \to \infty} f_1(g(n), n) \le y_1$; 5. $\limsup_{n \to \infty} f_2(g(n), n) \le y_2$.

Let $z \in [0, \infty]$ be an extended non-negative real number such that $z \neq \infty$. Let $(x_n)_{n \in \mathbb{N}}$ and $(y_n)_{n \in \mathbb{N}}$ be sequences of extended non-negative real numbers. If for all $n \in \mathbb{N}$, the inequality $x_n \le y_n + z$ holds, then $$\limsup_{n \to \infty} \frac{x_n}{n} \le \limsup_{n \to \infty} \frac{y_n}{n}.$$

Let $f: \mathbb{N} \to \alpha$ be a sequence in a topological space $\alpha$, and let $l$ be a filter on $\alpha$. For any natural number $k \in \mathbb{N}$, the sequence $n \mapsto f(n - k)$ converges to $l$ as $n \to \infty$ if and only if the sequence $f$ converges to $l$ as $n \to \infty$. Here, $n-k$ denotes truncated subtraction on natural numbers (returning $0$ if $n < k$).

Let $f: \alpha \to [0, \infty]$ be a function and $l$ be a filter on $\alpha$. For any constant $a \in [0, \infty]$, the limit of $f(x) - a$ as $x$ tends to $l$ is $0$ if and only if the limit superior of $f$ along $l$ is less than or equal to $a$, i.e., $$\lim_{l} (f(x) - a) = 0 \iff \limsup_{l} f \le a.$$ Note that here management of subtraction is in the context of extended non-negative real numbers ($[0, \infty]$), where $x - a = 0$ for all $x \le a$.