LiouvilleWith.add_rat_iff
theorem LiouvilleWith.add_rat_iff : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p (x + ↑r) ↔ LiouvilleWith p x
The theorem `LiouvilleWith.add_rat_iff` states that for any real numbers `p` and `x`, and any rational number `r`, `x` is a Liouville number with exponent `p` if and only if `x + r` is a Liouville number with exponent `p`. In other words, adding a rational number to a Liouville number gives another Liouville number with the same exponent.
More concisely: For any real numbers `x` being a Liouville number with exponent `p` if and only if `x + r` is a Liouville number with exponent `p`, where `r` is a rational number.
|
LiouvilleWith.rat_mul_iff
theorem LiouvilleWith.rat_mul_iff : ∀ {p x : ℝ} {r : ℚ}, r ≠ 0 → (LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x) := by
sorry
The theorem `LiouvilleWith.rat_mul_iff` states that for any real number `x` and rational number `r` with `r ≠ 0`, the product `r * x` is a Liouville number with exponent `p` if and only if `x` is also a Liouville number with exponent `p`. In other words, multiplying a Liouville number by a non-zero rational number doesn't change its status as a Liouville number with the same exponent.
More concisely: For any real number `x` and non-zero rational number `r`, `x` and `r * x` have the same Liouville exponent if and only if both are Liouville numbers with that exponent.
|
Mathlib.NumberTheory.Liouville.LiouvilleWith._auxLemma.11
theorem Mathlib.NumberTheory.Liouville.LiouvilleWith._auxLemma.11 :
∀ {p x : ℝ}, LiouvilleWith p (-x) = LiouvilleWith p x
The theorem `Mathlib.NumberTheory.Liouville.LiouvilleWith._auxLemma.11` states that for any real numbers `p` and `x`, a real number `-x` is a Liouville number with exponent `p` if and only if `x` is a Liouville number with exponent `p`. In other words, the property of being a Liouville number with a given exponent is invariant under negation of the number.
More concisely: The theorem `Mathlib.NumberTheory.Liouville.LiouvilleWith._auxLemma.11` asserts that negating a Liouville number with exponent `p` results in another Liouville number with the same exponent.
|
LiouvilleWith.mul_rat_iff
theorem LiouvilleWith.mul_rat_iff : ∀ {p x : ℝ} {r : ℚ}, r ≠ 0 → (LiouvilleWith p (x * ↑r) ↔ LiouvilleWith p x) := by
sorry
The theorem `LiouvilleWith.mul_rat_iff` states that for any real numbers `p` and `x`, and any rational number `r` not equal to zero, the product `x * r` is a Liouville number with exponent `p` if and only if `x` itself is a Liouville number with the same exponent `p`. A Liouville number with exponent `p` is defined as a real number `x` for which there exists a real number `C` such that for infinitely many natural numbers `n` (acting as denominators), there exists an integer `m` (acting as numerator) such that `x` is not equal to `m/n` and the absolute value of the difference between `x` and `m/n` is less than `C / n^p`.
More concisely: For real numbers `x` and `p`, `x` is a Liouville number with exponent `p` if and only if `x * r` is a Liouville number with exponent `p` for any non-zero rational number `r`.
|
LiouvilleWith.exists_pos
theorem LiouvilleWith.exists_pos :
∀ {p x : ℝ},
LiouvilleWith p x →
∃ C, ∃ (_ : 0 < C), ∃ᶠ (n : ℕ) in Filter.atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
This theorem states that for any real numbers 'p' and 'x', if 'x' is a Liouville number with exponent 'p' (according to the definition of `LiouvilleWith`), then there exists a positive constant 'C' such that, for infinitely many natural numbers 'n' tending to infinity (with 'n' being greater than or equal to 1), there exists an integer 'm' such that 'x' is not equal to 'm/n' and the absolute difference between 'x' and 'm/n' is less than 'C' divided by 'n' raised to the power 'p'. This theorem also mentions that while this statement is equivalent to the original definition of a Liouville number, the case when 'n' is zero is excluded as it breaks many arguments.
More concisely: For any real number 'x' being a Liouville number with exponent 'p' according to `LiouvilleWith` in Lean 4, there exists a constant 'C' such that for infinitely many natural numbers 'n' (greater than or equal to 1), there exists an integer 'm' satisfying 'x' ≠ 'm/n' and |x - m/n| < C/n^p.
|
LiouvilleWith.frequently_lt_rpow_neg
theorem LiouvilleWith.frequently_lt_rpow_neg :
∀ {p q x : ℝ},
LiouvilleWith p x → q < p → ∃ᶠ (n : ℕ) in Filter.atTop, ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < ↑n ^ (-q)
The theorem `LiouvilleWith.frequently_lt_rpow_neg` states that for any real numbers `p`, `q`, and `x`, if `x` satisfies the Liouville condition with exponent `p` (i.e., it is a Liouville number with exponent `p`) and `q` is less than `p`, then `x` also satisfies the Liouville condition with exponent `q` and a specific constant `1`. In other words, if a real number `x` is a Liouville number with an exponent `p` and we have another real number `q` which is less than `p`, then `x` is also a Liouville number with this lower exponent `q` and the constant `1`. Here, `Filter.atTop` implies that this statement is true for infinitely many natural numbers `n`, and there exists a corresponding integer `m` for each of these `n` such that `x` is not equal to `m / n` and the absolute difference between `x` and `m / n` is less than `1 / n` raised to the power of `q`.
More concisely: If a real number `x` is a Liouville number with exponent `p`, then it is also a Liouville number with exponent `q` for any `q` less than `p`.
|
LiouvilleWith.mul_rat
theorem LiouvilleWith.mul_rat : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p x → r ≠ 0 → LiouvilleWith p (x * ↑r)
The theorem `LiouvilleWith.mul_rat` states that for any real number `p` and `x`, and any nonzero rational number `r`, if `x` is a Liouville number with exponent `p` (meaning there exists a real number `C` such that for infinitely many natural numbers `n`, there exists an integer `m` for which `x` is not equal to `m/n` and the absolute difference between `x` and `m/n` is less than `C/n^p`), then the product of `x` and `r` is also a Liouville number with the same exponent `p`.
More concisely: If `x` is a Liouville number with exponent `p` and `r` is a nonzero rational number, then the product `x * r` is also a Liouville number with exponent `p`.
|
forall_liouvilleWith_iff
theorem forall_liouvilleWith_iff : ∀ {x : ℝ}, (∀ (p : ℝ), LiouvilleWith p x) ↔ Liouville x
This theorem says that a real number `x` satisfies the Liouville condition with any real exponent if and only if it is a Liouville number. In other words, there exists some real number `C` and infinitely many denominators `n`, with a corresponding numerator `m`, such that `x ≠ m / n` and `|x - m / n| < C / n^p` for all real `p`, if and only if for every natural number `n`, there exist integers `a` and `b` with `1 < b` such that `x ≠ a/b` and `|x - a/b| < 1/b^n`.
More concisely: A real number `x` is a Liouville number if and only if there exist infinitely many rational numbers `a/b` with `b > 0` such that `x neq a/b` and `|x - a/b| < 1/b^n` for all natural numbers `n`. Alternatively, `x` satisfies the Liouville condition with any real exponent if and only if there exist `C` and infinitely many rational denominators `n` and numerators `m` such that `x neq m/n` and `|x - m/n| < C/n^p` for all real `p`.
|
liouvilleWith_one
theorem liouvilleWith_one : ∀ (x : ℝ), LiouvilleWith 1 x
This theorem states that for any real number `x`, the property of being a Liouville number with exponent `p = 1` holds. This means that there exists a real number `C` such that for infinitely many natural numbers `n`, there exists an integer `m` for which `x` is not equal to `m/n` and the absolute value of the difference between `x` and `m/n` is less than `C/n`. Since this condition is satisfied for `p = 1`, it is also satisfied for any `p` less than or equal to `1`.
More concisely: Every real number is a Liouville number with exponent 1.
|
Liouville.liouvilleWith
theorem Liouville.liouvilleWith : ∀ {x : ℝ}, Liouville x → ∀ (p : ℝ), LiouvilleWith p x
The theorem states that if a real number 'x' is a Liouville number, then 'x' is also a Liouville number with any real exponent 'p'. In other words, for any Liouville number 'x', for any real number 'p', there is a real number 'C' such that for infinitely many natural numbers 'n', there exists an integer 'm' such that 'x' is not equal to 'm/n' and the absolute difference between 'x' and 'm/n' is less than 'C' divided by 'n' to the power 'p'.
More concisely: If a real number is a Liouville number, then it is a Liouville number with exponent 'p' for any real number 'p'. That is, for any Liouville number 'x' and real 'p', there exists a constant 'C' such that for infinitely many natural numbers 'n', there exists an integer 'm' with 'x' not equal to 'm/n' and the difference '|x - m/n|' being less than 'C' divided by 'n' raised to the power 'p'.
|
LiouvilleWith.mono
theorem LiouvilleWith.mono : ∀ {p q x : ℝ}, LiouvilleWith p x → q ≤ p → LiouvilleWith q x
The theorem `LiouvilleWith.mono` states that if a real number `x` is a Liouville number with exponent `p`, then `x` is also a Liouville number with any other exponent `q` that is less than or equal to `p`. In mathematical terms, if there exists a real number `C` such that for infinitely many denominators `n` there is a numerator `m` such that `x ≠ m / n` and the absolute value of `x - m / n` is less than `C / n^p`, then for any `q` less than or equal to `p`, there exists a `C'` such that the absolute value of `x - m / n` is less than `C' / n^q` for infinitely many `n`.
More concisely: If a real number `x` is a Liouville number with exponent `p`, then it is also a Liouville number with exponent `q` for any `q ≤ p`.
|
LiouvilleWith.irrational
theorem LiouvilleWith.irrational : ∀ {p x : ℝ}, LiouvilleWith p x → 1 < p → Irrational x
The theorem states that any real number `x` satisfying the Liouville condition with an exponent `p` greater than 1 is an irrational number. The Liouville condition is met if there exists a real number `C` such that for infinitely many natural numbers `n`, there exists an integer `m` satisfying two conditions: `x` is not equal to `m / n`, and the absolute difference between `x` and `m / n` is less than `C / n ^ p`. An irrational number is a real number that is not a rational number. Therefore, the theorem proves that numbers meeting these conditions cannot be expressed as a ratio of two integers.
More concisely: A real number `x` satisfying the Liouville condition with exponent `p > 1` is an irrational number.
|
LiouvilleWith.sub_rat_iff
theorem LiouvilleWith.sub_rat_iff : ∀ {p x : ℝ} {r : ℚ}, LiouvilleWith p (x - ↑r) ↔ LiouvilleWith p x
This theorem states that for any real numbers `p` and `x`, and any rational number `r`, the number `x` is a Liouville number with exponent `p`, if and only if the number `x - r` is a Liouville number with the same exponent `p`. In other words, subtracting a rational number from a Liouville number results in another Liouville number with the same exponent.
More concisely: If `x` is a Liouville number with exponent `p`, then so is `x - r` for any rational number `r` (i.e., Liouville numbers are closed under subtraction of rational numbers with the same exponent).
|
Liouville.frequently_exists_num
theorem Liouville.frequently_exists_num :
∀ {x : ℝ}, Liouville x → ∀ (n : ℕ), ∃ᶠ (b : ℕ) in Filter.atTop, ∃ a, x ≠ ↑a / ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ n := by
sorry
The theorem `Liouville.frequently_exists_num` asserts that if `x` is a Liouville number, then for any natural number `n`, there are infinitely many natural number denominators `b` for which there exists an integer numerator `a` such that `x` is not equal to `a / b` and the absolute value of the difference between `x` and `a / b` is less than `1 / b^n`. Here, the phrase "infinitely many" is mathematically represented by `Filter.atTop`, which denotes a condition that holds true for sufficiently large values.
More concisely: If `x` is a Liouville number, then for each natural number `n`, there exist infinitely many natural number denominators `b` and an integer numerator `a` such that `|x - a/b| < 1/b^n`.
|