Heights of finitely supported coefficient vectors

The native Finsupp.mulHeight is a projective height on the nonzero support. This module identifies it with finite tuples containing that support, and proves invariance under scalar multiplication and injective reindexing. These interfaces allow polynomial coefficient heights to use the finite-tuple height estimates in Mathlib.

Finsupp.mulHeight_eq_mul_of_injOn transfers Mathlib's Segre relation Height.mulHeight_fun_mul_eq to finitely supported vectors: a vector whose nonzero entries are exactly the products x a * y b, each occurring once, has the product of the heights of x and y. The coefficients of a product of polynomials in disjoint sets of variables have this form.

References

• The multiplication-table height follows DiophantineApproximation/DisjointVariables.lean in Ralf Stephan's rwst/Subspace-Theorems, snapshot c26d909dc48cf7fe (Apache 2.0).

theorem Finsupp.mulHeight_eq_of_support_subset {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) (s : Finset α) (hs : x.support ⊆ s) : x.mulHeight = Height.mulHeight fun (i : ↥s) => x ↑i

Padding a finitely supported coefficient vector by zeroes does not change its height.

@[simp]

theorem Finsupp.mulHeight_zero {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] : mulHeight 0 = 1

@[simp]

theorem Finsupp.logHeight_zero {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] : logHeight 0 = 0

theorem Finsupp.one_le_mulHeight {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) : 1 ≤ x.mulHeight

theorem Finsupp.mulHeight_pos {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) : 0 < x.mulHeight

theorem Finsupp.mulHeight_eq_mulHeight_coe {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) : x.mulHeight = Height.mulHeight ⇑x

The full coefficient function and its nonzero support have the same projective height, even when the index type is infinite.

theorem Finsupp.logHeight_eq_log_mulHeight_support {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) : x.logHeight = Real.log x.mulHeight

The native logarithmic Finsupp height is the logarithm of its support height. Mathlib's native characteristic equation uses Height.mulHeight ⇑x; this bridge uses Finsupp.mulHeight x, the height on the finite support.

theorem Finsupp.logHeight_nonneg {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) : 0 ≤ x.logHeight

@[simp]

theorem Finsupp.mulHeight_single {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : α) (c : K) : (single i c).mulHeight = 1

A coefficient vector supported at one index has projective height one.

@[simp]

theorem Finsupp.logHeight_single {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (i : α) (c : K) : (single i c).logHeight = 0

@[simp]

theorem Finsupp.mulHeight_smul {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) {c : K} (hc : c ≠ 0) : (c • x).mulHeight = x.mulHeight

Multiplication by a nonzero scalar preserves projective coefficient height.

@[simp]

theorem Finsupp.logHeight_smul {K : Type u_1} {α : Type u_2} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) {c : K} (hc : c ≠ 0) : (c • x).logHeight = x.logHeight

@[simp]

theorem Finsupp.mulHeight_embDomain {K : Type u_1} {α : Type u_2} {β : Type u_3} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) (f : α ↪ β) : (embDomain f x).mulHeight = x.mulHeight

Injective reindexing preserves the height of a finitely supported coefficient vector.

@[simp]

theorem Finsupp.logHeight_embDomain {K : Type u_1} {α : Type u_2} {β : Type u_3} [Field K] [Height.AdmissibleAbsValues K] (x : α →₀ K) (f : α ↪ β) : (embDomain f x).logHeight = x.logHeight

theorem Finsupp.mulHeight_eq_mul_of_injOn {K : Type u_1} {α : Type u_2} {β : Type u_3} [Field K] [Height.AdmissibleAbsValues K] {γ : Type u_4} {x : α →₀ K} {y : β →₀ K} {z : γ →₀ K} {e : α × β → γ} (he : Set.InjOn e ↑(x.support ×ˢ y.support)) (hz : ∀ a ∈ x.support, ∀ b ∈ y.support, z (e (a, b)) = x a * y b) (hsupp : ∀ c ∈ z.support, ∃ a ∈ x.support, ∃ b ∈ y.support, e (a, b) = c) (hx : x ≠ 0) (hy : y ≠ 0) : z.mulHeight = x.mulHeight * y.mulHeight

The height of a multiplication table. Suppose that e is injective on pairs of indices in the supports of x and y, that z (e (a, b)) = x a * y b for such pairs, and that every index in the support of z is of this form. If x and y are nonzero, then the height of z is the product of the heights of x and y. This is the Segre relation Height.mulHeight_fun_mul_eq for finitely supported vectors.

theorem Finsupp.logHeight_eq_add_of_injOn {K : Type u_1} {α : Type u_2} {β : Type u_3} [Field K] [Height.AdmissibleAbsValues K] {γ : Type u_4} {x : α →₀ K} {y : β →₀ K} {z : γ →₀ K} {e : α × β → γ} (he : Set.InjOn e ↑(x.support ×ˢ y.support)) (hz : ∀ a ∈ x.support, ∀ b ∈ y.support, z (e (a, b)) = x a * y b) (hsupp : ∀ c ∈ z.support, ∃ a ∈ x.support, ∃ b ∈ y.support, e (a, b) = c) (hx : x ≠ 0) (hy : y ≠ 0) : z.logHeight = x.logHeight + y.logHeight

The logarithmic height of a multiplication table. Under the hypotheses of Finsupp.mulHeight_eq_mul_of_injOn, the logarithmic height of z is the sum of the logarithmic heights of x and y.