Documentation

TauCeti.NumberTheory.Height.LinearForm

Heights of values of linear forms and of determinants #

The value ∑ i, a i * x i of a linear form and the determinant of a matrix are not homogeneous of degree zero in their arguments: scaling the coefficient tuple a by c multiplies the value by c but leaves the projective height Height.mulHeight a unchanged. So no bound on the height of such a value in terms of projective heights can hold (Height.exists_not_mulHeight₁_det_le records this for determinants). The bounds that do hold use the affine height Height.mulHeightAff, whose local factor at a place v is max (⨆ i, v (x i)) 1.

The affine bounds come from one estimate, Height.mulHeight₁_sum_le_prod_mulHeightAff: if every term of a finite sum is bounded, at every absolute value, by the product of the affine local factors of a fixed family of tuples, then the height of the sum is at most #s ^ totalWeight K times the product of the affine heights of the tuples. The factor #s is paid only at the archimedean places; at the nonarchimedean places the ultrametric inequality makes it disappear. It is in turn an instance of the local-to-global bound Height.mulHeight₁_le_pow_mul_prod_mulHeightAff: local bounds by C times the affine local factors at the archimedean places, and by the affine local factors alone at the nonarchimedean places, give the height bound with constant C ^ totalWeight K.

A scale-invariant alternative divides a product of coordinates by the linear-form value: Height.mulHeight₁_mul_div_sum_mul_le bounds the height of a i * x j / ∑ k, a k * x k by card ι ^ totalWeight K * H(a) * H(x). At a number-field place, this gives local Liouville bounds comparing the product of the sup norms of a and x with the absolute value of the form. At an infinite place both local quantities are raised to its multiplicity. The same global constant is necessary even at a finite place, since the height still uses the infinite places. These bounds compare local factors of Plücker coordinates with their projective height in height estimates for subspaces.

Main results #

Implementation notes #

The global step needs the finiteness of the multiplicative support of the nonarchimedean local factors max (v x) 1 of Height.mulHeight₁, which Mathlib proves by the private fun_prop lemma Height.hasFiniteMulSupport_max_nonarchAbsVal in Mathlib/NumberTheory/Height/Basic.lean; it is reached by import all, as Mathlib's own Mathlib/NumberTheory/Height/MvPolynomial.lean does. The affine counterpart is the public Height.hasFiniteMulSupport_max_iSup_nonarchAbsVal.

References #

