The value of a polynomial at one absolute value

Let P be a polynomial over a commutative ring R with partial degrees degreeOf i P ≤ L i and coefficients of absolute value at most B under an absolute value v : AbsoluteValue R ℝ. This file bounds v(P(x)) at a point x, in two ways.

• Trivially. P(x) is a sum of at most ∏ i, (L i + 1) terms, each at most B ∏ i, max(v(x_i), 1) ^ L i. At a nonarchimedean v the count disappears. These bounds, AbsoluteValue.apply_eval_le and IsNonarchimedean.apply_eval_le, are in TauCeti.RingTheory.MvPolynomial.Abv.Eval; here they give the trivial bound for the jets.
• Through the Taylor expansion at a point a where P has weighted index at least t with respect to the weights L. Then P(x) = ∑_d (∂^d P)(a) (x - a)^d involves only multi-indices d ≤ L of weight ∑ i, d i / L i ≥ t. If every such d has ∏ i, v(x_i - a_i) ^ d i ≤ E, then v(P(x)) ≤ B (∏ i, (L i + 1))² ∏ i, (2 max(v(a_i), 1)) ^ L i · E, and at a nonarchimedean v simply v(P(x)) ≤ B ∏ i, max(v(a_i), 1) ^ L i · E.

In the proof of Roth's theorem over a number field K an auxiliary polynomial P over K vanishes to a high index at a point a with coordinates in a finite extension F, and is evaluated at a point x ∈ Kⁿ close to a at the places of a finite set S. The Taylor bound is the upper estimate for P(x) at a place of S; the trivial bound is the upper estimate at every other place, where the nonarchimedean form is needed because there are infinitely many of them. The comparison of the product of these bounds with the product formula is the contradiction that proves the theorem. The forms AbsoluteValue.LiesOver.apply_eval_le_of_le_weightedIndex and AbsoluteValue.LiesOver.apply_eval_le_of_le_weightedIndex_of_isNonarchimedean state the Taylor bound for P over K at an absolute value w of F lying over an absolute value v of K, so that the targets a need not lie in K.

Main results

• AbsoluteValue.apply_eval_hasseDeriv_le: the trivial bound for the jets (∂^d P)(a), whose coefficients carry an extra factor 2 ^ ∑ i, L i.
• AbsoluteValue.apply_eval_le_of_le_weightedIndex, IsNonarchimedean.apply_eval_le_of_le_weightedIndex: the bounds through the Taylor expansion at a point of weighted index at least t.
• AbsoluteValue.LiesOver.apply_eval_le_of_le_weightedIndex, AbsoluteValue.LiesOver.apply_eval_le_of_le_weightedIndex_of_isNonarchimedean: the same for a polynomial over K and a point a over an extension F.

References

• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §6.4, the proof of Theorem 6.4.1.
• L. Pottmeyer, Diophantine Approximation, lecture notes (2022), §3.5.3.

theorem AbsoluteValue.apply_eval_hasseDeriv_le {ι : Type u_1} {R : Type u_2} [Fintype ι] [CommRing R] (v : AbsoluteValue R ℝ) {P : MvPolynomial ι R} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) (a : ι → R) (d : ι →₀ ℕ) : v ((MvPolynomial.eval a) ((MvPolynomial.hasseDeriv d) P)) ≤ (B * ∏ i : ι, (↑(L i) + 1)) * ∏ i : ι, (2 * max (v (a i)) 1) ^ L i

The jets of a polynomial. If P has partial degrees degreeOf i P ≤ L i and coefficients of absolute value at most B, then every Hasse derivative of P satisfies v((∂^d P)(a)) ≤ B ∏ i, (L i + 1) ∏ i, (2 max(v(a_i), 1)) ^ L i.

theorem AbsoluteValue.apply_eval_le_of_le_weightedIndex {ι : Type u_1} {R : Type u_2} [Fintype ι] [CommRing R] [Nontrivial R] (v : AbsoluteValue R ℝ) {P : MvPolynomial ι R} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) {a : ι → R} {t : ℝ} (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex L a P) (x : ι → R) {E : ℝ} (hE0 : 0 ≤ E) (hE : ∀ (d : ι →₀ ℕ), (∀ (i : ι), d i ≤ L i) → t ≤ ∑ i : ι, ↑(d i) / ↑(L i) → ∏ i : ι, v (x i - a i) ^ d i ≤ E) : v ((MvPolynomial.eval x) P) ≤ (B * (∏ i : ι, (↑(L i) + 1)) ^ 2 * ∏ i : ι, (2 * max (v (a i)) 1) ^ L i) * E

The value of a polynomial near a point of high index. Let P have partial degrees degreeOf i P ≤ L i, coefficients of absolute value at most B, and weighted index at least t at a with respect to the weights L. If 0 ≤ E and ∏ i, v(x_i - a_i) ^ d i ≤ E for every multi-index d ≤ L of weight ∑ i, d i / L i ≥ t, then v(P(x)) ≤ B (∏ i, (L i + 1))² ∏ i, (2 max(v(a_i), 1)) ^ L i · E.

