Theorems · Theorem · number theory

Height.logHeight_eval_ge

∀ {K : Type u_6} [inst : Field K] {ι : Type u_7} {ι' : Type u_8} [inst_1 : Fintype ι']
  [inst_2 : Height.AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K},
  (∀ (a : ι × ι'), (q a).IsHomogeneous M) →
    ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
      (∀ (k : ι), ∑ j, (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) →
        -Real.log (↑(Nat.card ι') ^ Height.totalWeight K * max (Height.mulHeightBound q) 1) + ↑N * Height.logHeight x ≤
          Height.logHeight fun j => (MvPolynomial.eval x) (p j)

If * p : ι' → MvPolynomial ι K is a family of polynomials (which in practice will be homogeneous of the same degree N), * q : ι × ι' → MvPolynomial ι K is a family of homogeneous polynomials of the same degree M, * x : ι → K is such that for all k : ι, ∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N), then the logarithmic height of fun j ↦ (p j).eval x is bounded below by an (explicit) constant depending only on q plus N times the logarithmic height of 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

FieldFintypeHeight.AdmissibleAbsValuesFinite