def HexRealRootsMathlib.Dyadic.toReal (x : Dyadic) : ℝ

Real value of a dyadic number, through Dyadic.toRat.

Equations

• HexRealRootsMathlib.Dyadic.toReal x = ↑x.toRat

@[simp]

theorem HexRealRootsMathlib.toReal_eq_cast_toRat (x : Dyadic) : Dyadic.toReal x = ↑x.toRat

Dyadic.toReal is the rational cast of toRat. A plain-import restatement of the definition, so downstream modules that do not import all this file can still bridge Dyadic.toReal to the ℚ-valued endpoints of an isolation.

@[reducible, inline]

noncomputable abbrev HexRealRootsMathlib.toPolyℝ (p : Hex.ZPoly) : Polynomial ℝ

The real cast of an executable integer polynomial.

Equations

• HexRealRootsMathlib.toPolyℝ p = Polynomial.map (Int.castRingHom ℝ) (HexPolyZMathlib.toPolynomial p)

@[reducible, inline]

noncomputable abbrev HexRealRootsMathlib.toPolyℂ (p : Hex.ZPoly) : Polynomial ℂ

The complex cast of an executable integer polynomial.

Equations

• HexRealRootsMathlib.toPolyℂ p = Polynomial.map (Int.castRingHom ℂ) (HexPolyZMathlib.toPolynomial p)

theorem HexRealRootsMathlib.toRat_shiftLeft (x : Dyadic) (i : ℤ) : (x <<< i).toRat = x.toRat * 2 ^ i

toRat turns a left shift into multiplication by a power of two.

theorem HexRealRootsMathlib.toRat_shiftRight (x : Dyadic) (i : ℤ) : (x >>> i).toRat = x.toRat * 2 ^ (-i)

toRat turns a right shift into multiplication by a negative power of two.

@[simp]

theorem HexRealRootsMathlib.toReal_ofInt (n : ℤ) : Dyadic.toReal (Dyadic.ofInt n) = ↑n

The real value of an integer dyadic is the integer cast.

@[simp]

theorem HexRealRootsMathlib.toReal_twoPow (k : ℤ) : Dyadic.toReal (Hex.twoPow k) = 2 ^ k

Hex.twoPow k has real value 2 ^ k.

theorem HexRealRootsMathlib.toReal_shiftLeft (x : Dyadic) (i : ℤ) : Dyadic.toReal (x <<< i) = Dyadic.toReal x * 2 ^ i

The real value of a left shift is multiplication by a power of two.

theorem HexRealRootsMathlib.toReal_shiftRight (x : Dyadic) (i : ℤ) : Dyadic.toReal (x >>> i) = Dyadic.toReal x * 2 ^ (-i)

The real value of a right shift is multiplication by a negative power of two.

@[simp]

theorem HexRealRootsMathlib.toReal_ofInt_shiftRight (n i : ℤ) : Dyadic.toReal (Dyadic.ofInt n >>> i) = ↑n * 2 ^ (-i)

The real value of the dyadic n / 2ⁱ (an integer shifted right by i bits).

theorem HexRealRootsMathlib.le_two_pow_ceilLog2Nat (m : ℕ) : m ≤ 2 ^ Hex.ceilLog2Nat m

ceilLog2Nat m is a base-two ceiling: m ≤ 2 ^ (ceilLog2Nat m).

theorem HexRealRootsMathlib.range_foldl_max_eq_finset_sup (g : ℕ → ℕ) (m : ℕ) : List.foldl (fun (acc i : ℕ) => max acc (g i)) 0 (List.range m) = (Finset.range m).sup g

The List.range fold used by rootBound to compute the maximum absolute non-leading coefficient equals the corresponding Finset.sup.

@[simp]

theorem HexRealRootsMathlib.coeff_toPolyℝ (p : Hex.ZPoly) (n : ℕ) : (toPolyℝ p).coeff n = ↑(Hex.DensePoly.coeff p n)

theorem HexRealRootsMathlib.eval_toPolyℝ (p : Hex.ZPoly) (x : ℝ) : Polynomial.eval x (toPolyℝ p) = ∑ i ∈ Finset.range (Hex.DensePoly.size p), ↑(Hex.DensePoly.coeff p i) * x ^ i

