Completed statement bridges for Salem’s theorem.
theorem
SalemTheorem.salem_theorem
(alpha : ℝ)
(halpha : 1 < alpha)
(hint : IsIntegral ℤ alpha)
(hpisot : ∀ z ∈ (minpoly ℚ alpha).aroots ℂ, z ≠ ↑alpha → ‖z‖ < 1)
(eps : ℝ)
(heps : 0 < eps)
:
(∃ (tau : ℝ),
(1 < tau ∧ IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0) ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (tau : ℝ),
(1 < tau ∧ IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0) ∧ alpha < tau ∧ tau < alpha + eps
Salem's theorem for Pisot numbers: transported through the
pattern data of minpoly ℤ α.
theorem
SalemTheorem.salem_construction_two_sided
(P : Polynomial ℤ)
(hmonic : P.Monic)
(alpha : ℝ)
(halpha : 1 < alpha)
(inside : Multiset ℂ)
(hin : ∀ z ∈ inside, ‖z‖ < 1)
(hconj : Multiset.map (⇑(starRingEnd ℂ)) inside = inside)
(hfac :
Polynomial.map (Int.castRingHom ℂ) P = (Polynomial.X - Polynomial.C ↑alpha) * (Multiset.map (fun (z : ℂ) => Polynomial.X - Polynomial.C z) inside).prod)
(hnd : Polynomial.eval alpha⁻¹ (Polynomial.map (Int.castRingHom ℝ) P) ≠ 0)
(eps : ℝ)
(heps : 0 < eps)
:
∃ (e : ℤ),
(e = 1 ∨ e = -1) ∧ 0 < ↑e * Polynomial.eval alpha⁻¹ (Polynomial.map (Int.castRingHom ℝ) P) ∧ (∃ (m : ℕ),
2 ≤ m ∧ ∃ (tau : ℝ),
(1 < tau ∧ IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0) ∧ Polynomial.eval tau
(Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * P + Polynomial.C e * P.reverse)) = 0 ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (m : ℕ),
2 ≤ m ∧ ∃ (tau : ℝ),
(1 < tau ∧ IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0) ∧ Polynomial.eval tau
(Polynomial.map (Int.castRingHom ℝ) (Polynomial.X ^ m * P - Polynomial.C e * P.reverse)) = 0 ∧ alpha < tau ∧ tau < alpha + eps
The main construction, with its family root.
theorem
SalemTheorem.salem_quadratic_unit
(r : ℤ)
(hr : 3 ≤ r)
(alpha : ℝ)
(halpha : 1 < alpha)
(hmin : alpha ^ 2 = ↑r * alpha - 1)
(eps : ℝ)
(heps : 0 < eps)
:
(∃ (m : ℕ),
1 ≤ m ∧ ∃ (tau : ℝ),
(1 < tau ∧ IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0) ∧ Polynomial.eval tau
(Polynomial.map (Int.castRingHom ℝ)
((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1) + Polynomial.X ^ (m + 1))) = 0 ∧ alpha - eps < tau ∧ tau < alpha) ∧ ∃ (m : ℕ),
1 ≤ m ∧ ∃ (tau : ℝ),
(1 < tau ∧ IsIntegral ℤ tau ∧ (∀ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 → z ≠ ↑tau → ‖z‖ ≤ 1) ∧ (∃ (z : ℂ), (Polynomial.aeval z) (minpoly ℚ tau) = 0 ∧ ‖z‖ = 1) ∧ (Polynomial.aeval (↑tau)⁻¹) (minpoly ℚ tau) = 0) ∧ Polynomial.eval tau
(Polynomial.map (Int.castRingHom ℝ)
((Polynomial.X ^ 2 - Polynomial.C r * Polynomial.X + 1) * (Polynomial.X ^ (2 * m) + 1) - Polynomial.X ^ (m + 1))) = 0 ∧ alpha < tau ∧ tau < alpha + eps
The reciprocal quadratic case, with its family root.