Theorems · Theorem · number theory

Height.logHeight_linearMap_apply_le

∀ {K : Type u_1} [inst : Field K] {ι : Type u_2} {ι' : Type u_3} [inst_1 : Fintype ι] [Finite ι']
  [inst_3 : Height.AdmissibleAbsValues K] (A : ι' × ι → K) (x : ι → K),
  (Height.logHeight fun j => ∑ i, A (j, i) * x i) ≤
    ↑(Height.totalWeight K) * Real.log ↑(Nat.card ι) + Height.logHeight A + Height.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.)

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

0 results in Mathlib

Foundations

Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFintypeFiniteHeight.AdmissibleAbsValues