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.mulHeightBound_zero_one {K : Type u_4} [Field K] [AdmissibleAbsValues K] : 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.