theorem HexPolyZMathlib.norm_pow_sub_pow_le {x y : ℂ} {C : ℝ} (hx : ‖x‖ ≤ C) (hy : ‖y‖ ≤ C) (hC : 1 ≤ C) (i : ℕ) : ‖y ^ i - x ^ i‖ ≤ ↑i * C ^ (i - 1) * ‖y - x‖

The divided-difference entry bound: ‖yⁱ − xⁱ‖ ≤ i · Cⁱ⁻¹ · ‖y − x‖ when ‖x‖, ‖y‖ ≤ C and 1 ≤ C. Follows from the geometric factorisation yⁱ − xⁱ = (∑_{l<i} yˡ xⁱ⁻¹⁻ˡ)(y − x).

theorem HexPolyZMathlib.sqrt_sum_pow_sq_le (a : ℂ) (N : ℕ) : √(∑ i : Fin N, ‖a ^ ↑i‖ ^ 2) ≤ √↑N * max 1 ‖a‖ ^ (N - 1)

The L² norm of an ordinary Vandermonde column: √(∑ᵢ ‖aⁱ‖²) ≤ √N · max(1,‖a‖)^{N-1}.

theorem HexPolyZMathlib.sqrt_sum_sub_pow_sq_le {x y : ℂ} {C : ℝ} (hx : ‖x‖ ≤ C) (hy : ‖y‖ ≤ C) (hC : 1 ≤ C) (N : ℕ) : √(∑ i : Fin N, ‖y ^ ↑i - x ^ ↑i‖ ^ 2) ≤ C ^ (N - 2) * ‖y - x‖ * √(∑ i : Fin N, ↑↑i ^ 2)

The L² norm of the isolating (differenced) Vandermonde column: √(∑ᵢ ‖yⁱ − xⁱ‖²) ≤ C^{N-2} · ‖y − x‖ · √(∑ᵢ i²).

theorem HexPolyZMathlib.sqrt_sum_sq_le (N : ℕ) : √(∑ i : Fin N, ↑↑i ^ 2) ≤ √↑N ^ 3

√(∑_{i<N} i²) ≤ (√N)³.

theorem HexPolyZMathlib.norm_det_vandermonde_le {N : ℕ} (hN : 2 ≤ N) (c : ℂ) (α : Fin N → ℂ) {i₀ i₁ : Fin N} (hne : i₀ ≠ i₁) (hle : ‖α i₀‖ ≤ ‖α i₁‖) : ‖c‖ ^ (N - 1) * ‖(Matrix.vandermonde α).det‖ ≤ √↑N ^ (N - 1) * √(∑ i : Fin N, ↑↑i ^ 2) * (‖c‖ * ∏ j : Fin N, max 1 ‖α j‖) ^ (N - 1) * ‖α i₁ - α i₀‖

Mahler's isolating-column bound. For a leading coefficient c and points α : Fin N → ℂ with ‖α i₀‖ ≤ ‖α i₁‖, the scaled Vandermonde determinant is bounded by √N^{N-1} · √(∑ i²) · (‖c‖ · ∏ max(1,‖α j‖))^{N-1} · ‖α i₁ − α i₀‖.

theorem HexPolyZMathlib.norm_prod_roots_eq_sq {N : ℕ} (α : Fin N → ℂ) (hα : Function.Injective α) : ‖(Multiset.map (fun (x : ℂ) => (Multiset.map (fun (y : ℂ) => x - y) ((Multiset.map α Finset.univ.val).erase x)).prod) (Multiset.map α Finset.univ.val)).prod‖ = ‖(Matrix.vandermonde α).det‖ ^ 2

The off-diagonal root-difference product equals ‖det V‖² in norm.

theorem HexPolyZMathlib.norm_discr_eq {N : ℕ} (α : Fin N → ℂ) (hα : Function.Injective α) {f : Polynomial ℂ} (hf : 0 < f.degree) (hsplit : f.Splits) (hroots : f.roots = Multiset.map α Finset.univ.val) : ‖f.discr‖ = ‖f.leadingCoeff‖ ^ (2 * f.natDegree - 2) * ‖(Matrix.vandermonde α).det‖ ^ 2

The discriminant in root-enumeration form: ‖disc f‖ = ‖lc‖^{2n-2} · ‖det V‖².

theorem HexPolyZMathlib.one_le_mahlerDist_of_separable (p : Polynomial ℤ) (hsep : (Polynomial.map (Int.castRingHom ℚ) p).Separable) {z₁ z₂ : ℂ} (hr₁ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₁) (hr₂ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₂) (hne : z₁ ≠ z₂) : 1 ≤ √↑p.natDegree ^ (p.natDegree + 2) * (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ^ (p.natDegree - 1) * ‖z₁ - z₂‖

The exponent-independent assembly of Mahler's root-separation argument. For two distinct roots of a separable integral polynomial, the product of their distance with the Hadamard degree factor and the appropriate power of the Mahler measure is at least one. Executable precision specializations need only bound the final two factors.

theorem HexPolyZMathlib.one_le_mahlerDist (p : Polynomial ℤ) (hp : p ≠ 0) {z₁ z₂ : ℂ} (hr₁ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₁) (hr₂ : (Polynomial.map (Int.castRingHom ℂ) p).IsRoot z₂) (hne : z₁ ≠ z₂) : 1 ≤ √↑p.natDegree ^ (p.natDegree + 2) * (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure ^ (p.natDegree - 1) * ‖z₁ - z₂‖

Mahler separation for arbitrary nonzero integral polynomials. Repeated factors do not affect the set of roots: applying the separable theorem to the integral radical gives the same two roots, no larger degree, and no larger Mahler measure.