Theorems · Theorem · number theory

Height.logHeight_eval_le

∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K},
  (∀ (i : ι'), (p i).IsHomogeneous N) →
    ∀ (x : ι → K),
      (Height.logHeight fun j => (MvPolynomial.eval x) (p j)) ≤
        Real.log (max (Height.mulHeightBound p) 1) + ↑N * Height.logHeight x

Let K be a field with an admissible family of absolute values (giving rise to a logarithmic height). Let p be a family (indexed by ι') of homogeneous polynomials in variables indexed by the finite type ι and of the same degree N. Then for any x : ι → K, the logarithmic height of fun j : ι' ↦ eval x (p j) is bounded by a constant (which is made explicit) plus N * logHeight x.

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldHeight.AdmissibleAbsValuesFiniteFinite