Height bounds for coordinate ratios and from local estimates

The height of a ratio of two coordinates is bounded by the projective height of the tuple, and the height of a quotient by the sum of the heights of its numerator and denominator. If t (x - θ₂ y) = x - θ₀ y, the formula x / y = (θ₀ - t θ₂) / (1 - t) bounds the height of x / y by those of t, θ₀ and θ₂; this recovers a Thue solution from a unit equation. These bounds control the affine coordinates of a projective point after normalization. Both multiplicative and logarithmic heights are treated over any field with admissible absolute values and any finite coordinate type.

Changing the signs of some coordinates of a tuple changes none of its local factors, so it does not change the height. Together with invariance under scaling and reindexing, this is how the height of a subspace is compared with the height of its orthogonal complement, whose Plücker coordinates are those of the subspace up to a common factor, signs and reindexing.

A height bound for a tuple z in terms of a tuple x often comes from estimates at each absolute value separately: the local factor ⨆ i, v (z i) is at most a constant times (⨆ j, v (x j)) ^ p at the archimedean absolute values, and at most (⨆ j, v (x j)) ^ p at the nonarchimedean ones. Height.mulHeight_le_of_forall_iSup_le multiplies these estimates over all absolute values. This is how heights of polynomial expressions such as determinants are bounded, since no bound for the height of a sum in terms of the heights of its terms holds. Its constant case Height.mulHeight_le_pow_totalWeight bounds the height of a single tuple whose local factors are at most C at the archimedean absolute values and at most 1 at the others; for instance a tuple of natural numbers at most N ≥ 1 has height at most N ^ totalWeight K (Height.mulHeight_natCast_le). Conversely, two tuples with the same local factors everywhere have the same height (Height.mulHeight_eq_of_forall_iSup_eq), which computes the height of the tuple of powers α ^ k, 0 ≤ k ≤ d, as mulHeight₁ α ^ d (Height.mulHeight_pow_range).

Implementation notes

The nonarchimedean step needs the finiteness of the multiplicative support of the local factors ⨆ i, v (x i), which Mathlib proves by the private fun_prop lemma Height.hasFiniteMulSupport_iSup_nonarchAbsVal in Mathlib/NumberTheory/Height/Basic.lean; it is reached by import all, as in TauCeti/NumberTheory/Height/LinearForm.lean.

References

The ratio bounds are adapted from Ralf Stephan's ArithmeticHeights/Northcott.lean in rwst/Subspace-Theorems, commit e443c2479e19f7665b31d8e94e2317c8ced1ca06 (Apache 2.0). The local-to-global bound follows DiophantineApproximation/HeightTransport.lean in the same repository, snapshot c26d909dc48cf7fe (Apache 2.0); see also E. Bombieri and W. Gubler, Heights in Diophantine Geometry (2006), §1.6. The constant bound, the bound for natural numbers and the height of the tuple of powers follow DiophantineApproximation/MonomialHeight.lean in the same repository, commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338 (Apache 2.0).

theorem Height.mulHeight₁_div_le_mulHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (i j : ι) : mulHeight₁ (x i / x j) ≤ mulHeight x

The multiplicative height of a ratio of two coordinates is at most the height of the tuple. The denominator may vanish, with division interpreted as the field's totalized division.

theorem Height.logHeight₁_div_le_logHeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K) (i j : ι) : logHeight₁ (x i / x j) ≤ logHeight x

The logarithmic height of a ratio of two coordinates is at most the height of the tuple.

theorem Height.logHeight₁_div_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] (x y : K) : logHeight₁ (x / y) ≤ logHeight₁ x + logHeight₁ y

The logarithmic height of a quotient is at most the sum of the logarithmic heights.

theorem Height.logHeight₁_div_le_of_mul_sub_mul_eq {K : Type u_1} [Field K] [AdmissibleAbsValues K] {θ₀ θ₂ x y t : K} (hθ : θ₀ ≠ θ₂) (ht : t * (x - θ₂ * y) = x - θ₀ * y) : logHeight₁ (x / y) ≤ 2 * logHeight₁ t + logHeight₁ θ₀ + logHeight₁ θ₂ + 2 * (↑(totalWeight K) * Real.log 2)

