In this Mizar article, we complete the formalization of one of the items from Abad and Abad’s challenge list of “Top 100 Theorems” about Liouville numbers and the existence of transcendental numbers. It is item #18 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/. Liouville numbers were introduced by Joseph Liouville in 1844 [15] as an example of an object which can be approximated “quite closely” by a sequence of rational numbers. A real...

We present a method for constructing almost periodic sequences and functions with values in a metric space. Applying this method, we find almost periodic sequences and functions with prescribed values. Especially, for any totally bounded countable set $X$ in a metric space, it is proved the existence of an almost periodic sequence ${\left\{{\psi }_k\right\}}_{k\in \mathbb{Z}}$ such that $\{{\psi }_k;k\in \mathbb{Z}\}=X$ and ${\psi }_k={\psi }_{k+lq\left(k\right)}$, $l\in \mathbb{Z}$ for all $k$ and some $q\left(k\right)\in \mathbb{N}$ which depends on $k$.

Let $Q={\left(Q_k\right)}_{k\ge 0},Q_0=1,Q_{k+1}=q_k{Q}_k,q_k\ge 2$, be a Cantor scale, ${𝐙}_Q$ the compact projective limit group of the groups $𝐙/Q_k𝐙$, identified to ${\prod }_{0\le j\le k-1}𝐙/q_j𝐙$, and let $\mu$ be its normalized Haar measure. To an element $x=\{a_0,a_1,a_2,\cdots \},0\le a_k\le q_{k+1}-1$, of ${𝐙}_Q$ we associate the sequence of integral valued random variables $x_k={\sum }_{0\le j\le k}{a}_j{Q}_j$. The main result of this article is that, given a complex $𝐐$-multiplicative function $g$ of modulus $1$, we have$$\underset{x_k\to x}{lim}(\frac{1}{x_k}\sum _{n\le x_k-1}g\left(n\right)-\prod _{0\le j\le k}\frac{1}{q_j}\sum _{0\le a\le q_j}g\left(a{Q}_j\right))=0\mu \text{-a.e}.$$

A new class of $b$-adic normal numbers is built recursively by using Eulerian paths in a sequence of de Bruijn digraphs. In this recursion, a path is constructed as an extension of the previous one, in such way that the $b$-adic block determined by the path contains the maximal number of different $b$-adic subblocks of consecutive lengths in the most compact arrangement. Any source of redundancy is avoided at every step. Our recursive construction is an alternative to the several well-known concatenative...

Duffin and Schaeffer have generalized the classical theorem of Khintchine in metric Diophantine approximation in the case of any error function under the assumption that all the rational approximants are irreducible. This result is extended to the case where the numerators and the denominators of the rational approximants are related by a congruential constraint stronger than coprimality.

We prove a version of the Khinchin-Groshev theorem in Diophantine approximation for quadratic extensions of function fields in positive characteristic.