Gauss norm for polynomials

This file defines the Gauss norm for polynomials. Given a polynomial p in R[X], a function v : R → ℝ and a real number c, the Gauss norm is defined as the supremum of the set of all values of v (p.coeff i) * c ^ i for all i in the support of p.

This is mostly useful when v is an absolute value on R and c is set to be 1, in which case the Gauss norm corresponds to the maximum of the absolute values of the coefficients of p. When R is a subring of ℂ and v is the standard absolute value, this is sometimes called the "height" of p.

In the file Mathlib/RingTheory/PowerSeries/GaussNorm.lean, the Gauss norm is defined for power series. This is a generalization of the Gauss norm defined in this file in case v is a non-negative function with v 0 = 0 and c ≥ 0.

Main Definitions and Results

• Polynomial.gaussNorm is the supremum of the set of all values of v (p.coeff i) * c ^ i for all i in the support of p, where p is a polynomial in R[X], v : R → ℝ is a function and c is a real number.
• Polynomial.gaussNorm_coe_powerSeries: if v is a non-negative function with v 0 = 0 and c is nonnegative, the Gauss norm of a polynomial is equal to its Gauss norm as a power series.
• Polynomial.gaussNorm_nonneg: if v is a non-negative function, then the Gauss norm is non-negative.
• Polynomial.gaussNorm_eq_zero_iff: if v x = 0 ↔ x = 0 for all x : R, then the Gauss norm is zero if and only if the polynomial is zero.

def Polynomial.gaussNorm {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) (p : Polynomial R) : ℝ

Given a polynomial p in R[X], a function v : R → ℝ and a real number c, the Gauss norm is defined as the supremum of the set of all values of v (p.coeff i) * c ^ i for all i in the support of p.

Equations

• Polynomial.gaussNorm v c p = if h : p.support.Nonempty then p.support.sup' h fun (i : ℕ) => v (p.coeff i) * c ^ i else 0

@[simp]

theorem Polynomial.gaussNorm_zero {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) : gaussNorm v c 0 = 0

theorem Polynomial.exists_eq_gaussNorm {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) (p : Polynomial R) [ZeroHomClass F R ℝ] : ∃ (i : ℕ), gaussNorm v c p = v (p.coeff i) * c ^ i

@[simp]

theorem Polynomial.gaussNorm_C {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) [ZeroHomClass F R ℝ] (r : R) : gaussNorm v c (C r) = v r

@[simp]

theorem Polynomial.gaussNorm_monomial {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) [ZeroHomClass F R ℝ] (n : ℕ) (r : R) : gaussNorm v c ((monomial n) r) = v r * c ^ n

@[simp]

theorem Polynomial.gaussNorm_coe_powerSeries {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) : PowerSeries.gaussNorm v c ↑p = gaussNorm v c p

@[simp]

theorem Polynomial.gaussNorm_eq_zero_iff {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (h_eq_zero : ∀ (x : R), v x = 0 → x = 0) (hc : 0 < c) : gaussNorm v c p = 0 ↔ p = 0

theorem Polynomial.gaussNorm_nonneg {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R) (hc : 0 ≤ c) [NonnegHomClass F R ℝ] : 0 ≤ gaussNorm v c p

theorem Polynomial.le_gaussNorm {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} (p : Polynomial R) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) (i : ℕ) : v (p.coeff i) * c ^ i ≤ gaussNorm v c p

@[simp]

theorem PowerSeries.gaussNorm_C {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} (r : R) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) : gaussNorm v c (C r) = v r

@[simp]

theorem PowerSeries.gaussNorm_monomial {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} (r : R) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hc : 0 ≤ c) (n : ℕ) : gaussNorm v c ((monomial n) r) = v r * c ^ n