QuantumInfo.ForMathlib.Filter

For any natural number $m$, the limit of the sequence $f(x) = \frac{1}{x} \cdot \lfloor \frac{x}{m} \rfloor$ as $x$ tends to infinity is $\frac{1}{m}$. Here, $x$ and $m$ are natural numbers, the division $x/m$ denotes integer division (the floor of the quotient), and the calculations are performed in the real numbers $\mathbb{R}$.

Let $\iota$ be a type and $f: \iota \to [0, \infty]$ be a function. Let $\mathcal{F}$ be a filter on $\iota$, and let $x \in [0, \infty]$. If $f(i)$ is eventually not equal to $\infty$ with respect to $\mathcal{F}$ (i.e., $\{i \mid f(i) \neq \infty\} \in \mathcal{F}$) and $x \neq \infty$, then the function $n \mapsto \text{toReal}(f(n))$ converges to $\text{toReal}(x)$ along $\mathcal{F}$ if and only if $f$ converges to $x$ along $\mathcal{F}$ in the extended non-negative real numbers. Here, $\text{toReal}$ denotes the coercion from $[0, \infty]$ to $\mathbb{R}$, where $\infty$ maps to $0$.