source
theorem Height.mulHeight₁_le_pow_mul_prod_mulHeightAff {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {κ : Type u_3} [Fintype κ] [Finite ι] {C : ℝ} (hC : 1 ≤ C) (z : K) (y : κ → ι → K) (harch : ∀ v ∈ AdmissibleAbsValues.archAbsVal, v z ≤ C * ∏ k : κ, max (⨆ (i : ι), v (y k i)) 1) (hnonarch : ∀ v ∈ AdmissibleAbsValues.nonarchAbsVal, v z ≤ ∏ k : κ, max (⨆ (i : ι), v (y k i)) 1) :
mulHeight₁ z ≤ C ^ totalWeight K * ∏ k : κ, mulHeightAff (y k)

Local-to-global bound. Let y : κ → ι → K be a finite family of tuples and C ≥ 1. If v z ≤ C * ∏ k, max (⨆ i, v (y k i)) 1 at every archimedean absolute value v and v z ≤ ∏ k, max (⨆ i, v (y k i)) 1 at every nonarchimedean one, then the height of z is at most C ^ totalWeight K times the product of the affine heights of the tuples y k.

source
theorem Height.mulHeight₁_sum_le_prod_mulHeightAff {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} {α : Type u_3} {κ : Type u_4} [Fintype κ] [Finite ι] {s : Finset α} (hs : s.Nonempty) (t : α → K) (y : κ → ι → K) (ht : ∀ (v : AbsoluteValue K ℝ), ∀ a ∈ s, v (t a) ≤ ∏ k : κ, max (⨆ (i : ι), v (y k i)) 1) :
mulHeight₁ (∑ a ∈ s, t a) ≤ ↑s.card ^ totalWeight K * ∏ k : κ, mulHeightAff (y k)

Local-to-global bound for sums. Let y : κ → ι → K be a finite family of tuples, and let every term t a, a ∈ s, of a nonempty finite sum satisfy v (t a) ≤ ∏ k, max (⨆ i, v (y k i)) 1 at every absolute value v. Then the height of the sum is at most #s ^ totalWeight K times the product of the affine heights of the tuples y k.

The value of a linear form #

source
theorem Height.mulHeight₁_sum_mul_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [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 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.

The heights on the right have to be affine: scaling a by c multiplies the value by c and leaves the projective height mulHeight a unchanged. The constant is attained over ℚ (Height.exists_mulHeight₁_sum_mul_eq).

source
theorem Height.logHeight₁_sum_mul_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Fintype ι] (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. It needs no nonemptiness hypothesis, thanks to the junk value log 0 = 0.

source
theorem Height.exists_mulHeight₁_sum_mul_eq {ι : Type u_2} [Fintype ι] [Nonempty ι] :
∃ (a : ι → ℚ) (x : ι → ℚ), mulHeight₁ (∑ i : ι, a i * x i) = ↑(Nat.card ι) ^ totalWeight ℚ * (mulHeightAff a * mulHeightAff x)

The constant of Height.mulHeight₁_sum_mul_le is sharp. Over ℚ, for every nonempty finite ι, the tuples a = x = 1 have affine height 1 while the value ∑ i, a i * x i is Nat.card ι, of height Nat.card ι = Nat.card ι ^ totalWeight ℚ.

source
theorem Height.mulHeight₁_mul_div_sum_mul_le {K : Type u_1} [Field K] [AdmissibleAbsValues K] {ι : Type u_2} [Fintype ι] (a x : ι → K) (i j : ι) :
mulHeight₁ (a i * x j / ∑ k : ι, a k * x k) ≤ ↑(Fintype.card ι) ^ totalWeight K * (mulHeight a * mulHeight x)

The height of a product of two coordinates divided by the value of the corresponding linear form is at most card ι ^ totalWeight K times the product of the projective heights. The denominator may vanish, with division interpreted as totalized division.

Local Liouville bounds #

source
theorem NumberField.InfinitePlace.iSup_mul_iSup_pow_mult_le {K : Type u_1} {ι : Type u_2} [Field K] [NumberField K] [Fintype ι] (v : InfinitePlace K) (a x : ι → K) (hz : ∑ i : ι, a i * x i ≠ 0) :
((⨆ (i : ι), v (a i)) * ⨆ (i : ι), v (x i)) ^ v.mult ≤ ↑(Fintype.card ι) ^ Module.finrank ℚ K * (Height.mulHeight a * Height.mulHeight x) * v (∑ i : ι, a i * x i) ^ v.mult

Local Liouville inequality for a linear form at an infinite place. The product of the two local sup norms, raised to v.mult, is bounded by the local value of the form raised to v.mult, times card ι ^ [K : ℚ] and the product of the projective heights. The constant and the projective heights are not raised to v.mult.

source
theorem NumberField.FinitePlace.iSup_mul_iSup_le {K : Type u_1} {ι : Type u_2} [Field K] [NumberField K] [Fintype ι] (v : FinitePlace K) (a x : ι → K) (hz : ∑ i : ι, a i * x i ≠ 0) :
(⨆ (i : ι), v (a i)) * ⨆ (i : ι), v (x i) ≤ ↑(Fintype.card ι) ^ Module.finrank ℚ K * (Height.mulHeight a * Height.mulHeight x) * v (∑ i : ι, a i * x i)

Local Liouville inequality for a linear form at a finite place. The constant card ι ^ [K : ℚ] remains present, since the global height still uses the infinite places.

The determinant #

source
theorem Matrix.mulHeight₁_det_le {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n K) :
Height.mulHeight₁ A.det ≤ ↑(Nat.card n).factorial ^ Height.totalWeight K * ∏ j : n, Height.mulHeightAff fun (i : n) => A i j

The height of a determinant. The height of A.det is at most (Nat.card n)! ^ totalWeight K times the product of the affine heights of the columns of A. This is the Leibniz expansion: the determinant is a sum of (Nat.card n)! signed products, each taking one entry from every column.

The heights of the columns have to be affine: A ↦ c • A fixes the projective height of the entries and multiplies the determinant by c ^ Nat.card n (see Height.exists_not_mulHeight₁_det_le).

source
theorem Matrix.logHeight₁_det_le {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n K) :
Height.logHeight₁ A.det ≤ ↑(Height.totalWeight K) * Real.log ↑(Nat.card n).factorial + ∑ j : n, Height.logHeightAff fun (i : n) => A i j

The logarithmic form of Matrix.mulHeight₁_det_le.

source
theorem Matrix.mulHeight₁_det_le_mulHeightAff_pow {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n K) :
Height.mulHeight₁ A.det ≤ ↑(Nat.card n).factorial ^ Height.totalWeight K * (Height.mulHeightAff fun (p : n × n) => A p.1 p.2) ^ Nat.card n

The height of a determinant against the affine height of the tuple of all entries: mulHeight₁ A.det ≤ (Nat.card n)! ^ totalWeight K * mulHeightAff (entries A) ^ Nat.card n.

source
theorem Matrix.logHeight₁_det_le_logHeightAff {K : Type u_1} [Field K] [Height.AdmissibleAbsValues K] {n : Type u_2} [Fintype n] [DecidableEq n] (A : Matrix n n K) :
Height.logHeight₁ A.det ≤ ↑(Height.totalWeight K) * Real.log ↑(Nat.card n).factorial + ↑(Nat.card n) * Height.logHeightAff fun (p : n × n) => A p.1 p.2

The logarithmic form of Matrix.mulHeight₁_det_le_mulHeightAff_pow.

source
theorem Height.exists_not_mulHeight₁_det_le (C : ℝ) :
∃ (A : Matrix (Fin 1) (Fin 1) ℚ), ¬mulHeight₁ A.det ≤ C * mulHeight fun (p : Fin 1 × Fin 1) => A p.1 p.2

The determinant is not bounded by the projective height of the entries. For every constant C some 1 × 1 matrix over ℚ violates mulHeight₁ A.det ≤ C * mulHeight (entries A): a single entry has projective height 1, while the determinant is that entry. This is why Matrix.mulHeight₁_det_le uses affine heights.

Examples #