The analytic bound for Schneider's auxiliary function

Let β ∈ ℂ be irrational, λ ∈ ℂ, and let

F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j λ z)

be an exponential polynomial with complex coefficients that vanishes at the L² distinct points u + v β of the grid 1 ≤ u, v ≤ L. This is Schneider's auxiliary function from the proof of the Gelfond–Schneider theorem, whose coefficients are produced by Siegel's lemma in RingHom.exists_schneider_auxiliary. This file shows that F is very small on the larger grid 0 ≤ u, v ≤ c L: the extrapolation estimate of Evertse's Lemma 4.27.

The proof applies Schwarz's lemma with prescribed zeros (TauCeti.norm_le_mul_three_mul_div_pow) on discs of radii R and T = 3 e R, where R bounds the moduli of all the grid points. On the circle of radius T the function F is trivially bounded by D₁ D₂ A T ^ D₁ exp (D₂ |λ| T), where A bounds the coefficients, and the L² zeros contribute the factor exp (-L²).

In the proof of the Gelfond–Schneider theorem the values F(u + v β) are the images of algebraic numbers whose houses and denominators are bounded by exp (O(L^{3/2} log L)). The factor exp (-L²) here then forces those algebraic numbers to vanish, by Liouville's inequality.

Main results

• TauCeti.norm_schneider_auxiliary_le: the bound ‖F z‖ ≤ D₁ D₂ A T ^ D₁ exp (D₂ ‖λ‖ T) (3 R / T) ^ (L ^ 2) for ‖z‖ ≤ R.
• TauCeti.exists_norm_schneider_auxiliary_le_exp: if |a_{ij}| ≤ exp (c₁ (D₁ log L + D₂ L)), then |F(u + v β)| ≤ exp (C (D₁ log L + D₂ L) - L ^ 2) for 0 ≤ u, v ≤ c L.
• TauCeti.exists_norm_schneider_auxiliary_le_exp_rpow: for Schneider's parameters L = 2 d M², D₁ = (2 d)² M³, D₂ = 2 d M, the bound |F(u + v β)| ≤ exp (c₄ L ^ (3 / 2) log L - L ^ 2) of Lemma 4.27.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 4, §4.4, Lemmas 4.26 and 4.27.

theorem TauCeti.norm_schneider_auxiliary_le {β : ℂ} (hβ : ∀ (q : ℚ), ↑q ≠ β) {l : ℂ} {L D₁ D₂ : ℕ} {a : Fin D₁ → Fin D₂ → ℂ} {A R T : ℝ} (ha : ∀ (i : Fin D₁) (j : Fin D₂), ‖a i j‖ ≤ A) (hzero : ∀ (u v : ℕ), 1 ≤ u → u ≤ L → 1 ≤ v → v ≤ L → ∑ i : Fin D₁, ∑ j : Fin D₂, a i j * (↑u + ↑v * β) ^ ↑i * Complex.exp (↑↑j * l * (↑u + ↑v * β)) = 0) (hR : ↑L * (1 + ‖β‖) ≤ R) (hRT : 3 * R ≤ T) (hT : 1 ≤ T) {z : ℂ} (hz : ‖z‖ ≤ R) : ‖∑ i : Fin D₁, ∑ j : Fin D₂, a i j * z ^ ↑i * Complex.exp (↑↑j * l * z)‖ ≤ ↑D₁ * ↑D₂ * A * T ^ D₁ * Real.exp (↑D₂ * ‖l‖ * T) * (3 * R / T) ^ L ^ 2

Schwarz's lemma for Schneider's auxiliary function. Let β ∈ ℂ be irrational and let F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j λ z) vanish at u + v β for 1 ≤ u, v ≤ L. If ‖a_{ij}‖ ≤ A, L (1 + ‖β‖) ≤ R, 3 R ≤ T and 1 ≤ T, then on the disc ‖z‖ ≤ R ‖F z‖ ≤ D₁ D₂ A T ^ D₁ exp (D₂ ‖λ‖ T) (3 R / T) ^ (L ^ 2).