Evaluating the real cast at x is the degree-indexed sum of the integer coefficients cast to ℝ. For a literal ofCoeffs this unfolds via Finset.sum_range_succ into an explicit polynomial in x; combined with Polynomial.IsRoot, it turns a root goal into a plain equation ring/norm_num can discharge.

theorem HexRealRootsMathlib.natDegree_toPolyℝ (p : Hex.ZPoly) : (toPolyℝ p).natDegree = Hex.DensePoly.natDegree p

@[simp]

theorem HexRealRootsMathlib.coeff_toPolyℂ (p : Hex.ZPoly) (n : ℕ) : (toPolyℂ p).coeff n = ↑(Hex.DensePoly.coeff p n)

Coefficients of the complex cast are the complex casts of the integer coefficients.

theorem HexRealRootsMathlib.natDegree_toPolyℂ (p : Hex.ZPoly) : (toPolyℂ p).natDegree = Hex.DensePoly.natDegree p

The complex cast preserves the natural degree.

theorem HexRealRootsMathlib.leadingCoeff_toPolyℂ (p : Hex.ZPoly) : (toPolyℂ p).leadingCoeff = ↑(Hex.DensePoly.leadingCoeff p)

The complex cast preserves the leading coefficient.

theorem HexRealRootsMathlib.toPolyℂ_eq_map (p : Hex.ZPoly) : toPolyℂ p = Polynomial.map (Int.castRingHom ℂ) (HexPolyZMathlib.toPolynomial p)

The complex cast is the map of the integer polynomial.

theorem HexRealRootsMathlib.cauchyBound_le_rootBound (p : Hex.ZPoly) : ↑(toPolyℝ p).cauchyBound ≤ Dyadic.toReal (Hex.rootBound p)

The power-of-two Cauchy bound Hex.rootBound p dominates Cauchy's bound.

theorem HexRealRootsMathlib.rootBound_bounds_roots (p : Hex.ZPoly) (hp : toPolyℝ p ≠ 0) (r : ℝ) : (toPolyℝ p).IsRoot r → |r| < Dyadic.toReal (Hex.rootBound p)

Cauchy root bound. Every real root of a nonzero toPolyℝ p lies strictly inside the power-of-two bound Hex.rootBound p.

theorem HexRealRootsMathlib.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‖

Compatibility forwarding theorem for the generic divided-difference bound.

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

Compatibility forwarding theorem for the ordinary Vandermonde-column bound.

theorem HexRealRootsMathlib.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)

Compatibility forwarding theorem for the differenced Vandermonde-column bound.

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

Compatibility forwarding theorem for the sum-of-squares estimate.

theorem HexRealRootsMathlib.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₀‖

Compatibility forwarding theorem for the isolating-column determinant bound.

theorem HexRealRootsMathlib.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

Compatibility forwarding theorem for the off-diagonal root-product identity.

theorem HexRealRootsMathlib.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

Compatibility forwarding theorem for the discriminant/Vandermonde identity.

theorem HexRealRootsMathlib.pow_le_two_pow_sepExp (n L : ℕ) : √↑n ^ (n + 2) * ↑L ^ (n - 1) ≤ 2 ^ (((n + 2) * Hex.ceilLog2Nat n + 1) / 2 + (n - 1) * Hex.ceilLog2Nat L)

The closed-form separation exponent dominates the analytic bound: √n^{n+2} · L^{n-1} ≤ 2^E where E = ((n+2)·⌈log₂ n⌉ + 1)/2 + (n-1)·⌈log₂ L⌉.

theorem HexRealRootsMathlib.sepPrec_separates (p : Hex.ZPoly) (hsep : (Polynomial.map (Int.castRingHom ℚ) (HexPolyZMathlib.toPolynomial p)).Separable) (z₁ z₂ : ℂ) : (toPolyℂ p).IsRoot z₁ → (toPolyℂ p).IsRoot z₂ → z₁ ≠ z₂ → 2 ^ (-↑(Hex.sepPrec p)) < ‖z₁ - z₂‖ / 4

Mahler's separation bound. For a p whose rational image is separable (equivalently squarefree over ℚ; squareFreeRat_iff discharges this from Hex.SquareFreeRat), any two distinct complex roots of toPolyℂ p are more than 4 · 2^{-sepPrec p} apart. Vacuous for degree ≤ 1 (where sepPrec = 0 and there is at most one root), so the content is the degree ≥ 2 case.