Linear forms, sums of coordinates, and the Segre relation

Mathlib bounds the height of a sum of field elements, Height.mulHeight₁_sum_le, with the constant #s ^ totalWeight K, and the height of the image of a tuple under a linear map, Height.mulHeight_linearMap_apply_le, with the constant Nat.card ι ^ totalWeight K. It also has the Segre relation Height.mulHeight_fun_mul_eq, that the height of the multiplication table fun (i, j) ↦ x i * y j is the product of the heights. This file adds the two statements about linear forms that those leave open, and the Arakelov form of the second.

The first is the tuple sum bound: if every term of a sum is an entry of one and the same tuple w, read off along index maps, then the height of the tuple of sums exceeds mulHeight w by at most #s ^ totalWeight K — a single height on the right, not a product of heights of the terms. This is what Height.mulHeight₁_sum_le cannot say, and it is the form an iteration needs, since it costs one additive totalWeight K * log #s per step rather than a multiplicative factor.

The second is the value of a linear form, ∑ i, a i * x i. Its projective height is not bounded by the projective heights of a and x in any way: scaling a by c multiplies the value by c and leaves mulHeight a fixed. The bound that is true replaces both by the affine height Height.mulHeightAff of Layer 0.5, and then the constant is again Nat.card ι ^ totalWeight K. Both are deduced here from the tuple sum bound and the Segre relation, applied to the multiplication table of the two affine tuples.

Finally, in the Arakelov normalization of ArithmeticHeights.Arakelov — the ℓ² norm at the archimedean places — the constant disappears: Cauchy–Schwarz at each infinite place gives NumberField.arakelovMulHeight_linearMap_apply_le with constant 1, against Nat.card ι ^ totalWeight K for the sup norm. This is the first place in the development where the Arakelov normalization is strictly better and not merely different.

Main results

• Height.mulHeight_sum_comp_le and Height.logHeight_sum_comp_le: the tuple sum bound, with the constant #s ^ totalWeight K; Height.mulHeight_sum_comp_le' is the version whose index set of summation may depend on the coordinate.
• Height.mulHeight₁_sum_mul_le and Height.logHeight₁_sum_mul_le: the value of a linear form against the affine heights of its coefficients and of the point, with the constant Nat.card ι ^ totalWeight K.
• Height.exists_not_mulHeight_add_le: the naive tuple analogue of Height.mulHeight₁_sum_le is false over ℚ, for every constant.
• NumberField.arakelovMulHeight_linearMap_apply_le and NumberField.arakelovLogHeight_linearMap_apply_le: the Arakelov height of the image of a tuple under a linear map, with constant 1.

Implementation notes

The local halves are separated out as AbsoluteValue.iSup_abv_sum_comp_le' and IsNonarchimedean.iSup_abv_sum_comp_le', following Mathlib's AbsoluteValue.iSup_abv_linearMap_apply_le, so that the archimedean cost #s and its disappearance at the nonarchimedean places are visible before any global product is formed.

The global step needs Height.hasFiniteMulSupport_iSup_nonarchAbsVal, which is private in Mathlib/NumberTheory/Height/Basic.lean; it is reached by import all, the way Mathlib's own Mathlib/NumberTheory/Height/MvPolynomial.lean reaches it. It should be public upstream.

The affine height is a normalization and not a theorem about linear forms, so it lives in Layer 0.5, ArithmeticHeights.Affine, and not here. What this file uses of it is that it is not invariant under scaling — Height.exists_mulHeightAff_smul_ne — which is why it and not Height.mulHeight can appear on the right of a bound on a linear form's value.

The Arakelov bound is stated for a number field because Height.AdmissibleAbsValues records no archimedean structure — no inner product at an archimedean place, hence no Cauchy–Schwarz.

References

E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Proposition 1.5.15 and 1.5.14 for the sum bound and the Segre relation, and Definition 2.8.1 for the Arakelov normalization used here.

This is Layer 2.4 of the ArithmeticHeights roadmap.

theorem AbsoluteValue.iSup_abv_sum_comp_le' {K : Type u_1} [Field K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Nonempty ι] [Finite κ] (v : AbsoluteValue K ℝ) {n : ℕ} {s : ι → Finset α} (hs : ∀ (i : ι), (s i).card ≤ n) (f : α → ι → κ) (w : κ → K) : ⨆ (i : ι), v (∑ a ∈ s i, w (f a i)) ≤ ↑n * ⨆ (k : κ), v (w k)

