Baker's binomial polynomials

For k : ℕ, Baker's binomial polynomial is

Δ(X; k) = (X + 1) (X + 2) ⋯ (X + k) / k!,

so that Δ(n; k) = (n + k choose k) at natural numbers n. In the language of binomial rings this is the multiset coefficient Ring.multichoose (X + 1 : ℚ[X]) k, which is how it is written here; its Pascal recursion is Ring.multichoose_succ_succ, and its translates and values follow from Ring.map_multichoose. In the method of linear forms in logarithms, archimedean as well as p-adic, the auxiliary functions are built from the divided derivatives

Δ(x; k, l, m) = (1 / m!) (d / dx) ^ m (Δ(x; k) ^ l),

which are written here as (hasseDeriv m (Ring.multichoose (X + 1 : ℚ[X]) k ^ l)).eval x. The estimates on such an auxiliary function at integral points use two bounds for these numbers: a denominator bound and a size bound.

• Denominators. If L is an integer divisible by each of 1, …, k, for instance L = lcm(1, …, k), then L ^ m Δ(x; k, l, m) is an integer for every integer x. The polynomial form of this is that Δ(a + L X; k) has integral coefficients for every integer a. For a = 0 it is the product of the integral linear polynomials 1 + (L / j) X, and the Pascal recursion Δ(X + 1; k + 1) = Δ(X; k + 1) + Δ(X + 1; k) moves a up and down. The Taylor expansion of Δ(X; k) ^ l at x, rescaled by L, has the numbers L ^ m Δ(x; k, l, m) as coefficients.
• Size. If x is rational with |x| ≤ n, then |Δ(x; k, l, m)| ≤ 2 ^ (l (n + k + 1)), because the coefficient length of Δ(X + x; k) is at most (n + k + 1 choose k).

Read at a single prime p, the denominator bound with L = lcm(1, …, k) says that v_p(Δ(x; k, l, m)) ≥ -m v_p(lcm(1, …, k)) for every integer x.

Main results

• TauCeti.degree_multichoose_X_add_one: Δ(X; k) has degree k.
• TauCeti.multichoose_X_add_one_comp_C_add_C_mul_X_mem_lifts: Δ(a + L X; k) has integral coefficients.
• TauCeti.pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast: Baker's denominator bound, L ^ m Δ(x; k, l, m) ∈ ℤ for integral x.
• TauCeti.lcm_pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast: its classical form, with L = lcm(1, …, k).
• TauCeti.pow_mul_eval_hasseDeriv_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast: the denominator bound for Δ(q X; k) over a field of characteristic zero, at points x with q x integral.
• TauCeti.eval_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast: its case m = 0, Δ(q x; k) ∈ ℤ.
• TauCeti.bakerDeltaSequence: for q ≠ 0, the polynomials Δ(q X; k) over a field of characteristic zero form a polynomial sequence.
• TauCeti.abs_eval_hasseDeriv_multichoose_X_add_one_pow_le: the size bound.

References

• A. Baker, A sharpening of the bounds for linear forms in logarithms, Acta Arith. 21 (1972), 117–129.
• Kunrui Yu, Linear forms in p-adic logarithms II, Compositio Math. 74 (1990), 15–113, §1.

@[simp]

theorem TauCeti.degree_multichoose_X_add_one (k : ℕ) : (Ring.multichoose (Polynomial.X + 1) k).degree = ↑k

Baker's binomial polynomial Δ(X; k) has degree k.

@[simp]

theorem TauCeti.natDegree_multichoose_X_add_one (k : ℕ) : (Ring.multichoose (Polynomial.X + 1) k).natDegree = k

Baker's binomial polynomial Δ(X; k) has natural degree k.

theorem TauCeti.multichoose_X_add_one_comp_C_add_C_mul_X_mem_lifts {k : ℕ} {L : ℤ} (hL : ∀ j ∈ Finset.Icc 1 k, ↑j ∣ L) (a : ℤ) : (Ring.multichoose (Polynomial.X + 1) k).comp (Polynomial.C ↑a + Polynomial.C ↑L * Polynomial.X) ∈ Polynomial.lifts (Int.castRingHom ℚ)

Integer translates of Baker's binomial polynomial. If each of 1, …, k divides the integer L, then Δ(a + L X; k) has integral coefficients for every integer a.

theorem TauCeti.pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast {k : ℕ} {L : ℤ} (hL : ∀ j ∈ Finset.Icc 1 k, ↑j ∣ L) (l m : ℕ) (x : ℤ) : ↑L ^ m * Polynomial.eval (↑x) ((Polynomial.hasseDeriv m) (Ring.multichoose (Polynomial.X + 1) k ^ l)) ∈ Set.range Int.cast

