Pisot–Vijayaraghavan numbers

A Pisot–Vijayaraghavan number (or PV number) is a real algebraic integer θ > 1 all of whose Galois conjugates other than θ itself lie strictly inside the complex unit disc. Equivalently, every root in ℂ of the minimal polynomial of θ over ℚ, apart from θ, has modulus < 1.

References:

• Wikipedia, Pisot–Vijayaraghavan number

Main definitions

• IsPisot: a real number is a Pisot–Vijayaraghavan number.

Main statements

• isPisot_goldenRatio: the golden ratio is a Pisot number.

def IsPisot (θ : ℝ) : Prop

A Pisot–Vijayaraghavan number is a real algebraic integer θ > 1 all of whose other conjugates lie strictly inside the complex unit disc: every root in ℂ of the minimal polynomial of θ over ℚ, except θ itself, has modulus < 1.

Equations

• IsPisot θ = (1 < θ ∧ IsIntegral ℤ θ ∧ ∀ z ∈ (minpoly ℚ θ).aroots ℂ, z ≠ ↑θ → ‖z‖ < 1)

theorem isPisot_goldenRatio : IsPisot Real.goldenRatio

The golden ratio φ = (1 + √5) / 2 is a Pisot number: it is an algebraic integer greater than 1, its minimal polynomial over ℚ is X ^ 2 - X - 1, and its only other conjugate ψ = (1 - √5) / 2 has modulus (√5 - 1) / 2 < 1.