If t (x - θ₂ y) = x - θ₀ y with θ₀ ≠ θ₂, so that for y ≠ 0 x / y = (θ₀ - t θ₂) / (1 - t), then h(x / y) ≤ 2 h(t) + h(θ₀) + h(θ₂) + 2 totalWeight K log 2. For y = 0 the quotient is the field's totalized 0 and the bound is trivial.

theorem Height.mulHeight_eq_of_forall_eq_or_eq_neg {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {x y : ι → K} (h : ∀ (i : ι), y i = x i ∨ y i = -x i) : mulHeight y = mulHeight x

The multiplicative height is unchanged by changing the signs of some coordinates.

theorem Height.logHeight_eq_of_forall_eq_or_eq_neg {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {x y : ι → K} (h : ∀ (i : ι), y i = x i ∨ y i = -x i) : logHeight y = logHeight x

The logarithmic height is unchanged by changing the signs of some coordinates.

theorem Height.mulHeight_le_of_forall_iSup_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {ι' : Type u_3} [Finite ι'] {x : ι → K} (hx : x ≠ 0) (z : ι' → K) {C : ℝ} (hC : 1 ≤ C) {p : ℕ} (harch : ∀ v ∈ AdmissibleAbsValues.archAbsVal, ⨆ (i : ι'), v (z i) ≤ C * (⨆ (j : ι), v (x j)) ^ p) (hnon : ∀ v ∈ AdmissibleAbsValues.nonarchAbsVal, ⨆ (i : ι'), v (z i) ≤ (⨆ (j : ι), v (x j)) ^ p) : mulHeight z ≤ C ^ totalWeight K * mulHeight x ^ p

Local-to-global height bound. Suppose that at every archimedean absolute value v the local factor ⨆ i, v (z i) is at most C * (⨆ j, v (x j)) ^ p, and at every nonarchimedean one it is at most (⨆ j, v (x j)) ^ p. Then mulHeight z ≤ C ^ totalWeight K * mulHeight x ^ p.

theorem Height.ne_zero_of_forall_iSup_eq {K : Type u_1} [Field K] {ι : Type u_2} {ι' : Type u_3} {x : ι → K} {y : ι' → K} (hx : x ≠ 0) (h : ∀ (v : AbsoluteValue K ℝ), ⨆ (i : ι), v (x i) = ⨆ (i : ι'), v (y i)) : y ≠ 0

A tuple with the same local factor ⨆ i, v (x i) at every absolute value as a nonzero tuple is nonzero: the trivial absolute value sees a nonzero coordinate.

theorem Height.mulHeight_eq_of_forall_iSup_eq {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {ι' : Type u_3} {x : ι → K} {y : ι' → K} (h : ∀ (v : AbsoluteValue K ℝ), ⨆ (i : ι), v (x i) = ⨆ (i : ι'), v (y i)) : mulHeight x = mulHeight y

Two tuples with the same local factor ⨆ i, v (x i) at every absolute value have the same height.

theorem Height.mulHeight_le_pow_totalWeight {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] {x : ι → K} {C : ℝ} (hC : 1 ≤ C) (harch : ∀ v ∈ AdmissibleAbsValues.archAbsVal, ⨆ (i : ι), v (x i) ≤ C) (hnon : ∀ v ∈ AdmissibleAbsValues.nonarchAbsVal, ⨆ (i : ι), v (x i) ≤ 1) : mulHeight x ≤ C ^ totalWeight K

A tuple whose local factor ⨆ i, v (x i) is at most C at every archimedean absolute value and at most 1 at every nonarchimedean one has height at most C ^ totalWeight K.

theorem Height.mulHeight_natCast_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {n : ι → ℕ} {N : ℕ} (hN : 1 ≤ N) (hn : ∀ (i : ι), n i ≤ N) : (mulHeight fun (i : ι) => ↑(n i)) ≤ ↑N ^ totalWeight K

A tuple of natural numbers bounded by N ≥ 1 has height at most N ^ totalWeight K. The index type need not be finite: the tuple takes only finitely many values.

theorem Height.mulHeight_pow_range {K : Type u_1} [Field K] [AdmissibleAbsValues K] (α : K) (d : ℕ) : (mulHeight fun (k : Fin (d + 1)) => α ^ ↑k) = mulHeight₁ α ^ d

The tuple of powers α ^ k, 0 ≤ k ≤ d, has height exactly mulHeight₁ α ^ d: at every absolute value its local factor is max (v α) 1 ^ d.