PdtPisotLadder — the general Pisot ladder

The general Pisot ladder — the analytic half of Salem's construction; Salem-ness of the roots is NOT proved here (that is PdtSalemArith).

For a real polynomial P = (X − C α)·G with α > 1 and G > 0 on [1, ∞) (so α is the unique root of P in [1, ∞)), and a companion polynomial Q, the family R_m = X^m·P + Q is studied on [c, α] and [α, ∞):

• the ladder (pisot_ladder_family): if 1 < c < α and Q > 0 on [c, α], then for m large the family R_m has a canonical root lam m ∈ (c, α), the largest root below α; the sequence is strictly increasing in m; and it tends to α;
• eventual positivity above α (pisot_ladder_pos_eventually): if moreover P is monic, Q(α) > 0 and natDegree Q ≤ natDegree P, then for m large R_m > 0 on all of [α, ∞) — uniformly in x. (Q may be negative somewhere above α, so the positivity is genuinely eventual in m.)

The proof skeleton: the scalar recurrence R_{m+1}(y) = y·R_m(y) + (1 − y)·Q(y), the endpoint identity R_m(α) = Q(α), base negativity by power blow-up, sSup root canonicity, the one-line monotone step, and the order-topology limit — plus the uniform tail bound for the second theorem (a coefficient-sum growth bound for Q against a positive lower bound for P on [s, ∞)).

Remark: in pisot_ladder_family the hypothesis halpha : 1 < alpha is mathematically redundant (it follows from hc : 1 < c and hca : c < alpha); it is kept for interface symmetry with pisot_ladder_pos_eventually, where it is essential.

Eval basics — the family at scalar level

theorem PDT.PisotLadder.eval_family (P Q : Polynomial ℝ) (m : ℕ) (x : ℝ) : Polynomial.eval x (Polynomial.X ^ m * P + Q) = x ^ m * Polynomial.eval x P + Polynomial.eval x Q

theorem PDT.PisotLadder.family_rec (P Q : Polynomial ℝ) (m : ℕ) (y : ℝ) : Polynomial.eval y (Polynomial.X ^ (m + 1) * P + Q) = y * Polynomial.eval y (Polynomial.X ^ m * P + Q) + (1 - y) * Polynomial.eval y Q

The scalar recurrence R_{m+1}(y) = y·R_m(y) + (1 − y)·Q(y).

Sign facts from the factorization P = (X − C α)·G

theorem PDT.PisotLadder.eval_P_eq (P G : Polynomial ℝ) (alpha : ℝ) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (x : ℝ) : Polynomial.eval x P = (x - alpha) * Polynomial.eval x G

theorem PDT.PisotLadder.eval_P_alpha (P G : Polynomial ℝ) (alpha : ℝ) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) : Polynomial.eval alpha P = 0

theorem PDT.PisotLadder.eval_P_neg (P G : Polynomial ℝ) (alpha : ℝ) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) {x : ℝ} (hx1 : 1 ≤ x) (hxa : x < alpha) : Polynomial.eval x P < 0

Below α (and at least 1), P is strictly negative.

theorem PDT.PisotLadder.family_at_alpha (P G Q : Polynomial ℝ) (alpha : ℝ) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (m : ℕ) : Polynomial.eval alpha (Polynomial.X ^ m * P + Q) = Polynomial.eval alpha Q

The endpoint identity: R_m(α) = Q(α) for every m.

theorem PDT.PisotLadder.family_at_alpha_pos (P G Q : Polynomial ℝ) (alpha : ℝ) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hQa : 0 < Polynomial.eval alpha Q) (m : ℕ) : 0 < Polynomial.eval alpha (Polynomial.X ^ m * P + Q)

Base negativity below α, for m large (power blow-up)

theorem PDT.PisotLadder.exists_eval_neg (P G Q : Polynomial ℝ) (alpha t : ℝ) (ht1 : 1 < t) (hta : t < alpha) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) : ∃ (M0 : ℕ), ∀ (m : ℕ), M0 ≤ m → Polynomial.eval t (Polynomial.X ^ m * P + Q) < 0

At any point t ∈ (1, α) the family is eventually negative in m: t^m·P(t) blows down past the fixed value Q(t).

The canonical root — sSup of the root set in [c, α]

