The linear-form exponent and Mahler's exponent

For θ : ι → ℝ with ι finite, the linear-form exponent linearFormExponent θ is the supremum of the real exponents w for which infinitely many integer vectors x = (x₀, (xᵢ)ᵢ) satisfy 0 < |x₀ + ∑ i, xᵢ θᵢ| ≤ ‖x‖ ^ (-w), where ‖x‖ is the sup norm over all coordinates of x, including x₀. The supremum is taken in ℝ≥0∞, so negative exponents contribute 0. Mahler's exponent mahlerExponent n ξ is the linear-form exponent of (ξ, ξ ^ 2, …, ξ ^ n), so it measures how small nonzero values of integer polynomials of degree at most n can be at ξ.

Main results

• linearFormApproximations_antitone: the solution sets shrink as the exponent grows.
• ofReal_le_linearFormExponent_of_forall_lt: if every exponent below w has infinitely many solutions, then w ≤ w(θ).
• linearFormExponent_comp_le: forgetting coordinates along an injective reindexing can only decrease the exponent; in particular Mahler's exponent is monotone in the degree (mahlerExponent_mono).
• linearFormExponent_le_of_map: an integer change of variables that multiplies the linear form by a fixed nonzero factor and grows sup norms at most linearly can only increase the exponent.
• linearFormExponent_of_isEmpty: the empty vector has exponent 0.
• linearFormExponent_one_add: for every real ξ, w(ξ) + 1 = μ(ξ), where μ is the irrationality exponent. Consequently rational numbers have exponent 0 (linearFormExponent_ratCast) and exactly the Liouville numbers have exponent ⊤ (linearFormExponent_eq_top_iff).
• card_le_linearFormExponent: Dirichlet's lower bound w(θ) ≥ n when 1, θ₁, …, θₙ satisfy no nontrivial integer relation; consequently w_n(ξ) ≥ n when ξ is not algebraic of degree at most n (natCast_le_mahlerExponent).
• coeffVec and linearFormPoly: the correspondence between integer polynomials of degree at most n and integer vectors x = (x₀, (xⱼ)ⱼ), under which P(ξ) is the linear form of x at ξ, ξ ^ 2, …, ξ ^ n.

References

• Y. Bugeaud, Exponents of Diophantine approximation, §1, Definition 1.2 and §2, Definition 2.1 and Theorem 2.5.

def TauCeti.linearFormApproximations {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) (w : ℝ) : Set (ℤ × (ι → ℤ))

The integer vectors x = (x₀, (xᵢ)ᵢ) with 0 < |x₀ + ∑ i, xᵢ θᵢ| ≤ ‖x‖ ^ (-w); here ‖x‖ is the sup norm over all coordinates of x, including x₀.

@[simp]

theorem TauCeti.mem_linearFormApproximations {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} {w : ℝ} {x : ℤ × (ι → ℤ)} : x ∈ linearFormApproximations θ w ↔ 0 < |↑x.1 + ∑ i : ι, ↑(x.2 i) * θ i| ∧ |↑x.1 + ∑ i : ι, ↑(x.2 i) * θ i| ≤ ‖x‖ ^ (-w)

Membership in linearFormApproximations θ w unfolds to the two defining inequalities.

theorem TauCeti.linearFormApproximations_antitone {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) : Antitone (linearFormApproximations θ)

The solution sets shrink as the exponent grows.

theorem TauCeti.norm_le_max_of_abs_add_sum_mul_le {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} {δ N : ℝ} {x : ℤ × (ι → ℤ)} (hL : |↑x.1 + ∑ i : ι, ↑(x.2 i) * θ i| ≤ δ) (hN : ‖x.2‖ ≤ N) : ‖x‖ ≤ max (δ + N * ∑ i : ι, |θ i|) N

If the linear form x₀ + ∑ i, xᵢ θᵢ of an integer vector x has absolute value at most δ and ‖(xᵢ)ᵢ‖ ≤ N, then the sup norm of the full vector satisfies ‖x‖ ≤ max (δ + N ∑ i, |θᵢ|) N.

