L1 norm and root bounds for polynomials

DefinitionL1 norm of a polynomial#✓fully proved

Let \(K\) be a semiring and \(v\) a real-valued absolute value on \(K\). The L1 norm of a polynomial \(p = \sum_i a_i X^i \in K[X]\) with respect to \(v\) is the real number \(\|p\|_v = \sum_i v(a_i)\), where the sum runs over the indices \(i\) with \(a_i \neq 0\).

noncomputable def l1Norm (v : AbsoluteValue K ℝ) (p : Polynomial K) : ℝ :=
  p.sum fun _ a ↦ v a

Used by 11

Used byRoot bound by the L1 norm · L1 norm as a sum over the support · L1 norm as a sum up to the degree · L1 norm of a monic polynomial · Nonnegativity of the L1 norm · L1 norm of the zero polynomial · Monic polynomials close in L1 norm have the same degree · Monic polynomials have L1 norm at least one · Closest conjugate roots of nearby monic polynomials · Approximation by irreducible separable polynomials over a dense field · Small monic perturbations stay irreducible and separable

TheoremL1 norm as a sum over the support#✓fully proved

Let \(K\) be a semiring and \(v\) a real-valued absolute value on \(K\). For every polynomial \(p = \sum_i a_i X^i \in K[X]\), the L1 norm \(\|p\|_v\) of \(p\) with respect to \(v\) equals \(\sum_{i \in S} v(a_i)\), where \(S = \{ i : a_i \neq 0 \}\) is the support of \(p\).

theorem l1Norm_def (v : AbsoluteValue K ℝ) (p : Polynomial K) :
    l1Norm v p = ∑ i ∈ p.support, v (p.coeff i)

Uses 1 · Used by 5

Statement usesL1 norm of a polynomial

Used byL1 norm as a sum up to the degree · Nonnegativity of the L1 norm · Monic polynomials close in L1 norm have the same degree · Closest conjugate roots of nearby monic polynomials · Approximation by irreducible separable polynomials over a dense field

TheoremL1 norm of the zero polynomial#✓fully proved

Let \(K\) be a semiring and \(v\) a real-valued absolute value on \(K\). The L1 norm of the zero polynomial in \(K[X]\) with respect to \(v\) is \(0\).

@[simp]
theorem l1Norm_zero (v : AbsoluteValue K ℝ) :
    l1Norm v (0 : Polynomial K) = 0

Uses 1

Statement usesL1 norm of a polynomial

TheoremNonnegativity of the L1 norm#✓fully proved

Let \(K\) be a semiring and \(v\) a real-valued absolute value on \(K\). For every polynomial \(p \in K[X]\), the L1 norm of \(p\) with respect to \(v\) satisfies \(\|p\|_v \ge 0\).

theorem l1Norm_nonneg (v : AbsoluteValue K ℝ) (p : Polynomial K) :
    0 ≤ l1Norm v p

Uses 2 · Used by 1

Statement usesL1 norm of a polynomial

Proof usesL1 norm as a sum over the support

Used byClosest conjugate roots of nearby monic polynomials

TheoremL1 norm as a sum up to the degree#✓fully proved

Let \(K\) be a semiring and \(v\) a real-valued absolute value on \(K\). Let \(p = \sum_i a_i X^i \in K[X]\) and let \(n\) be the degree of \(p\), with \(n = 0\) when \(p = 0\). Then the L1 norm of \(p\) with respect to \(v\) is \(\|p\|_v = \sum_{i=0}^{n} v(a_i)\).

theorem l1Norm_eq_sum_range (v : AbsoluteValue K ℝ) (p : Polynomial K) :
    l1Norm v p = ∑ i ∈ Finset.range (p.natDegree + 1), v (p.coeff i)

Uses 2 · Used by 2

Statement usesL1 norm of a polynomial

Proof usesL1 norm as a sum over the support

Used byL1 norm of a monic polynomial · Monic polynomials have L1 norm at least one

TheoremL1 norm of a monic polynomial#✓fully proved

Let \(K\) be a nontrivial semiring (one with \(0 \neq 1\)) and \(v\) a real-valued absolute value on \(K\). If \(f = \sum_i a_i X^i \in K[X]\) is monic of degree \(n\), then the L1 norm of \(f\) with respect to \(v\) is \(\|f\|_v = \sum_{i=0}^{n-1} v(a_i) + 1\).

theorem l1Norm_eq_sum_range_add_one_of_monic [Nontrivial K]
    (v : AbsoluteValue K ℝ) (f : Polynomial K) (hf : f.Monic) :
    l1Norm v f = (∑ i ∈ Finset.range f.natDegree, v (f.coeff i)) + 1

Uses 2 · Used by 1

Statement usesL1 norm of a polynomial

Proof usesL1 norm as a sum up to the degree

Used byRoot bound by the L1 norm

TheoremMonic polynomials have L1 norm at least one#✓fully proved

Let \(K\) be a nontrivial semiring (one with \(0 \neq 1\)) and \(v\) a real-valued absolute value on \(K\). If \(f \in K[X]\) is monic, then the L1 norm of \(f\) with respect to \(v\) satisfies \(\|f\|_v \ge 1\).

theorem one_le_l1Norm_of_monic [Nontrivial K]
    (v : AbsoluteValue K ℝ) (f : Polynomial K) (hf : f.Monic) :
    1 ≤ l1Norm v f

Uses 2 · Used by 2

Statement usesL1 norm of a polynomial

Proof usesL1 norm as a sum up to the degree

Used byRoot bound by the L1 norm · Closest conjugate roots of nearby monic polynomials

TheoremMonic polynomials close in L1 norm have the same degree#✓fully proved

Let \(K\) be a nontrivial ring and \(v\) a real-valued absolute value on \(K\). If \(f, g \in K[x]\) are monic and the L1 norm of \(f - g\) with respect to \(v\) is strictly less than \(1\), then \(f\) and \(g\) have the same degree.

theorem natDegree_eq_of_monic_of_l1Norm_sub_lt_one (v : AbsoluteValue K ℝ)
    {f g : Polynomial K} (hf : f.Monic) (hg : g.Monic)
    (h : l1Norm v (f - g) < 1) : f.natDegree = g.natDegree

Uses 2 · Used by 2

Statement usesL1 norm of a polynomial

Proof usesL1 norm as a sum over the support

Used byClosest conjugate roots of nearby monic polynomials · Small monic perturbations stay irreducible and separable

TheoremRoot bound by the L1 norm#✓fully proved

Let \(K\) and \(L\) be fields with \(L\) a \(K\)-algebra, let \(v\) be a real-valued absolute value on \(K\), and let \(w\) be a real-valued absolute value on \(L\) lying over \(v\), that is, \(w(x) = v(x)\) for every \(x \in K\) viewed in \(L\) through the algebra map. If \(f\) is a monic polynomial over \(K\) and \(\alpha \in L\) is a root of \(f\), then \(w(\alpha)\) is strictly less than the L1 norm of \(f\) with respect to \(v\).

No algebraicity, finiteness, completeness, or archimedean hypothesis is needed.

theorem aeval_lt_l1Norm_of_monic_of_aeval_eq_zero {f : Polynomial K}
    (hf : f.Monic) {α : L} (hroot : aeval α f = 0) :
    w α < l1Norm v f

Uses 3 · Used by 1

Statement usesL1 norm of a polynomial

Proof usesL1 norm of a monic polynomial · Monic polynomials have L1 norm at least one

Used byClosest conjugate roots of nearby monic polynomials

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.