def PDT.PisotLadder.rootSet (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) : Set ℝ

The roots of R_m in [c, α].

Equations

• PDT.PisotLadder.rootSet P Q alpha c m = {x : ℝ | x ∈ Set.Icc c alpha ∧ Polynomial.eval x (Polynomial.X ^ m * P + Q) = 0}

noncomputable def PDT.PisotLadder.lam (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) : ℝ

The canonical root: the largest root of R_m in [c, α].

Equations

• PDT.PisotLadder.lam P Q alpha c m = sSup (PDT.PisotLadder.rootSet P Q alpha c m)

theorem PDT.PisotLadder.rootSet_isCompact (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) : IsCompact (rootSet P Q alpha c m)

theorem PDT.PisotLadder.rootSet_nonempty (P Q : Polynomial ℝ) (alpha c : ℝ) (hca : c ≤ alpha) (m : ℕ) (hbase : Polynomial.eval c (Polynomial.X ^ m * P + Q) < 0) (hpos : 0 < Polynomial.eval alpha (Polynomial.X ^ m * P + Q)) : (rootSet P Q alpha c m).Nonempty

theorem PDT.PisotLadder.lam_mem (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) (hne : (rootSet P Q alpha c m).Nonempty) : lam P Q alpha c m ∈ rootSet P Q alpha c m

theorem PDT.PisotLadder.lam_gt_c (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) (hne : (rootSet P Q alpha c m).Nonempty) (hbase : Polynomial.eval c (Polynomial.X ^ m * P + Q) < 0) : c < lam P Q alpha c m

theorem PDT.PisotLadder.lam_lt_alpha (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) (hne : (rootSet P Q alpha c m).Nonempty) (hpos : 0 < Polynomial.eval alpha (Polynomial.X ^ m * P + Q)) : lam P Q alpha c m < alpha

theorem PDT.PisotLadder.lam_max (P Q : Polynomial ℝ) (alpha c : ℝ) (m : ℕ) (hne : (rootSet P Q alpha c m).Nonempty) {y : ℝ} (h1 : lam P Q alpha c m < y) (h2 : y < alpha) : Polynomial.eval y (Polynomial.X ^ m * P + Q) ≠ 0

Maximality: no roots of R_m strictly between lam m and α.

Strict monotonicity

theorem PDT.PisotLadder.family_succ_at_root (P Q : Polynomial ℝ) (m : ℕ) {y : ℝ} (h1 : 1 < y) (hQy : 0 < Polynomial.eval y Q) (hy : Polynomial.eval y (Polynomial.X ^ m * P + Q) = 0) : Polynomial.eval y (Polynomial.X ^ (m + 1) * P + Q) < 0

The heart: at a root of R_m, the next member is negative — R_{m+1}(y) = (1 − y)·Q(y) < 0 when y > 1 and Q(y) > 0.

theorem PDT.PisotLadder.lam_strictMono (P G Q : Polynomial ℝ) (alpha c : ℝ) (hc : 1 < c) (hca : c < alpha) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hQ : ∀ (x : ℝ), c ≤ x → x ≤ alpha → 0 < Polynomial.eval x Q) (m : ℕ) (hbase : Polynomial.eval c (Polynomial.X ^ m * P + Q) < 0) : lam P Q alpha c m < lam P Q alpha c (m + 1)

The limit

theorem PDT.PisotLadder.lam_tendsto (P G Q : Polynomial ℝ) (alpha c : ℝ) (hc : 1 < c) (hca : c < alpha) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQ : ∀ (x : ℝ), c ≤ x → x ≤ alpha → 0 < Polynomial.eval x Q) : Filter.Tendsto (fun (m : ℕ) => lam P Q alpha c m) Filter.atTop (nhds alpha)

The canonical roots tend to α: below any y < α the base negativity plus the intermediate value theorem plants a root above y eventually, and lam m < α always (for m past the base index).

The first theorem: the general Pisot ladder

