Theorems · Theorem · number theory

Height.mulHeight_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)) →
        (↑(Nat.card ι') ^ Height.totalWeight K * max (Height.mulHeightBound q) 1)⁻¹ * Height.mulHeight x ^ N ≤
          Height.mulHeight 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 multiplicative height of fun j ↦ (p j).eval x is bounded below by an (explicit) positive constant depending only on q times the Nth power of the multiplicative height of x.

Defined in

Mathlib.NumberTheory.Height.MvPolynomial

Cited by

2 results in Mathlib

Foundations

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

Assumes

FieldFintypeHeight.AdmissibleAbsValuesFinite