theorem TauCeti.exists_norm_schneider_auxiliary_le_exp {β : ℂ} (hβ : ∀ (q : ℚ), ↑q ≠ β) (l : ℂ) (c₁ : ℝ) (c : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (L D₁ D₂ : ℕ), 2 ≤ L → ∀ (a : Fin D₁ → Fin D₂ → ℂ), (∀ (i : Fin D₁) (j : Fin D₂), ‖a i j‖ ≤ Real.exp (c₁ * (↑D₁ * Real.log ↑L + ↑D₂ * ↑L))) → (∀ (u v : ℕ), 1 ≤ u → u ≤ L → 1 ≤ v → v ≤ L → ∑ i : Fin D₁, ∑ j : Fin D₂, a i j * (↑u + ↑v * β) ^ ↑i * Complex.exp (↑↑j * l * (↑u + ↑v * β)) = 0) → ∀ (u v : ℕ), u ≤ c * L → v ≤ c * L → ‖∑ i : Fin D₁, ∑ j : Fin D₂, a i j * (↑u + ↑v * β) ^ ↑i * Complex.exp (↑↑j * l * (↑u + ↑v * β))‖ ≤ Real.exp (C * (↑D₁ * Real.log ↑L + ↑D₂ * ↑L) - ↑L ^ 2)

Extrapolation of Schneider's auxiliary function, the estimate of Evertse's Lemma 4.27 for arbitrary parameters. Let β ∈ ℂ be irrational, λ ∈ ℂ, c₁ ∈ ℝ and c ∈ ℕ. There is C ≥ 0 such that the following holds for all L ≥ 2 and D₁, D₂. If F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j λ z) has coefficients ‖a_{ij}‖ ≤ exp (c₁ (D₁ log L + D₂ L)) and vanishes at u + v β for 1 ≤ u, v ≤ L, then ‖F(u + v β)‖ ≤ exp (C (D₁ log L + D₂ L) - L ^ 2) for all 0 ≤ u, v ≤ c L.

theorem TauCeti.exists_norm_schneider_auxiliary_le_exp_rpow {β : ℂ} (hβ : ∀ (q : ℚ), ↑q ≠ β) (l : ℂ) (d : ℕ) (c₁ : ℝ) (c : ℕ) : ∃ (c₄ : ℝ), ∀ (M L D₁ D₂ : ℕ), 1 ≤ M → L = 2 * d * M ^ 2 → D₁ = (2 * d) ^ 2 * M ^ 3 → D₂ = 2 * d * M → ∀ (a : Fin D₁ → Fin D₂ → ℂ), (∀ (i : Fin D₁) (j : Fin D₂), ‖a i j‖ ≤ Real.exp (c₁ * (↑D₁ * Real.log ↑L + ↑D₂ * ↑L))) → (∀ (u v : ℕ), 1 ≤ u → u ≤ L → 1 ≤ v → v ≤ L → ∑ i : Fin D₁, ∑ j : Fin D₂, a i j * (↑u + ↑v * β) ^ ↑i * Complex.exp (↑↑j * l * (↑u + ↑v * β)) = 0) → ∀ (u v : ℕ), u ≤ c * L → v ≤ c * L → ‖∑ i : Fin D₁, ∑ j : Fin D₂, a i j * (↑u + ↑v * β) ^ ↑i * Complex.exp (↑↑j * l * (↑u + ↑v * β))‖ ≤ Real.exp (c₄ * ↑L ^ (3 / 2) * Real.log ↑L - ↑L ^ 2)

Extrapolation of Schneider's auxiliary function, Lemma 4.27 form (Evertse, Lemma 4.27). Let β ∈ ℂ be irrational, λ ∈ ℂ, c₁ ∈ ℝ and d, c ∈ ℕ. There is c₄ such that, for Schneider's parameters L = 2 d M², D₁ = (2 d)² M³, D₂ = 2 d M with M ≥ 1, every F(z) = ∑_{i < D₁, j < D₂} a_{ij} z ^ i exp (j λ z) with coefficients ‖a_{ij}‖ ≤ exp (c₁ (D₁ log L + D₂ L)) vanishing at u + v β for 1 ≤ u, v ≤ L satisfies ‖F(u + v β)‖ ≤ exp (c₄ L ^ (3 / 2) log L - L ^ 2) for all 0 ≤ u, v ≤ c L.