Interpolation on grids of p-adic integers

In the p-adic method of linear forms in logarithms, an auxiliary function f analytic on a closed disc of radius c ≥ 1 over a field K ⊇ ℚ_p vanishes to order T at the points of a grid of p-adic integers, typically rational integers. The Schwarz lemma for restricted series bounds f at every other p-adic integer x by the interpolation denominator ∏_{b} (x - b):

‖f(x)‖ ≤ ‖f‖_c * (‖∏_{b ∈ s} (x - b)‖ / c ^ #s) ^ T.

This file makes the denominators explicit for the grids of the method.

• For an arithmetic progression a, a + d, …, a + (n - 1) d with unit step d, rescaling by d turns the denominator into a value y (y - 1) ⋯ (y - n + 1) of the descending Pochhammer polynomial on ℤ_p, which Mathlib bounds by ‖n!‖ (PadicInt.norm_ascPochhammer_le). Hence ‖∏_{j < n} (x - (a + j d))‖ ≤ ‖n!‖, whatever the position of x.
• For the integers 0 ≤ j < N not divisible by an auxiliary integer q prime to p, the grid contains the q - 1 progressions r + q m, 1 ≤ r < q, m < ⌊N / q⌋, each with unit step q. Hence the denominator has norm at most ‖⌊N / q⌋!‖ ^ (q - 1).

The extrapolation steps of the method also need the Hasse derivatives of f at new points. Since D⁽ᵏ⁾ f vanishes to order T - k on the grid and ‖D⁽ᵏ⁾ f‖_c ≤ c⁻ᵏ ‖f‖_c, each bound holds for D⁽ᵏ⁾ f with the exponent T - k and an extra factor c⁻ᵏ:

‖(D⁽ᵏ⁾ f)(x)‖ ≤ c⁻ᵏ * ‖f‖_c * (‖∏_{b ∈ s} (x - b)‖ / c ^ #s) ^ (T - k).

Main results

• PadicInt.norm_prod_range_sub_add_mul_le: the factorial bound for a progression with unit step.
• PadicInt.norm_prod_filter_not_dvd_sub_le: the bound for the integers not divisible by q.
• PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_prod: the Schwarz lemma on a grid of p-adic integers, with the interpolation denominator.
• PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial, PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial_pow: its explicit forms on a progression and on the integers not divisible by q.
• PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_norm_prod, PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_norm_factorial, PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_norm_factorial_pow: the same three bounds for the Hasse derivatives D⁽ᵏ⁾ f.

References

• K. Yu, Linear forms in p-adic logarithms. II, Compositio Math. 74 (1990), 15–113, §1.

theorem PadicInt.norm_prod_range_sub_add_mul_le {p : ℕ} [Fact (Nat.Prime p)] (x a : ℤ_[p]) {d : ℤ_[p]} (hd : IsUnit d) (n : ℕ) : ‖∏ j ∈ Finset.range n, (x - (a + ↑j * d))‖ ≤ ‖↑n.factorial‖

Interpolation denominators on a progression. For p-adic integers x and a and a unit step d, the product of the distances from x to the n points a + j d, j < n, has norm at most ‖n!‖.

theorem PadicInt.norm_prod_filter_not_dvd_sub_le {p : ℕ} [Fact (Nat.Prime p)] (x : ℤ_[p]) {q : ℕ} (hq : p.Coprime q) (N : ℕ) : ‖∏ j ∈ Finset.range N with ¬q ∣ j, (x - ↑j)‖ ≤ ‖↑(N / q).factorial‖ ^ (q - 1)

Interpolation denominators on the integers not divisible by q. Let q be prime to p. For a p-adic integer x, the product of the distances from x to the integers 0 ≤ j < N not divisible by q has norm at most ‖⌊N / q⌋!‖ ^ (q - 1).

theorem PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_prod {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} (hf : IsRestricted c f) (hc : 1 ≤ c) {s : Finset ℤ_[p]} {T : ℕ} (hzero : ∀ b ∈ s, ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ((algebraMap ℚ_[p] K) ↑b) = 0) (x : ℤ_[p]) : ‖f.evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤ gaussNorm norm c f * (‖∏ b ∈ s, (x - b)‖ / c ^ s.card) ^ T

The Schwarz lemma on a grid of p-adic integers. Let K be a complete normed field extension of ℚ_p and f a power series over K restricted at a radius c ≥ 1. If the Hasse derivatives (D⁽ᵗ⁾ f)(b) vanish for t < T at every point b of a finite set s of p-adic integers, then at every p-adic integer x

‖f(x)‖ ≤ ‖f‖_c * (‖∏_{b ∈ s} (x - b)‖ / c ^ #s) ^ T.

theorem PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} (hf : IsRestricted c f) (hc : 1 ≤ c) (a : ℤ_[p]) {d : ℤ_[p]} (hd : IsUnit d) {n T : ℕ} (hzero : ∀ j < n, ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ((algebraMap ℚ_[p] K) ↑(a + ↑j * d)) = 0) (x : ℤ_[p]) : ‖f.evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤ gaussNorm norm c f * (‖↑n.factorial‖ / c ^ n) ^ T

The Schwarz lemma on a progression of p-adic integers. Let K be a complete normed field extension of ℚ_p and f a power series over K restricted at a radius c ≥ 1. If the Hasse derivatives (D⁽ᵗ⁾ f)(a + j d) vanish for t < T and j < n, where d is a unit of ℤ_p, then at every p-adic integer x

‖f(x)‖ ≤ ‖f‖_c * (‖n!‖ / c ^ n) ^ T.

theorem PowerSeries.IsRestricted.norm_evalAt_le_gaussNorm_mul_norm_factorial_pow {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} (hf : IsRestricted c f) (hc : 1 ≤ c) {q : ℕ} (hq : p.Coprime q) {N T : ℕ} (hzero : ∀ j < N, ¬q ∣ j → ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ↑j = 0) (x : ℤ_[p]) : ‖f.evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤ gaussNorm norm c f * (‖↑(N / q).factorial‖ ^ (q - 1) / c ^ {x ∈ Finset.range N | ¬q ∣ x}.card) ^ T

The Schwarz lemma on the integers not divisible by q. Let K be a complete normed field extension of ℚ_p, f a power series over K restricted at a radius c ≥ 1, and q an integer prime to p. If the Hasse derivatives (D⁽ᵗ⁾ f)(j) vanish for t < T at every integer 0 ≤ j < N not divisible by q, a grid of S points, then at every p-adic integer x

‖f(x)‖ ≤ ‖f‖_c * (‖⌊N / q⌋!‖ ^ (q - 1) / c ^ S) ^ T.

theorem PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_norm_prod {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} (hf : IsRestricted c f) (hc : 1 ≤ c) {s : Finset ℤ_[p]} {T : ℕ} (hzero : ∀ b ∈ s, ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ((algebraMap ℚ_[p] K) ↑b) = 0) (k : ℕ) (x : ℤ_[p]) : ‖((PowerSeries.hasseDeriv k) f).evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤ c⁻¹ ^ k * gaussNorm norm c f * (‖∏ b ∈ s, (x - b)‖ / c ^ s.card) ^ (T - k)

The Schwarz lemma for Hasse derivatives on a grid of p-adic integers. Let K be a complete normed field extension of ℚ_p and f a power series over K restricted at a radius c ≥ 1. If the Hasse derivatives (D⁽ᵗ⁾ f)(b) vanish for t < T at every point b of a finite set s of p-adic integers, then for every k and every p-adic integer x

‖(D⁽ᵏ⁾ f)(x)‖ ≤ c⁻ᵏ * ‖f‖_c * (‖∏_{b ∈ s} (x - b)‖ / c ^ #s) ^ (T - k).

theorem PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_norm_factorial {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} (hf : IsRestricted c f) (hc : 1 ≤ c) (a : ℤ_[p]) {d : ℤ_[p]} (hd : IsUnit d) {n T : ℕ} (hzero : ∀ j < n, ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ((algebraMap ℚ_[p] K) ↑(a + ↑j * d)) = 0) (k : ℕ) (x : ℤ_[p]) : ‖((PowerSeries.hasseDeriv k) f).evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤ c⁻¹ ^ k * gaussNorm norm c f * (‖↑n.factorial‖ / c ^ n) ^ (T - k)

The Schwarz lemma for Hasse derivatives on a progression of p-adic integers. Let K be a complete normed field extension of ℚ_p and f a power series over K restricted at a radius c ≥ 1. If the Hasse derivatives (D⁽ᵗ⁾ f)(a + j d) vanish for t < T and j < n, where d is a unit of ℤ_p, then for every k and every p-adic integer x

‖(D⁽ᵏ⁾ f)(x)‖ ≤ c⁻ᵏ * ‖f‖_c * (‖n!‖ / c ^ n) ^ (T - k).

theorem PowerSeries.IsRestricted.norm_evalAt_hasseDeriv_le_gaussNorm_mul_norm_factorial_pow {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_1} [NormedField K] [NormedAlgebra ℚ_[p] K] [CompleteSpace K] {c : ℝ} {f : PowerSeries K} (hf : IsRestricted c f) (hc : 1 ≤ c) {q : ℕ} (hq : p.Coprime q) {N T : ℕ} (hzero : ∀ j < N, ¬q ∣ j → ∀ t < T, ((PowerSeries.hasseDeriv t) f).evalAt ↑j = 0) (k : ℕ) (x : ℤ_[p]) : ‖((PowerSeries.hasseDeriv k) f).evalAt ((algebraMap ℚ_[p] K) ↑x)‖ ≤ c⁻¹ ^ k * gaussNorm norm c f * (‖↑(N / q).factorial‖ ^ (q - 1) / c ^ {x ∈ Finset.range N | ¬q ∣ x}.card) ^ (T - k)

The Schwarz lemma for Hasse derivatives on the integers not divisible by q. Let K be a complete normed field extension of ℚ_p, f a power series over K restricted at a radius c ≥ 1, and q an integer prime to p. If the Hasse derivatives (D⁽ᵗ⁾ f)(j) vanish for t < T at every integer 0 ≤ j < N not divisible by q, a grid of S points, then for every k and every p-adic integer x

‖(D⁽ᵏ⁾ f)(x)‖ ≤ c⁻ᵏ * ‖f‖_c * (‖⌊N / q⌋!‖ ^ (q - 1) / c ^ S) ^ (T - k).