Height bounds for linear and polynomial maps

We prove an upper bound for the height of the image of a tuple under a linear map.

We also prove upper and lower bounds for the height of fun i ↦ eval P i x, where P is a family of homogeneous polynomials over the field K of the same degree N and x : ι → K with ι finite.

theorem IsNonarchimedean.apply_sum_le {α : Type u_3} {β : Type u_4} {F : Type u_5} [AddCommMonoid β] [FunLike F β ℝ] [NonnegHomClass F β ℝ] [ZeroHomClass F β ℝ] {v : F} (hv : IsNonarchimedean ⇑v) {l : α → β} {s : Finset α} : v (∑ i ∈ s, l i) ≤ ⨆ (i : ↥s), v (l ↑i)

The ultrametric triangle inequality for finite sums.

Upper bound for the height of the image under a linear map

theorem AbsoluteValue.iSup_abv_linearMap_apply_le {K : Type u_1} [Field K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Finite ι'] (v : AbsoluteValue K ℝ) (A : ι' × ι → K) (x : ι → K) : ⨆ (j : ι'), v (∑ i : ι, A (j, i) * x i) ≤ (↑(Nat.card ι) * ⨆ (ji : ι' × ι), v (A ji)) * ⨆ (i : ι), v (x i)

theorem IsNonarchimedean.iSup_abv_linearMap_apply_le {K : Type u_1} [Field K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Finite ι'] {v : AbsoluteValue K ℝ} (hv : IsNonarchimedean ⇑v) (A : ι' × ι → K) (x : ι → K) : ⨆ (j : ι'), v (∑ i : ι, A (j, i) * x i) ≤ (⨆ (ji : ι' × ι), v (A ji)) * ⨆ (i : ι), v (x i)