The local form of the tuple sum bound at an arbitrary absolute value, with the index set of the sum allowed to depend on the coordinate: if every sum has at most n terms, then the supremum of v over the entries of fun i ↦ ∑ a ∈ s i, w (f a i) is at most n times the supremum of v over the entries of w.

theorem AbsoluteValue.iSup_abv_sum_comp_le {K : Type u_1} [Field K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Nonempty ι] [Finite κ] (v : AbsoluteValue K ℝ) (s : Finset α) (f : α → ι → κ) (w : κ → K) : ⨆ (i : ι), v (∑ a ∈ s, w (f a i)) ≤ ↑s.card * ⨆ (k : κ), v (w k)

The local form of the tuple sum bound at an arbitrary absolute value.

theorem IsNonarchimedean.iSup_abv_sum_comp_le' {K : Type u_1} [Field K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Nonempty ι] [Finite κ] {v : AbsoluteValue K ℝ} (hv : IsNonarchimedean ⇑v) (s : ι → Finset α) (f : α → ι → κ) (w : κ → K) : ⨆ (i : ι), v (∑ a ∈ s i, w (f a i)) ≤ ⨆ (k : κ), v (w k)

The local form of the tuple sum bound at a nonarchimedean absolute value: there the factor #s disappears, because the absolute value of a sum is bounded by the maximum of the absolute values of its terms.

theorem IsNonarchimedean.iSup_abv_sum_comp_le {K : Type u_1} [Field K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Nonempty ι] [Finite κ] {v : AbsoluteValue K ℝ} (hv : IsNonarchimedean ⇑v) (s : Finset α) (f : α → ι → κ) (w : κ → K) : ⨆ (i : ι), v (∑ a ∈ s, w (f a i)) ≤ ⨆ (k : κ), v (w k)

The local form of the tuple sum bound at a nonarchimedean absolute value.

The height of a tuple of sums of entries of a single tuple

theorem Height.mulHeight_sum_comp_le' {K : Type u_1} [Field K] [AdmissibleAbsValues K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Finite ι] [Finite κ] {n : ℕ} (hn : 0 < n) {s : ι → Finset α} (hs : ∀ (i : ι), (s i).card ≤ n) (f : α → ι → κ) (w : κ → K) : (mulHeight fun (i : ι) => ∑ a ∈ s i, w (f a i)) ≤ ↑n ^ totalWeight K * mulHeight w

The tuple sum bound, with the index set of summation allowed to depend on the coordinate. If every term of the sum is an entry of one and the same tuple w : κ → K, read off along index maps f a : ι → κ, and every sum has at most n terms, then the height of the resulting tuple exceeds that of w by at most n ^ totalWeight K.

Contrast Height.mulHeight₁_sum_le, whose right-hand side is a product of the heights of the terms; here a single mulHeight w suffices, which is what makes an iteration cost an additive rather than a multiplicative constant per step.

theorem Height.mulHeight_sum_comp_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Finite ι] [Finite κ] {s : Finset α} (hs : s.Nonempty) (f : α → ι → κ) (w : κ → K) : (mulHeight fun (i : ι) => ∑ a ∈ s, w (f a i)) ≤ ↑s.card ^ totalWeight K * mulHeight w

The tuple sum bound, all the sums over the same index set.

theorem Height.logHeight_sum_comp_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {α : Type u_2} {ι : Type u_3} {κ : Type u_4} [Finite ι] [Finite κ] {s : Finset α} (hs : s.Nonempty) (f : α → ι → κ) (w : κ → K) : (logHeight fun (i : ι) => ∑ a ∈ s, w (f a i)) ≤ ↑(totalWeight K) * Real.log ↑s.card + logHeight w

The logarithmic form of Height.mulHeight_sum_comp_le.

The value of a linear form

theorem Height.mulHeight₁_sum_mul_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_3} [Fintype ι] [Nonempty ι] (a x : ι → K) : mulHeight₁ (∑ i : ι, a i * x i) ≤ ↑(Nat.card ι) ^ totalWeight K * (mulHeightAff a * mulHeightAff x)

The height of the value of a linear form. The affine height of ∑ i, a i * x i is at most Nat.card ι ^ totalWeight K times the product of the affine heights of the coefficient tuple a and of the point x.