noncomputable def TauCeti.linearFormExponent {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) : ENNReal

The linear-form exponent w(θ) of θ : ι → ℝ is the supremum, in ℝ≥0∞, of the real exponents w for which infinitely many integer vectors x = (x₀, (xᵢ)ᵢ) satisfy 0 < |x₀ + ∑ i, xᵢ θᵢ| ≤ ‖x‖ ^ (-w). Negative exponents contribute 0.

theorem TauCeti.linearFormExponent_def {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) : linearFormExponent θ = ⨆ (w : ℝ), ⨆ (_ : (linearFormApproximations θ w).Infinite), ENNReal.ofReal w

The linear-form exponent is the supremum of ENNReal.ofReal w over the exponents w with infinitely many solutions.

theorem TauCeti.le_linearFormExponent_of_infinite {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} {w : ℝ} (h : (linearFormApproximations θ w).Infinite) : ENNReal.ofReal w ≤ linearFormExponent θ

An exponent with infinitely many solutions is at most the linear-form exponent.

theorem TauCeti.linearFormExponent_le_iff {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} {a : ENNReal} : linearFormExponent θ ≤ a ↔ ∀ (w : ℝ), (linearFormApproximations θ w).Infinite → ENNReal.ofReal w ≤ a

The linear-form exponent is bounded by a exactly when every exponent with infinitely many solutions maps below a.

theorem TauCeti.infinite_linearFormApproximations_of_lt {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} {w : ℝ} (h : ENNReal.ofReal w < linearFormExponent θ) : (linearFormApproximations θ w).Infinite

A real exponent strictly below the linear-form exponent has infinitely many solutions.

theorem TauCeti.ofReal_le_linearFormExponent_of_forall_lt {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} {w : ℝ} (h : ∀ w' < w, (linearFormApproximations θ w').Infinite) : ENNReal.ofReal w ≤ linearFormExponent θ

If every exponent below w has infinitely many solutions, then w is at most the linear-form exponent.

theorem TauCeti.linearFormExponent_le_of_map {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {θ : ι → ℝ} {θ' : κ → ℝ} (f : ℤ × (ι → ℤ) → ℤ × (κ → ℤ)) {r A : ℝ} (hr : r ≠ 0) (hf : ∀ (x : ℤ × (ι → ℤ)), ↑(f x).1 + ∑ k : κ, ↑((f x).2 k) * θ' k = r * (↑x.1 + ∑ i : ι, ↑(x.2 i) * θ i)) (hA : ∀ (x : ℤ × (ι → ℤ)), ‖f x‖ ≤ A * ‖x‖) : linearFormExponent θ ≤ linearFormExponent θ'

Transfer of the linear-form exponent. Let f send integer vectors for θ to integer vectors for θ', multiplying the linear form by a fixed nonzero factor r and growing the sup norm at most linearly. Then w(θ) ≤ w(θ').