Baker's denominator bound. If each of 1, …, k divides the integer L, then for every integer x and all l, m,

L ^ m Δ(x; k, l, m) = L ^ m (1 / m!) (d / dx) ^ m (Δ(x; k) ^ l)

is an integer.

theorem TauCeti.lcm_pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast (k l m : ℕ) (x : ℤ) : ↑((Finset.Icc 1 k).lcm id) ^ m * Polynomial.eval (↑x) ((Polynomial.hasseDeriv m) (Ring.multichoose (Polynomial.X + 1) k ^ l)) ∈ Set.range Int.cast

Baker's denominator bound, classical form: for every integer x and all l, m, lcm(1, …, k) ^ m Δ(x; k, l, m) is an integer.

theorem TauCeti.pow_mul_eval_hasseDeriv_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast {K : Type u_1} [Field K] [CharZero K] {k : ℕ} {L : ℤ} (hL : ∀ j ∈ Finset.Icc 1 k, ↑j ∣ L) (q : ℤ) {x : K} (hx : ↑q * x ∈ Set.range Int.cast) (m : ℕ) : ↑L ^ m * Polynomial.eval x ((Polynomial.hasseDeriv m) (Polynomial.map (algebraMap ℚ K) ((Ring.multichoose (Polynomial.X + 1) k).comp (Polynomial.C ↑q * Polynomial.X)))) ∈ Set.range Int.cast

Baker's denominator bound at points of a scaled lattice. Let K be a field of characteristic zero, q an integer and x ∈ K with q x an integer, and let L be an integer divisible by each of 1, …, k. Then for every m,

L ^ m (1 / m!) (d / dx) ^ m Δ(q x; k)

is an integer. Here Δ(q X; k) is mapped to K[X] and differentiated in X. For q = 1 and x integral this is the case l = 1 of TauCeti.pow_mul_eval_hasseDeriv_multichoose_X_add_one_pow_mem_range_intCast.

theorem TauCeti.eval_map_multichoose_X_add_one_comp_C_mul_X_mem_range_intCast {K : Type u_1} [Field K] [CharZero K] (k : ℕ) (q : ℤ) {x : K} (hx : ↑q * x ∈ Set.range Int.cast) : Polynomial.eval x (Polynomial.map (algebraMap ℚ K) ((Ring.multichoose (Polynomial.X + 1) k).comp (Polynomial.C ↑q * Polynomial.X))) ∈ Set.range Int.cast

Integer values of Baker's binomial polynomial at points of a scaled lattice. Let K be a field of characteristic zero, q an integer and x ∈ K with q x an integer. Then Δ(q x; k) is an integer.

noncomputable def TauCeti.bakerDeltaSequence (K : Type u_1) [Field K] [CharZero K] {q : ℤ} (hq : q ≠ 0) : Polynomial.Sequence K

For an integer q ≠ 0, Baker's binomial polynomials Δ(q X; k), mapped to K[X] for a field K of characteristic zero, form a polynomial sequence: Δ(q X; k) has degree k.

@[simp]

theorem TauCeti.bakerDeltaSequence_apply (K : Type u_1) [Field K] [CharZero K] {q : ℤ} (hq : q ≠ 0) (k : ℕ) : ↑(bakerDeltaSequence K hq) k = Polynomial.map (algebraMap ℚ K) ((Ring.multichoose (Polynomial.X + 1) k).comp (Polynomial.C ↑q * Polynomial.X))

The k-th term of TauCeti.bakerDeltaSequence K hq is Δ(q X; k).

theorem TauCeti.isUnit_leadingCoeff_bakerDeltaSequence (K : Type u_1) [Field K] [CharZero K] {q : ℤ} (hq : q ≠ 0) (k : ℕ) : IsUnit (↑(bakerDeltaSequence K hq) k).leadingCoeff

The leading coefficients of the polynomials Δ(q X; k) are units.

theorem TauCeti.abs_eval_hasseDeriv_multichoose_X_add_one_pow_le {x : ℚ} {n : ℕ} (hx : |x| ≤ ↑n) (k l m : ℕ) : |Polynomial.eval x ((Polynomial.hasseDeriv m) (Ring.multichoose (Polynomial.X + 1) k ^ l))| ≤ 2 ^ (l * (n + k + 1))

The size bound. If |x| ≤ n, then for all k, l, m,

|Δ(x; k, l, m)| = |(1 / m!) (d / dx) ^ m (Δ(x; k) ^ l)| ≤ 2 ^ (l (n + k + 1)).