theorem PDT.PisotLadder.pisot_ladder_family (P G Q : Polynomial ℝ) (alpha c : ℝ) (_halpha : 1 < alpha) (hc : 1 < c) (hca : c < alpha) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQ : ∀ (x : ℝ), c ≤ x → x ≤ alpha → 0 < Polynomial.eval x Q) : ∃ (M : ℕ) (lam : ℕ → ℝ), (∀ (m : ℕ), M ≤ m → (c < lam m ∧ lam m < alpha) ∧ Polynomial.eval (lam m) (Polynomial.X ^ m * P + Q) = 0 ∧ (∀ (y : ℝ), lam m < y → y < alpha → Polynomial.eval y (Polynomial.X ^ m * P + Q) ≠ 0) ∧ lam m < lam (m + 1)) ∧ Filter.Tendsto lam Filter.atTop (nhds alpha)

The general Pisot ladder. For P = (X − C α)·G with G > 0 on [1, ∞), and Q > 0 on [c, α] with 1 < c < α: for m large the family R_m = X^m·P + Q has a canonical root lam m ∈ (c, α), the largest root below α; the sequence is strictly increasing; and it tends to α.

halpha is derivable from hc and hca (see the module docstring); the hypothesis is retained for interface symmetry with the other ladder result.

Eventual uniform positivity on [α, ∞)

theorem PDT.PisotLadder.exists_window (Q : Polynomial ℝ) (alpha : ℝ) (hQa : 0 < Polynomial.eval alpha Q) : ∃ (s : ℝ), alpha < s ∧ ∀ x ∈ Set.Icc alpha s, 0 < Polynomial.eval x Q

The δ-window: Q(α) > 0 extends to a closed window [α, s] with α < s by continuity.

theorem PDT.PisotLadder.family_pos_on_window (P G Q : Polynomial ℝ) (alpha : ℝ) (halpha : 1 < alpha) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (s : ℝ) (hwin : ∀ x ∈ Set.Icc alpha s, 0 < Polynomial.eval x Q) (m : ℕ) {x : ℝ} (hx : x ∈ Set.Icc alpha s) : 0 < Polynomial.eval x (Polynomial.X ^ m * P + Q)

On the window [α, s] every member of the family is positive: x^m·P(x) ≥ 0 there and Q > 0 there.

theorem PDT.PisotLadder.P_natDegree_eq (P G : Polynomial ℝ) (alpha : ℝ) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hGne : G ≠ 0) : P.natDegree = 1 + G.natDegree

theorem PDT.PisotLadder.exists_eta (P G : Polynomial ℝ) (alpha : ℝ) (halpha : 1 < alpha) (hmonic : P.Monic) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) {s : ℝ} (hs : alpha < s) : ∃ (eta : ℝ), 0 < eta ∧ ∀ (x : ℝ), s ≤ x → eta ≤ Polynomial.eval x P

The uniform positive lower bound for P on [s, ∞), s > α: P → ∞ at infinity, and P is continuous and positive on the compact remainder.

theorem PDT.PisotLadder.abs_eval_le (Q : Polynomial ℝ) (x : ℝ) (hx : 1 ≤ x) : |Polynomial.eval x Q| ≤ (∑ i ∈ Finset.range (Q.natDegree + 1), |Q.coeff i|) * x ^ Q.natDegree

The coefficient-sum growth bound: for x ≥ 1, |Q(x)| ≤ (∑ |coeff|)·x^(natDegree Q).

The second theorem: eventual uniform positivity above α

theorem PDT.PisotLadder.pisot_ladder_pos_eventually (P G Q : Polynomial ℝ) (alpha : ℝ) (halpha : 1 < alpha) (hmonic : P.Monic) (hfac : P = (Polynomial.X - Polynomial.C alpha) * G) (hG : ∀ (x : ℝ), 1 ≤ x → 0 < Polynomial.eval x G) (hQa : 0 < Polynomial.eval alpha Q) (hdeg : Q.natDegree ≤ P.natDegree) : ∃ (M : ℕ), ∀ (m : ℕ), M ≤ m → ∀ (x : ℝ), alpha ≤ x → 0 < Polynomial.eval x (Polynomial.X ^ m * P + Q)

Eventual uniform positivity on [α, ∞). For monic P = (X − C α)·G with G > 0 on [1, ∞), Q(α) > 0, and natDegree Q ≤ natDegree P: for m large, R_m = X^m·P + Q is strictly positive on all of [α, ∞). Near α the window positivity of Q carries every member; past the window the term x^m·P(x) dominates the coefficient-sum bound on |Q(x)| once m ≥ natDegree P + K with s^K·η > ∑|coeff Q|.