theorem TauCeti.linearFormExponent_comp_le {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (θ : κ → ℝ) {f : ι → κ} (hf : Function.Injective f) : linearFormExponent (θ ∘ f) ≤ linearFormExponent θ

Restricting θ along an injective reindexing can only decrease the linear-form exponent: a solution for θ ∘ f extends by zero to a solution for θ with the same linear form and the same norm.

@[simp]

theorem TauCeti.linearFormExponent_of_isEmpty {ι : Type u_1} [Fintype ι] [IsEmpty ι] (θ : ι → ℝ) : linearFormExponent θ = 0

The empty vector has linear-form exponent 0: the linear form is then the integer x₀, which is at most |x₀| ^ (-w) in absolute value only for x₀ = ± 1 when 0 < w.

Comparison with the irrationality exponent

theorem TauCeti.linearFormExponent_one_add (ξ : ℝ) : linearFormExponent ![ξ] + 1 = irrationalityExponent ξ

The linear-form exponent of a single real number ξ is its irrationality exponent minus one: w(ξ) + 1 = μ(ξ). Both sides equal 1 for rational ξ.

@[simp]

theorem TauCeti.linearFormExponent_ratCast (q : ℚ) : linearFormExponent ![↑q] = 0

A rational number has linear-form exponent 0.

theorem TauCeti.linearFormExponent_eq_top_iff (ξ : ℝ) : linearFormExponent ![ξ] = ⊤ ↔ Liouville ξ

A real number has infinite linear-form exponent exactly when it is a Liouville number.

Dirichlet's lower bound

theorem TauCeti.infinite_linearFormApproximations_of_lt_card {ι : Type u_1} [Fintype ι] [Nonempty ι] {θ : ι → ℝ} (hθ : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i : ι, ↑(x.2 i) * θ i = 0 → x = 0) {w : ℝ} (hw : w < ↑(Fintype.card ι)) : (linearFormApproximations θ w).Infinite

Dirichlet's theorem for one linear form, infinitely many solutions. If 1 and the n ≥ 1 real numbers θᵢ satisfy no nontrivial integer relation, then every exponent w < n has infinitely many solutions 0 < |x₀ + ∑ i, xᵢ θᵢ| ≤ ‖x‖ ^ (-w), with the sup norm taken over all coordinates of x.

theorem TauCeti.card_le_linearFormExponent {ι : Type u_1} [Fintype ι] {θ : ι → ℝ} (hθ : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i : ι, ↑(x.2 i) * θ i = 0 → x = 0) : ↑(Fintype.card ι) ≤ linearFormExponent θ

Dirichlet's lower bound for the linear-form exponent. If 1 and the n real numbers θᵢ satisfy no nontrivial integer relation, that is, if they are linearly independent over ℚ, then the linear-form exponent of θ is at least n.

Mahler's exponent

noncomputable def TauCeti.mahlerExponent (n : ℕ) (ξ : ℝ) : ENNReal

Mahler's exponent w_n(ξ) is the linear-form exponent of (ξ, ξ ^ 2, …, ξ ^ n): the supremum of the w for which infinitely many integer polynomials P of degree at most n satisfy 0 < |P(ξ)| ≤ H(P) ^ (-w), where H(P) is the largest absolute value of a coefficient of P.

theorem TauCeti.mahlerExponent_def (n : ℕ) (ξ : ℝ) : mahlerExponent n ξ = linearFormExponent fun (j : Fin n) => ξ ^ (↑j + 1)

Mahler's exponent unfolds to the linear-form exponent of the powers ξ, ξ ^ 2, …, ξ ^ n.

def TauCeti.coeffVec (n : ℕ) (P : Polynomial ℤ) : ℤ × (Fin n → ℤ)

The coefficients of P in degrees 0, 1, …, n, split into the constant term and the coefficients of X, X ^ 2, …, X ^ n. For P of degree at most n, the linear form of this vector at ξ, ξ ^ 2, …, ξ ^ n is P(ξ).

noncomputable def TauCeti.linearFormPoly {n : ℕ} (x : ℤ × (Fin n → ℤ)) : Polynomial ℤ

The integer polynomial x₀ + ∑ j, xⱼ X ^ (j + 1) of degree at most n, a right inverse of coeffVec n. Its value at ξ is the linear form of x at ξ, ξ ^ 2, …, ξ ^ n.

@[simp]

theorem TauCeti.coeffVec_fst (n : ℕ) (P : Polynomial ℤ) : (coeffVec n P).1 = P.coeff 0

The first component of coeffVec n P is the constant coefficient of P.

@[simp]

theorem TauCeti.coeffVec_snd (n : ℕ) (P : Polynomial ℤ) (j : Fin n) : (coeffVec n P).2 j = P.coeff (↑j + 1)

The j-th entry of the second component of coeffVec n P is the coefficient of X ^ (j + 1) in P.

theorem TauCeti.coeffVec_linearForm {A : Type u_3} [CommRing A] {n : ℕ} {P : Polynomial ℤ} (hP : P.natDegree ≤ n) (z : A) : ↑(coeffVec n P).1 + ∑ j : Fin n, ↑((coeffVec n P).2 j) * z ^ (↑j + 1) = (Polynomial.aeval z) P

For P of degree at most n, the linear form of coeffVec n P at the powers of z is P(z).

theorem TauCeti.norm_coeffVec_le (n : ℕ) (P : Polynomial ℤ) : ‖coeffVec n P‖ ≤ P.supNorm

The sup norm of coeffVec n P is at most the coefficient sup norm of P.

theorem TauCeti.coeffVec_injOn (n : ℕ) : Set.InjOn (coeffVec n) {P : Polynomial ℤ | P.natDegree ≤ n}

Polynomials of degree at most n are determined by coeffVec n.

theorem TauCeti.natDegree_linearFormPoly_le {n : ℕ} (x : ℤ × (Fin n → ℤ)) : (linearFormPoly x).natDegree ≤ n

The polynomial linearFormPoly x has degree at most n.

@[simp]

theorem TauCeti.coeffVec_linearFormPoly {n : ℕ} (x : ℤ × (Fin n → ℤ)) : coeffVec n (linearFormPoly x) = x

coeffVec n recovers x from linearFormPoly x.

theorem TauCeti.linearFormPoly_coeffVec {n : ℕ} {P : Polynomial ℤ} (hP : P.natDegree ≤ n) : linearFormPoly (coeffVec n P) = P

On polynomials of degree at most n, linearFormPoly inverts coeffVec n.

@[simp]

theorem TauCeti.coeff_linearFormPoly_zero {n : ℕ} (x : ℤ × (Fin n → ℤ)) : (linearFormPoly x).coeff 0 = x.1

The constant coefficient of linearFormPoly x is x₀.

@[simp]

theorem TauCeti.coeff_linearFormPoly_succ {n : ℕ} (x : ℤ × (Fin n → ℤ)) (j : Fin n) : (linearFormPoly x).coeff (↑j + 1) = x.2 j

The coefficient of X ^ (j + 1) in linearFormPoly x is xⱼ.

theorem TauCeti.aeval_linearFormPoly {A : Type u_3} [CommRing A] {n : ℕ} (x : ℤ × (Fin n → ℤ)) (z : A) : (Polynomial.aeval z) (linearFormPoly x) = ↑x.1 + ∑ j : Fin n, ↑(x.2 j) * z ^ (↑j + 1)

The value of linearFormPoly x at z is the linear form of x at the powers of z.

theorem TauCeti.supNorm_linearFormPoly_le {n : ℕ} (x : ℤ × (Fin n → ℤ)) : (linearFormPoly x).supNorm ≤ ‖x‖

The coefficient sup norm of linearFormPoly x is at most the sup norm of x.

theorem TauCeti.mahlerExponent_mono (ξ : ℝ) : Monotone fun (x : ℕ) => mahlerExponent x ξ

Mahler's exponent is monotone in the degree.

@[simp]

theorem TauCeti.mahlerExponent_zero (ξ : ℝ) : mahlerExponent 0 ξ = 0

Constant integer polynomials give Mahler's exponent 0 in degree zero.

theorem TauCeti.mahlerExponent_one_add_one (ξ : ℝ) : mahlerExponent 1 ξ + 1 = irrationalityExponent ξ

Mahler's exponent in degree one is the irrationality exponent minus one.

theorem TauCeti.natCast_le_mahlerExponent {n : ℕ} {ξ : ℝ} (hξ : ¬(IsAlgebraic ℚ ξ ∧ (minpoly ℚ ξ).natDegree ≤ n)) : ↑n ≤ mahlerExponent n ξ

Dirichlet's lower bound for Mahler's exponent. If ξ is not algebraic of degree at most n, then w_n(ξ) ≥ n.