theorem AbsoluteValue.LiesOver.apply_eval_le_of_le_weightedIndex {ι : Type u_1} [Fintype ι] {K : Type u_3} {F : Type u_4} [CommRing K] [CommRing F] [Nontrivial F] [Algebra K F] [FaithfulSMul K F] (w : AbsoluteValue F ℝ) (v : AbsoluteValue K ℝ) [w.LiesOver v] {P : MvPolynomial ι K} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) {a : ι → F} {t : ℝ} (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex L a ((MvPolynomial.map (algebraMap K F)) P)) (x : ι → K) {E : ℝ} (hE0 : 0 ≤ E) (hE : ∀ (d : ι →₀ ℕ), (∀ (i : ι), d i ≤ L i) → t ≤ ∑ i : ι, ↑(d i) / ↑(L i) → ∏ i : ι, w ((algebraMap K F) (x i) - a i) ^ d i ≤ E) : v ((MvPolynomial.eval x) P) ≤ (B * (∏ i : ι, (↑(L i) + 1)) ^ 2 * ∏ i : ι, (2 * max (w (a i)) 1) ^ L i) * E

The value of a polynomial over K near a point over an extension F. Let w be an absolute value of F lying over the absolute value v of K, and let P over K have partial degrees degreeOf i P ≤ L i and coefficients with v-value at most B. If the image of P in F has weighted index at least t at a : ι → F, and ∏ i, w(x_i - a_i) ^ d i ≤ E with 0 ≤ E for every multi-index d ≤ L of weight at least t, then v(P(x)) ≤ B (∏ i, (L i + 1))² ∏ i, (2 max(w(a_i), 1)) ^ L i · E for x : ι → K.

theorem IsNonarchimedean.apply_eval_le_of_le_weightedIndex {ι : Type u_1} {R : Type u_2} [Fintype ι] [CommRing R] [Nontrivial R] {v : AbsoluteValue R ℝ} (hv : IsNonarchimedean ⇑v) {P : MvPolynomial ι R} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) {a : ι → R} {t : ℝ} (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex L a P) (x : ι → R) {E : ℝ} (hE0 : 0 ≤ E) (hE : ∀ (d : ι →₀ ℕ), (∀ (i : ι), d i ≤ L i) → t ≤ ∑ i : ι, ↑(d i) / ↑(L i) → ∏ i : ι, v (x i - a i) ^ d i ≤ E) : v ((MvPolynomial.eval x) P) ≤ (B * ∏ i : ι, max (v (a i)) 1 ^ L i) * E

The value of a polynomial near a point of high index, at a nonarchimedean absolute value. Let P have partial degrees degreeOf i P ≤ L i, coefficients of absolute value at most B, and weighted index at least t at a with respect to the weights L. If 0 ≤ E and ∏ i, v(x_i - a_i) ^ d i ≤ E for every multi-index d ≤ L of weight ∑ i, d i / L i ≥ t, then v(P(x)) ≤ B ∏ i, max(v(a_i), 1) ^ L i · E.

theorem AbsoluteValue.LiesOver.apply_eval_le_of_le_weightedIndex_of_isNonarchimedean {ι : Type u_1} [Fintype ι] {K : Type u_3} {F : Type u_4} [CommRing K] [CommRing F] [Nontrivial F] [Algebra K F] [FaithfulSMul K F] {w : AbsoluteValue F ℝ} (hw : IsNonarchimedean ⇑w) (v : AbsoluteValue K ℝ) [w.LiesOver v] {P : MvPolynomial ι K} {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) {B : ℝ} (hB : ∀ (s : ι →₀ ℕ), v (P.coeff s) ≤ B) {a : ι → F} {t : ℝ} (ht : ENNReal.ofReal t ≤ MvPolynomial.weightedIndex L a ((MvPolynomial.map (algebraMap K F)) P)) (x : ι → K) {E : ℝ} (hE0 : 0 ≤ E) (hE : ∀ (d : ι →₀ ℕ), (∀ (i : ι), d i ≤ L i) → t ≤ ∑ i : ι, ↑(d i) / ↑(L i) → ∏ i : ι, w ((algebraMap K F) (x i) - a i) ^ d i ≤ E) : v ((MvPolynomial.eval x) P) ≤ (B * ∏ i : ι, max (w (a i)) 1 ^ L i) * E

The value of a polynomial over K near a point over an extension F, at a nonarchimedean absolute value. Let w be a nonarchimedean absolute value of F lying over the absolute value v of K, and let P over K have partial degrees degreeOf i P ≤ L i and coefficients with v-value at most B. If the image of P in F has weighted index at least t at a : ι → F, and ∏ i, w(x_i - a_i) ^ d i ≤ E with 0 ≤ E for every multi-index d ≤ L of weight at least t, then v(P(x)) ≤ B ∏ i, max(w(a_i), 1) ^ L i · E for x : ι → K.