noncomputable def HexPolyZMathlib.l2norm (f : Polynomial ℤ) : ℝ

The Euclidean norm of the coefficient vector of an integer polynomial.

Equations

• HexPolyZMathlib.l2norm f = √(∑ i ∈ f.support, ↑(f.coeff i) ^ 2)

@[simp]

theorem HexPolyZMathlib.coeff_map_intCast (f : Polynomial ℤ) (n : ℕ) : (Polynomial.map (Int.castRingHom ℂ) f).coeff n = ↑(f.coeff n)

Coefficients of the complex cast of an integer polynomial are the complex casts of its integer coefficients.

@[simp]

theorem HexPolyZMathlib.natDegree_map_intCast (f : Polynomial ℤ) : (Polynomial.map (Int.castRingHom ℂ) f).natDegree = f.natDegree

Casting an integer polynomial into ℂ[X] preserves its natural degree.

@[simp]

theorem HexPolyZMathlib.support_map_intCast (f : Polynomial ℤ) : (Polynomial.map (Int.castRingHom ℂ) f).support = f.support

Casting an integer polynomial into ℂ[X] preserves its support.

@[simp]

theorem HexPolyZMathlib.norm_coeff_map_intCast (f : Polynomial ℤ) (n : ℕ) : ‖(Polynomial.map (Int.castRingHom ℂ) f).coeff n‖ = ↑(f.coeff n).natAbs

The complex norm of a cast coefficient is the absolute value of the integer coefficient.

theorem HexPolyZMathlib.sq_norm_coeff_map_intCast (f : Polynomial ℤ) (n : ℕ) : ‖(Polynomial.map (Int.castRingHom ℂ) f).coeff n‖ ^ 2 = ↑(f.coeff n) ^ 2

The squared complex norm of a cast coefficient is the squared integer coefficient, the term appearing under the l2norm square root.

theorem HexPolyZMathlib.mahlerMeasure_le_l2norm (f : Polynomial ℤ) : (Polynomial.map (Int.castRingHom ℂ) f).mahlerMeasure ≤ l2norm f

Landau's inequality specialized to Polynomial ℤ via the complex cast.

theorem HexPolyZMathlib.l2norm_toPolynomial_sq_le_coeffNormSq (f : Hex.ZPoly) : l2norm (toPolynomial f) ^ 2 ≤ ↑f.coeffNormSq

The transported Mathlib coefficient-vector norm squared is bounded by the executable squared coefficient norm.

theorem HexPolyZMathlib.l2norm_toPolynomial_sq_eq_coeffNormSq (f : Hex.ZPoly) : l2norm (toPolynomial f) ^ 2 = ↑f.coeffNormSq

The transported Mathlib coefficient-vector norm squared is exactly the executable squared coefficient norm; the executable range only pads Mathlib's finite support with zero coefficients.

theorem HexPolyZMathlib.binom_eq_choose (n k : ℕ) : Hex.Nat.binom n k = n.choose k

The executable Mignotte-bound binomial coefficient agrees with Mathlib's Nat.choose.

theorem HexPolyZMathlib.mignotte_bound (f g : Polynomial ℤ) (hf : f ≠ 0) (hg : g ∣ f) (j : ℕ) : ↑(g.coeff j).natAbs ≤ ↑(g.natDegree.choose j) * l2norm f

Mignotte's coefficient bound for integer polynomial factors, obtained by combining Mathlib's Mahler-measure coefficient estimate with Landau's inequality.

theorem HexPolyZMathlib.mignotte_cofactor_bound (g h : Polynomial ℤ) (j : ℕ) : ↑(h.leadingCoeff * g.coeff j).natAbs ≤ ↑(g.natDegree.choose j) * l2norm (g * h)

Mignotte's bound in the proportional coordinate used by direct Berlekamp--Zassenhaus recovery.

If f = g * h, the coefficients reconstructed from the monic local factors are those of leadingCoeff h • g, not necessarily those of g itself. The same Mignotte window bounds them: ‖leadingCoeff h‖ ≤ M(h), the ordinary coefficient estimate bounds g by choose · M(g), and multiplicativity of Mahler measure gives M(g) M(h) = M(f).