theorem Height.mulHeight_linearMap_apply_le {K : Type u_1} [Field K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Finite ι'] [AdmissibleAbsValues K] [Nonempty ι] (A : ι' × ι → K) (x : ι → K) : (mulHeight fun (j : ι') => ∑ i : ι, A (j, i) * x i) ≤ ↑(Nat.card ι) ^ totalWeight K * mulHeight A * mulHeight x

Let A : ι' × ι → K, which we can interpret as a linear map from ι → K to ι' → K. Let x : ι → K be a tuple. Then the multiplicative height of A x is bounded by #ι ^ totalWeight K * mulHeight A * mulHeight x (if ι is nonempty).

Note: We use the uncurried form of A so that we can write mulHeight A.

theorem Height.logHeight_linearMap_apply_le {K : Type u_1} [Field K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Finite ι'] [AdmissibleAbsValues K] (A : ι' × ι → K) (x : ι → K) : (logHeight fun (j : ι') => ∑ i : ι, A (j, i) * x i) ≤ ↑(totalWeight K) * Real.log ↑(Nat.card ι) + logHeight A + logHeight x

Let A : ι' × ι → K, which we can interpret as a linear map from ι → K to ι' → K. Let x : ι → K be a tuple. Then the logarithmic height of A x is bounded by totalWeight K * log #ι + logHeight A + logHeight x.

(Note that here we do not need to assume that ι is nonempty, due to the convenient junk value log 0 = 0.)

Upper bound for the height of the image under a polynomial map

If p : ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree N and x : ι → K, then the multiplicative height of fun j ↦ (p j).eval x is bounded above by an (explicit) constant depending only on p times the Nth power of the multiplicative height of x. A similar statement holds for the logarithmic height.

theorem AbsoluteValue.eval_mvPolynomial_le {K : Type u_4} [Field K] {ι : Type u_5} [Finite ι] (v : AbsoluteValue K ℝ) {p : MvPolynomial ι K} {N : ℕ} (hp : p.IsHomogeneous N) (x : ι → K) : v ((MvPolynomial.eval x) p) ≤ (Finsupp.sum p fun (x : ι →₀ ℕ) (c : K) => v c) * (⨆ (i : ι), v (x i)) ^ N

theorem IsNonarchimedean.eval_mvPolynomial_le {K : Type u_4} [Field K] {ι : Type u_5} [Finite ι] {v : AbsoluteValue K ℝ} (hv : IsNonarchimedean ⇑v) {p : MvPolynomial ι K} {N : ℕ} (hp : p.IsHomogeneous N) (x : ι → K) : v ((MvPolynomial.eval x) p) ≤ (⨆ (s : ↥p.support), v (MvPolynomial.coeff (↑s) p)) * (⨆ (i : ι), v (x i)) ^ N

noncomputable def Height.mulHeightBound {K : Type u_4} [Field K] {ι : Type u_5} {ι' : Type u_6} [AdmissibleAbsValues K] (p : ι' → MvPolynomial ι K) : ℝ

The constant in the (upper) height bound on values of p.

Equations

• One or more equations did not get rendered due to their size.

theorem Height.mulHeightBound_eq {K : Type u_4} [Field K] {ι : Type u_5} {ι' : Type u_6} [AdmissibleAbsValues K] (p : ι' → MvPolynomial ι K) : mulHeightBound p = (Multiset.map (fun (v : AbsoluteValue K ℝ) => ⨆ (j : ι'), Finsupp.sum (p j) fun (x : ι →₀ ℕ) (c : K) => v c) AdmissibleAbsValues.archAbsVal).prod * ∏ᶠ (v : ↑AdmissibleAbsValues.nonarchAbsVal), ⨆ (j : ι'), max (⨆ (s : ↥(p j).support), ↑v (MvPolynomial.coeff (↑s) (p j))) 1

theorem Height.max_mulHeightBound_zero_one_eq_one (K : Type u_4) [Field K] (ι : Type u_5) (ι' : Type u_6) [AdmissibleAbsValues K] : max (mulHeightBound 0) 1 = 1

theorem Height.mulHeight_eval_le {K : Type u_4} [Field K] {ι : Type u_5} {ι' : Type u_6} [AdmissibleAbsValues K] [Finite ι'] [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K} (hp : ∀ (i : ι'), (p i).IsHomogeneous N) (x : ι → K) : (mulHeight fun (j : ι') => (MvPolynomial.eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Let K be a field with an admissible family of absolute values (giving rise to a multiplicative height). Let p be a family (indexed by ι') of homogeneous polynomials in variables indexed by the finite type ι and of the same degree N. Then for any x : ι → K, the multiplicative height of fun j : ι' ↦ eval x (p j) is bounded by a positive constant (which is made explicit) times mulHeight x ^ N.

theorem Height.mulHeight_eval_le' {K : Type u_4} [Field K] {ι : Type u_5} {ι' : Type u_6} [AdmissibleAbsValues K] [Finite ι'] [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K} (hp : ∀ (i : ι'), (p i).IsHomogeneous N) : ∃ C > 0, ∀ (x : ι → K), (mulHeight fun (j : ι') => (MvPolynomial.eval x) (p j)) ≤ C * mulHeight x ^ N

Let K be a field with an admissible family of absolute values (giving rise to a multiplicative height). Let p be a family (indexed by ι') of homogeneous polynomials in variables indexed by the finite type ι and of the same degree N. Then for any x : ι → K, the multiplicative height of fun j : ι' ↦ eval x (p j) is bounded by a positive constant times mulHeight x ^ N.

The difference to mulHeight_eval_le is that the constant is not made explicit.

theorem Height.logHeight_eval_le {K : Type u_4} [Field K] {ι : Type u_5} {ι' : Type u_6} [AdmissibleAbsValues K] [Finite ι'] [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K} (hp : ∀ (i : ι'), (p i).IsHomogeneous N) (x : ι → K) : (logHeight fun (j : ι') => (MvPolynomial.eval x) (p j)) ≤ Real.log (max (mulHeightBound p) 1) + ↑N * logHeight x

Let K be a field with an admissible family of absolute values (giving rise to a logarithmic height). Let p be a family (indexed by ι') of homogeneous polynomials in variables indexed by the finite type ι and of the same degree N. Then for any x : ι → K, the logarithmic height of fun j : ι' ↦ eval x (p j) is bounded by a constant (which is made explicit) plus N * logHeight x.

theorem Height.logHeight_eval_le' {K : Type u_4} [Field K] {ι : Type u_5} {ι' : Type u_6} [AdmissibleAbsValues K] [Finite ι'] [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K} (hp : ∀ (i : ι'), (p i).IsHomogeneous N) : ∃ (C : ℝ), ∀ (x : ι → K), (logHeight fun (j : ι') => (MvPolynomial.eval x) (p j)) ≤ C + ↑N * logHeight x

Let K be a field with an admissible family of absolute values (giving rise to a logarithmic height). Let p be a family (indexed by ι') of homogeneous polynomials in variables indexed by the finite type ι and of the same degree N. Then for any x : ι → K, the logarithmic height of fun j : ι' ↦ eval x (p j) is bounded by a constant plus N * logHeight x.

The difference to logHeight_eval_le is that the constant is not made explicit.

Lower bound for the height of the image under a polynomial map

If

• p : ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree N,
• q : ι × ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree M,
• x : ι → K is such that for all k : ι, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N), then the multiplicative height of fun j ↦ (p j).eval x is bounded below by an (explicit) positive constant depending only on q times the Nth power of the mutiplicative height of x. A similar statement holds for the logarithmic height.

Note that we only require the polynomial relations ∑ j, q (k, j) * p j = X k ^ (M + N) to hold after evaluating at x. In this way, we can apply the result to points on some subvariety of projective space when the map given by p is a morphism on that subvariety, but not necessarily on all of the ambient space. In fact, the proof does not even need that p j is homogeneous (of fixed degree). In applications, this will be the case, however, and if the third condition above holds on the level of polynomials, then it follows.

The main idea is to reduce this to a combination of mulHeight_linearMap_apply_le and mulHeight_eval_le.

theorem Height.mulHeight_eval_ge {K : Type u_6} [Field K] {ι : Type u_7} {ι' : Type u_8} [Fintype ι'] [AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K} (hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M) (p : ι' → MvPolynomial ι K) {x : ι → K} (h : ∀ (k : ι), ∑ j : ι', (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) : (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1)⁻¹ * mulHeight x ^ N ≤ mulHeight fun (j : ι') => (MvPolynomial.eval x) (p j)

If

• p : ι' → MvPolynomial ι K is a family of polynomials (which in practice will be homogeneous of the same degree N),
• q : ι × ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree M,
• x : ι → K is such that for all k : ι, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N), then the multiplicative height of fun j ↦ (p j).eval x is bounded below by an (explicit) positive constant depending only on q times the Nth power of the mutiplicative height of x.

theorem Height.mulHeight_eval_ge' {K : Type u_6} [Field K] {ι : Type u_7} {ι' : Type u_8} [Fintype ι'] [AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K} (hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M) : ∃ C > 0, ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}, (∀ (k : ι), ∑ j : ι', (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) → C * mulHeight x ^ N ≤ mulHeight fun (j : ι') => (MvPolynomial.eval x) (p j)

If

• p : ι' → MvPolynomial ι K is a family of polynomials (which in practice will be homogeneous of the same degree N),
• q : ι × ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree M,
• x : ι → K is such that for all k : ι, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N), then the multiplicative height of fun j ↦ (p j).eval x is bounded below by a positive constant depending only on q times the Nth power of the mutiplicative height of x.

The difference to mulHeight_eval_ge is that the constant is not made explicit.

theorem Height.logHeight_eval_ge {K : Type u_6} [Field K] {ι : Type u_7} {ι' : Type u_8} [Fintype ι'] [AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K} (hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M) (p : ι' → MvPolynomial ι K) {x : ι → K} (h : ∀ (k : ι), ∑ j : ι', (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) : -Real.log (↑(Nat.card ι') ^ totalWeight K * max (mulHeightBound q) 1) + ↑N * logHeight x ≤ logHeight fun (j : ι') => (MvPolynomial.eval x) (p j)

If

• p : ι' → MvPolynomial ι K is a family of polynomials (which in practice will be homogeneous of the same degree N),
• q : ι × ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree M,
• x : ι → K is such that for all k : ι, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N), then the logarithmic height of fun j ↦ (p j).eval x is bounded below by an (explicit) constant depending only on q plus N times the logarithmic height of x.

theorem Height.logHeight_eval_ge' {K : Type u_6} [Field K] {ι : Type u_7} {ι' : Type u_8} [Fintype ι'] [AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K} (hq : ∀ (a : ι × ι'), (q a).IsHomogeneous M) : ∃ (C : ℝ), ∀ (p : ι' → MvPolynomial ι K) {x : ι → K}, (∀ (k : ι), ∑ j : ι', (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) → C + ↑N * logHeight x ≤ logHeight fun (j : ι') => (MvPolynomial.eval x) (p j)

If

• p : ι' → MvPolynomial ι K is a family of polynomials (which in practice will be homogeneous of the same degree N),
• q : ι × ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree M,
• x : ι → K is such that for all k : ι, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N), then the logarithmic height of fun j ↦ (p j).eval x is bounded below by a constant plus N times the logarithmic height of x.

The difference to logHeight_eval_ge is that the constant is not made explicit.

Bounds for the height of ![x*y, x+y, 1]

We show that the multiplicative height of ![a*c, a*d + b*c, b*d] is bounded from above and from below by a positive constant times the product of the multiplicative heights of ![a, b] and ![c, d] (and the analogous statements for the logarithmic heights).

The constants are unspecified here; with (likely considerably, but trivial) more work, we could make them explicit.

theorem Height.mulHeight_mul_mulHeight {K : Type u_4} [Field K] [AdmissibleAbsValues K] {a b c d : K} (hab : ![a, b] ≠ 0) (hcd : ![c, d] ≠ 0) : mulHeight ![a, b] * mulHeight ![c, d] = mulHeight ![a * c, a * d, b * c, b * d]

theorem Height.mulHeight_sym2_le (K : Type u_4) [Field K] [AdmissibleAbsValues K] : ∃ C > 0, ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C * mulHeight ![a, b] * mulHeight ![c, d]

theorem Height.mulHeight_sym2_ge (K : Type u_4) [Field K] [AdmissibleAbsValues K] : ∃ C > 0, ∀ {a b c d : K}, ![a, b] ≠ 0 → ![c, d] ≠ 0 → C * mulHeight ![a, b] * mulHeight ![c, d] ≤ mulHeight ![a * c, a * d + b * c, b * d]

theorem Height.logHeight_sym2_le (K : Type u_4) [Field K] [AdmissibleAbsValues K] : ∃ (C : ℝ), ∀ (a b c d : K), logHeight ![a * c, a * d + b * c, b * d] ≤ C + logHeight ![a, b] + logHeight ![c, d]

theorem Height.logHeight_sym2_ge (K : Type u_4) [Field K] [AdmissibleAbsValues K] : ∃ (C : ℝ), ∀ {a b c d : K}, ![a, b] ≠ 0 → ![c, d] ≠ 0 → C + logHeight ![a, b] + logHeight ![c, d] ≤ logHeight ![a * c, a * d + b * c, b * d]

theorem Height.abs_logHeight_sym2_sub_le (K : Type u_4) [Field K] [AdmissibleAbsValues K] : ∃ (C : ℝ), ∀ {a b c d : K}, ![a, b] ≠ 0 → ![c, d] ≠ 0 → |logHeight ![a * c, a * d + b * c, b * d] - (logHeight ![a, b] + logHeight ![c, d])| ≤ C