English
A LiouvilleWith statement provides a constructive bound; the existence of a positive C with infinitely many n for which there exists m with x ≠ m/n and |x − m/n| < C / n^p.
Русский
Утверждение LiouvilleWith обеспечивает конструктивную границу: существует положительная константа C и бесконечно многие n, для которых существует m с x ≠ m/n и |x − m/n| < C / n^p.
LaTeX
$$$ \exists C > 0, \exists^\infty n \in \mathbb N, \exists m \in \mathbb Z,\ x \neq m/n \land |x - m/n| < C / n^p$$$
Lean4
/-- We say that a real number `x` is a Liouville number with exponent `p : ℝ` if there exists a real
number `C` such that for infinitely many denominators `n` there exists a numerator `m` such that
`x ≠ m / n` and `|x - m / n| < C / n ^ p`.
A number is a Liouville number in the sense of `Liouville` if it is `LiouvilleWith` any real
exponent. -/
def LiouvilleWith (p x : ℝ) : Prop :=
∃ C, ∃ᶠ n : ℕ in atTop, ∃ m : ℤ, x ≠ m / n ∧ |x - m / n| < C / n ^ p