Both heights on the right have to be affine: scaling a by c multiplies the value by c and leaves mulHeight a unchanged, so with projective heights the statement is false for every constant.

The proof is the Segre relation Height.mulHeight_fun_mul_eq applied to the multiplication table of the two affine tuples, followed by Height.mulHeight_sum_comp_le': the pair ![∑ i, a i * x i, 1] reads off Nat.card ι entries of that table in its first coordinate and a single entry in its second.

theorem Height.logHeight₁_sum_mul_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_3} [Fintype ι] [Nonempty ι] (a x : ι → K) : logHeight₁ (∑ i : ι, a i * x i) ≤ ↑(totalWeight K) * Real.log ↑(Nat.card ι) + (logHeightAff a + logHeightAff x)

The logarithmic form of Height.mulHeight₁_sum_mul_le.

The naive tuple analogue of the sum bound is false

theorem Height.not_mulHeight_add_le_of_lt_mulHeight₁ {K : Type u_1} [Field K] [AdmissibleAbsValues K] {x : K} (hx : 2 ^ totalWeight K < mulHeight₁ x) : ¬mulHeight (![x, 0] + ![0, 1]) ≤ 2 ^ totalWeight K * (mulHeight ![x, 0] * mulHeight ![0, 1])

Any field element whose height exceeds 2 ^ totalWeight K refutes the tuple analogue of Height.mulHeight₁_sum_le: the two tuples ![x, 0] and ![0, 1] both have height 1, while their sum ![x, 1] has height mulHeight₁ x. The mechanism is scaling invariance (Height.mulHeight_smul_eq_mulHeight), which the left-hand side of such a bound does not enjoy, so no choice of constant can repair the statement.

theorem Height.exists_not_mulHeight_add_le : ∃ (x : ℚ), ¬mulHeight (![x, 0] + ![0, 1]) ≤ 2 ^ totalWeight ℚ * (mulHeight ![x, 0] * mulHeight ![0, 1])

The tuple analogue of Height.mulHeight₁_sum_le fails already over ℚ. This is why the right-hand side of Height.mulHeight₁_sum_mul_le is stated with affine heights, and why Height.mulHeight_sum_comp_le reads off all its summands from one tuple.

Linear maps in the Arakelov normalization

At an infinite place the local factor of the Arakelov height is an ℓ² norm, so Cauchy–Schwarz bounds the local factor of A x by the product of those of A and x with no constant at all; at a finite place the sup norm does the same, by the ultrametric inequality. The constant Nat.card ι ^ totalWeight K of Height.mulHeight_linearMap_apply_le therefore disappears.

theorem NumberField.arakelovMulHeight_linearMap_apply_le {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Fintype ι'] (A : ι' × ι → K) (x : ι → K) : (arakelovMulHeight fun (j : ι') => ∑ i : ι, A (j, i) * x i) ≤ arakelovMulHeight A * arakelovMulHeight x

The Arakelov height of the image of a tuple under a linear map, with constant 1. Let A : ι' × ι → K, read as a linear map from ι → K to ι' → K. Then

arakelovMulHeight (A x) ≤ arakelovMulHeight A * arakelovMulHeight x.

Mathlib's sup-norm statement Height.mulHeight_linearMap_apply_le carries the constant Nat.card ι ^ totalWeight K, which cannot be removed there — the affine form of that is the second example at the end of this file; here Cauchy–Schwarz at each infinite place removes it. No hypothesis on A or x is needed: the junk value arakelovMulHeight 0 = 1 is at most the right-hand side, which is at least 1.

theorem NumberField.arakelovLogHeight_linearMap_apply_le {K : Type u_1} [Field K] [NumberField K] {ι : Type u_2} {ι' : Type u_3} [Fintype ι] [Fintype ι'] (A : ι' × ι → K) (x : ι → K) : (arakelovLogHeight fun (j : ι') => ∑ i : ι, A (j, i) * x i) ≤ arakelovLogHeight A + arakelovLogHeight x

The logarithmic form of NumberField.arakelovMulHeight_linearMap_apply_le: in the Arakelov normalization a linear map costs nothing beyond the heights of the matrix and of the point.

Examples

The tests that fix the constants: that #s ^ totalWeight K in the tuple sum bound and Nat.card ι ^ totalWeight K in the linear-form bound are attained over ℚ, and that the Arakelov constant 1 is attained too.