Schneider's auxiliary function #
Let K ⊂ ℂ be a number field of degree d, given by an embedding σ : K →+* ℂ, let λ ∈ ℂ and
let α, β, γ ∈ K with σ α = exp λ and σ γ = exp (σ β λ). In Schneider's proof of the
Gelfond–Schneider theorem the auxiliary function is the exponential polynomial
F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j λ z),
whose integer coefficients are chosen so that F vanishes at the points u + v σ β of the grid
1 ≤ u, v ≤ L. Since exp (j λ (u + v σ β)) = σ (α ^ (u j) γ ^ (v j))
(RingHom.map_pow_mul_pow_eq_exp), the value F(u + v σ β) is the image under σ of
y_{uv} = ∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) ∈ K,
so the vanishing conditions are L² linear equations over K in the D₁ D₂ integer unknowns
a_{ij}. When D₁ D₂ ≥ 2 d L², Siegel's lemma with rational integer unknowns
(NumberField.exists_ne_zero_int_vec_abs_le_of_house_le) solves them with
|a_{ij}| ≤ exp (c (D₁ log L + D₂ L)), where c depends only on K, α, β and γ. To apply
it, each equation is multiplied by m ^ (D₁ + 2 L D₂) for a nonzero integer m such that
m α, m β and m γ are algebraic integers.
Schneider's proof then evaluates F on the larger grid u, v ≤ c L. The values y_{uv} there
have house exp (O (D₁ log L + D₂ L)), which is exp (O (L ^ (3 / 2) log L)) for Schneider's
parameters L = 2 d M², D₁ = (2 d)² M³, D₂ = 2 d M, and m ^ (D₁ + 2 c L D₂) y_{uv} is an
algebraic integer, where m ^ (D₁ + 2 c L D₂) ≤ exp (O (L ^ (3 / 2))). These are the arithmetic
inputs to Liouville's lower bound for a nonzero σ y_{uv}. The analytic upper bound for
|F(u + v σ β)|, from the zero estimate for exponential polynomials and Schwarz's lemma with
prescribed zeros, is not part of this file.
Main results #
TauCeti.exists_schneider_auxiliary_algebraic: a nonzero integer coefficient matrix with the bound above for which everyy_{uv},1 ≤ u, v ≤ L, vanishes inK.TauCeti.exists_intCast_pow_mul_schneider_term: a common denominatormand house bounds for the terms(u + v β) ^ k α ^ (u j) γ ^ (v j)of the valuesy_{uv}(and of Gelfond'sy_k(t)).RingHom.map_pow_mul_pow_eq_exp:σ (α ^ (u j) γ ^ (v j)) = exp (j λ (u + v σ β)).RingHom.map_schneider_value:σ y_{uv} = F(u + v σ β).RingHom.exists_schneider_auxiliary: the auxiliary functionFvanishes at the grid pointsu + v σ β,1 ≤ u, v ≤ L.TauCeti.house_schneider_value_le: an explicit bound for the house ofy_{uv},u, v ≤ B.TauCeti.isIntegral_intCast_pow_mul_schneider_value:m ^ (D₁ + 2 B D₂) y_{uv}is an algebraic integer foru, v ≤ Bwhenm α,m βandm γare.TauCeti.exists_house_schneider_value_le_exp: on the gridu, v ≤ c L, the house ofy_{uv}is at mostexp (C (D₁ log L + D₂ L)).TauCeti.exists_house_schneider_value_le_exp_rpow,TauCeti.exists_abs_pow_schneider_exponent_le_exp_rpow: for Schneider's parameters, the house ofy_{uv}is at mostexp (c₅ L ^ (3 / 2) log L)and the denominatorm ^ (D₁ + 2 c L D₂)is at mostexp (c₆ L ^ (3 / 2)).
References #
- J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 4, §4.4, Lemmas 4.22 and 4.27.
One term of Schneider's value y_{uv}, multiplied by m ^ N with i + u j + v j ≤ N, is an
algebraic integer when m α, m β and m γ are.
Denominators of Schneider's values. If m α, m β and m γ are algebraic integers,
then for u, v ≤ B the multiple
m ^ (D₁ + 2 B D₂) ∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) is an algebraic integer for
all integers a_{ij}, i < D₁, j < D₂.
The house bound for an entry of Schneider's linear system: if x, z, w have house at
most H and y has house at most L H, then for i ≤ D and i + s + t ≤ n the entry
x ^ (n - (i + s + t)) y ^ i z ^ s w ^ t has house at most L ^ D H ^ n.
A common denominator for the terms of Schneider's and Gelfond's values: there are a nonzero
integer c₀ and H ≥ 1 with |c₀| ≤ H such that for u, v ≤ B (B ≥ 1) and
k + u j + v j ≤ N the multiple c₀ ^ N ((u + v β) ^ k α ^ (u j) γ ^ (v j)) is an algebraic
integer of house at most B ^ k H ^ N.
Schneider's auxiliary function, algebraic form (Evertse, Lemma 4.22). Let K be a number
field of degree d and α, β, γ ∈ K. There is c > 0 such that for all integers L ≥ 3 and
D₁, D₂ with D₁ D₂ ≥ 2 d L² there are integers a_{ij}, i < D₁, j < D₂, not all zero,
with |a_{ij}| ≤ exp (c (D₁ log L + D₂ L)), such that
∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) = 0 for all 1 ≤ u, v ≤ L.
Size and denominators of the values y_{uv} #
Schneider's proof evaluates F at the points u + v σ β of a grid larger than the one on which
it was made to vanish. The value there is the image under σ of
y_{uv} = ∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) ∈ K, and the final contradiction
plays an upper bound for |σ y_{uv}| against Liouville's lower bound, which needs the house and
a denominator of y_{uv}.
The house of Schneider's values. If α, β, γ have house at most H ≥ 1 and the
integers a_{ij}, i < D₁, j < D₂, have absolute value at most A, then for u, v ≤ B with
B ≥ 1 the house of ∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) is at most
D₁ D₂ A (2 B) ^ D₁ H ^ (D₁ + 2 B D₂).
Schneider's values on an extended grid. Let α, β, γ ∈ K, c₁ ∈ ℝ and c ∈ ℕ. There
is C ≥ 0 such that for all integers L ≥ 2, D₁ and D₂, all integers a_{ij}, i < D₁,
j < D₂, with |a_{ij}| ≤ exp (c₁ (D₁ log L + D₂ L)), and all u, v ≤ c L, the house of
∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) is at most exp (C (D₁ log L + D₂ L)).
The house of Schneider's values (Evertse, Lemma 4.27(ii)). Let K be a number field of
degree d, let α, β, γ ∈ K, c₁ ∈ ℝ and c ∈ ℕ. There is c₅ such that, for every integer
M ≥ 1 with L = 2 d M², D₁ = (2 d)² M³ and D₂ = 2 d M, all integers a_{ij}, i < D₁,
j < D₂, with |a_{ij}| ≤ exp (c₁ (D₁ log L + D₂ L)) (the bound of
exists_schneider_auxiliary_algebraic) and all u, v ≤ c L, the value
y_{uv} = ∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) has house at most
exp (c₅ L ^ (3 / 2) log L). In particular ‖σ y_{uv}‖ satisfies the same bound for every
embedding σ : K →+* ℂ (NumberField.norm_embedding_le_house). Evertse takes
c = 1 + ⌊√(2 d)⌋.
The size of the denominator of Schneider's values (Evertse, Lemma 4.27). For
d, c ∈ ℕ and m ∈ ℝ there is c₆ such that, for L = 2 d M², D₁ = (2 d)² M³ and
D₂ = 2 d M, the denominator m ^ (D₁ + 2 c L D₂) of the values y_{uv}, u, v ≤ c L
(isIntegral_intCast_pow_mul_schneider_value), satisfies
|m| ^ (D₁ + 2 c L D₂) ≤ exp (c₆ L ^ (3 / 2)).
If σ α = exp λ and σ γ = exp (σ β λ), then
σ (α ^ (u j) γ ^ (v j)) = exp (j λ (u + v σ β)): the value of the exponential exp (j λ z) at
z = u + v σ β lies in the image of σ.
If σ α = exp λ and σ γ = exp (σ β λ), then σ maps Schneider's value
y_{uv} = ∑_{i, j} a_{ij} (u + v β) ^ i α ^ (u j) γ ^ (v j) to the value
F(u + v σ β) = ∑_{i, j} a_{ij} (u + v σ β) ^ i exp (j λ (u + v σ β)) of the auxiliary
function.
Schneider's auxiliary function (Evertse, Lemma 4.22). Let K be a number field of degree
d with an embedding σ : K →+* ℂ, let λ ∈ ℂ and α, β, γ ∈ K with σ α = exp λ and
σ γ = exp (σ β λ). There is c > 0 such that for all integers L ≥ 3 and D₁, D₂ with
D₁ D₂ ≥ 2 d L² there are integers a_{ij}, i < D₁, j < D₂, not all zero, with
|a_{ij}| ≤ exp (c (D₁ log L + D₂ L)), such that
F(z) = ∑_{i, j} a_{ij} z ^ i exp (j λ z) vanishes at z = u + v σ β for all 1 ≤ u, v ≤ L.