Documentation

Mathlib.Analysis.Polynomial.Norm

Sup Norm of Polynomials #

In this file we define the sup norm on Polynomials based on their coefficients as well as several basic results about this norm. We note that this is often called the (naive) height of the polynomial in the literature.

The sup norm is related to the Mahler measure of the polynomial. See Mathlib/Analysis/Polynomial/MahlerMeasure.lean.

Main definitions #

A Note on Naming #

In the literature, the sup norm is often called the (naive) height of a polynomial and the l^1 norm is often called the length of the polynomial. Unfortunately, these terms are extremely overloaded and Mathlib defines height differently.

TODOs #

All other l^p norms can be defined on Polynomials as well. In the literature, the l^1 norm is sometimes called the polynomial's length. The l^2 norm sometimes arises due to Parseval's theorem implying that the squared l^2 norm of a complex polynomial is the integral of the norm of the polynomial's value on the unit circle.

source
noncomputable def Polynomial.supNorm {A : Type u_1} [SeminormedRing A] (p : Polynomial A) :
ℝ

The sup norm of a polynomial on a semi-normed ring, defined as the maximum of its coefficients. Often called the (naive) height of the polynomial.

This is defined in terms of Polynomial.guassNorm.

Equations
Instances For
    source
    theorem Polynomial.supNorm_def' {A : Type u_1} [SeminormedRing A] (p : Polynomial A) :
    p.supNorm = if hp : p.support.Nonempty then p.support.sup' hp (norm ∘ p.coeff) else 0

    The direct definition of the supNorm

    source
    @[simp]
    theorem Polynomial.supNorm_zero {A : Type u_1} [SeminormedRing A] :
    supNorm 0 = 0
    source
    theorem Polynomial.supNorm_nonneg {A : Type u_1} [SeminormedRing A] (p : Polynomial A) :
    0 ≤ p.supNorm
    source
    @[simp]
    theorem Polynomial.supNorm_C {A : Type u_1} [SeminormedRing A] {a : A} :
    (C a).supNorm = ‖a‖
    source
    @[simp]
    theorem Polynomial.supNorm_monomial {A : Type u_1} [SeminormedRing A] (n : ℕ) {a : A} :
    ((monomial n) a).supNorm = ‖a‖
    source
    @[simp]
    theorem Polynomial.supNorm_X {A : Type u_1} [SeminormedRing A] [NormOneClass A] :
    X.supNorm = 1
    source
    theorem Polynomial.le_supNorm {A : Type u_1} [SeminormedRing A] (p : Polynomial A) (i : ℕ) :
    ‖p.coeff i‖ ≤ p.supNorm
    source
    theorem Polynomial.exists_eq_supNorm {A : Type u_1} [SeminormedRing A] (p : Polynomial A) :
    ∃ (i : ℕ), p.supNorm = ‖p.coeff i‖
    source
    theorem Polynomial.isGreatest_supNorm {A : Type u_1} [SeminormedRing A] (p : Polynomial A) :
    IsGreatest (Set.range fun (x : ℕ) => ‖p.coeff x‖) p.supNorm
    source
    theorem Polynomial.supNorm_eq_iSup {A : Type u_1} [SeminormedRing A] (p : Polynomial A) :
    p.supNorm = ⨆ (i : ℕ), ‖p.coeff i‖

    The supNorm can also be defined with an iSup. Note that this uses the fact that norm is both a ZeroHom and NonnegHom so is not a priori true from the gaussNorm definition.

    source
    theorem Polynomial.supNorm_eq_zero_iff {A : Type u_1} [NormedRing A] (p : Polynomial A) :
    p.supNorm = 0 ↔ p = 0