Dominant roots and reciprocal sums of recurrences

TheoremEneström–Kakeya theorem#●ready to prove

Let \(a_0 + a_1 x + \cdots + a_n x^n\) be a nonzero real polynomial of degree \(n\) with \(0 \le a_0 \le a_1 \le \cdots \le a_n\). Then every complex root \(z\) of this polynomial satisfies \(|z| \le 1\).

public theorem_wanted norm_le_one_of_aeval_eq_zero_of_monotone_coeff
    (p : ℝ[X]) (hp : p ≠ 0) (h0 : 0 ≤ p.coeff 0)
    (hmono : ∀ i < p.natDegree, p.coeff i ≤ p.coeff (i + 1))
    (z : ℂ) (hz : aeval z p = 0) : ‖z‖ ≤ 1

Sources

• Tingting Du, On the Reciprocal Sums and Products of m th-order Linear Recursive Sequences, Journal of Integer Sequences 27 (2024), Article 24.2.3, Lemma 3 (jis-2024-24.2.3-lem-3), quoted there as the Eneström–Kakeya theorem.

TheoremDominant root of \(x^m - a_1 x^{m-1} - \cdots - a_m\) with positive coefficients#●ready to prove

Let \(m \ge 2\) and let \(a_1, \dots, a_m\) be positive integers. Then the polynomial \(\varphi(x) = x^m - a_1 x^{m-1} - \cdots - a_m\) has exactly one positive real root \(\lambda\), this root satisfies \(\lambda > 1\), and the complex roots of \(\varphi\), counted with multiplicity, are \(\lambda\) (a simple root) together with \(m - 1\) roots of modulus less than \(\lambda\).

public theorem_wanted exists_dominant_root_of_pos_coeff_charPoly
    (m : ℕ) (hm : 2 ≤ m) (a : Fin m → ℕ) (ha : ∀ i, 0 < a i) (φ : ℤ[X])
    (hφ : φ = X ^ m - ∑ i : Fin m, C (a i : ℤ) * X ^ (m - 1 - (i : ℕ))) :
    ∃ ρ : ℝ, 1 < ρ ∧ (∀ x : ℝ, 0 < x → aeval x φ = 0 → x = ρ) ∧
      ∃ s : Multiset ℂ, (φ.map (Int.castRingHom ℂ)).roots = (ρ : ℂ) ::ₘ s ∧
        ∀ z ∈ s, ‖z‖ < ρ

Sources

• Tingting Du, On the Reciprocal Sums and Products of m th-order Linear Recursive Sequences, Journal of Integer Sequences 27 (2024), Article 24.2.3, Lemma 4 (jis-2024-24.2.3-lem-4).

TheoremAsymptotic expansion of a perturbed tail product#●ready to prove

Let \(\mu\) and \(\lambda\) be real numbers with \(1 < \mu < \lambda\), let \(c \ne 0\) be a real number, and let \((e_k)_{k \ge 0}\) be a real sequence with \(e_k = O\bigl((\mu/\lambda^3)^{k/2}\bigr)\) as \(k \to \infty\). Then, as \(n \to \infty\), \(\prod_{k \ge n} \bigl(1 - 1/(c\lambda^k) + e_k\bigr) = 1 - \sum_{k \ge n} 1/(c\lambda^k) + O\bigl((\mu/\lambda^3)^{n/2}\bigr)\).

public theorem_wanted tprod_one_sub_inv_add_eq_one_sub_tsum_add_isBigO
    (c α μ : ℝ) (hc : c ≠ 0) (hμ : 1 < μ) (hμα : μ < α) (e : ℕ → ℝ)
    (he : e =O[atTop] fun k : ℕ => (μ / α ^ 3) ^ ((k : ℝ) / 2)) :
    (fun n : ℕ => (∏' k : ℕ, (1 - 1 / (c * α ^ (n + k)) + e (n + k))) -
        (1 - ∑' k : ℕ, 1 / (c * α ^ (n + k)))) =O[atTop]
      fun n : ℕ => (μ / α ^ 3) ^ ((n : ℝ) / 2)

Sources

• Tingting Du, On the Reciprocal Sums and Products of m th-order Linear Recursive Sequences, Journal of Integer Sequences 27 (2024), Article 24.2.3, Lemma 7 (jis-2024-24.2.3-lem-7).

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.