Liouville.exists_one_le_pow_mul_dist
theorem Liouville.exists_one_le_pow_mul_dist :
∀ {Z : Type u_1} {N : Type u_2} {R : Type u_3} [inst : PseudoMetricSpace R] {d : N → ℝ} {j : Z → N → R} {f : R → R}
{α : R} {ε M : ℝ},
(∀ (a : N), 1 ≤ d a) →
0 < ε →
(∀ ⦃y : R⦄, y ∈ Metric.closedBall α ε → dist (f α) (f y) ≤ dist α y * M) →
(∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ Metric.closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))) →
∃ A, 0 < A ∧ ∀ (z : Z) (a : N), 1 ≤ d a * (dist α (j z a) * A)
This theorem, named "Liouville.exists_one_le_pow_mul_dist", is a statement about the approximation of a point in a metric space with certain cost constraints.
Given types `Z`, `N`, and `R`, where `R` is a pseudo metric space, a point `α : R`, a function `j : Z → N → R`, and a cost function `d : N → ℝ`, the theorem aims to estimate how close we can get to `α`, staying within the image of `j`, with the cost of reaching each point `j z a` being `d a`. The goal is to bound the quantity `d a * dist α (j z a)` from below by a strictly positive amount `1 / A`, implying that approximating `α` well with points in the image of `j` should come at a high cost.
The theorem requires two hypotheses about a function `f : R → R`. The first is that `f` is Lipschitz at `α`, giving a bound on the distance. The second, specific to the Liouville argument, provides the missing bound involving the cost function `d`. Given these conditions, the theorem states that there exists a strictly positive `A` such that for all `z : Z` and `a : N`, `1 ≤ d a * (dist α (j z a) * A)`.
More concisely: Given a Lipschitz function `f` at point `α` in a metric space `R` with cost function `d`, there exists a constant `A` such that for all `z` in the domain of a function `j` mapping `Z` to `N`, and `a` in the domain of `N`, `1 ≤ d(a) * dist(α, j(z)(a)) * A`.
|
Liouville.transcendental
theorem Liouville.transcendental : ∀ {x : ℝ}, Liouville x → Transcendental ℤ x
**Liouville's Theorem** states that for any real number `x`, if `x` is a Liouville number, then `x` is transcendental over the integers. In other words, any Liouville number (a real number `x` that for every natural number `n`, there exist integers `a` and `b` with `1 < b` such that `0 < |x - a/b| < 1/bⁿ`) is not algebraic over the integers, i.e., it is not a root of any non-zero polynomial equation with integer coefficients.
More concisely: A real number `x` is Liouville number if and only if it is transcendental over the integers.
|