The house of a polynomial expression in an algebraic number #
If every complex conjugate of γ is, up to the factor s ^ d, the value of an integer polynomial
P of degree d at the corresponding conjugate of g, then the house of γ is bounded by the
coefficient sup norm of P, a bound on the conjugates of g, and s.
Main results #
NumberField.house_le_of_norm_embedding_eq: the boundhouse γ ≤ s ^ n * ((n + 1) * R ^ n) * H(P).
theorem
NumberField.house_le_of_norm_embedding_eq
{F : Type u_1}
[Field F]
[NumberField F]
{g γ : F}
{R : ℝ}
(hR : ∀ (σ : F →+* ℂ), max 1 ‖σ g‖ ≤ R)
{s : ℝ}
(hs1 : 1 ≤ s)
{n : ℕ}
{P : Polynomial ℤ}
(hP : P.natDegree ≤ n)
(hγ : ∀ (σ : F →+* ℂ), ‖σ γ‖ = s ^ P.natDegree * ‖(Polynomial.aeval (σ g)) P‖)
:
If every conjugate σ γ of γ has absolute value s ^ d * ‖P(σ g)‖, where 1 ≤ s and P has
degree d ≤ n, and max 1 ‖σ g‖ ≤ R for every conjugate, then the house of γ is at most
s ^ n * ((n + 1) * R ^ n) * H(P).