Documentation

Mathlib.RingTheory.Polynomial.GaussNorm

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 nonnegative function with v 0 = 0 and c ≥ 0.

Main Definitions and Results #

source
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
Instances For
    source
    @[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
    source
    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
    source
    @[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
    source
    @[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
    source
    @[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

    If v is a nonnegative 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.

    source
    @[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

    If v x = 0 → x = 0 for all x : R and v is nonnegative, then the Gauss norm is zero if and only if the polynomial is zero.

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

    If v is a nonnegative function, then the Gauss norm is nonnegative.

    source
    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
    source
    @[simp]
    theorem Polynomial.gaussNorm_zero_right {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (p : Polynomial R) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] :
    gaussNorm v 0 p = v (p.coeff 0)
    source
    theorem Polynomial.exists_min_eq_gaussNorm {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (p : Polynomial R) (hc : 0 ≤ c) :
    ∃ (i : ℕ), gaussNorm v c p = v (p.coeff i) * c ^ i ∧ ∀ j < i, v (p.coeff j) * c ^ j < gaussNorm v c p

    If v is a nonnegative function with v 0 = 0 and c is nonnegative, there exists a minimal index i such that the Gauss norm of p at c is attained at i.

    source
    theorem Polynomial.isNonarchimedean_gaussNorm {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] (hna : IsNonarchimedean ⇑v) {c : ℝ} (hc : 0 ≤ c) :
    IsNonarchimedean (gaussNorm v c)

    If v is a nonnegative nonarchimedean function with v 0 = 0 and c is nonnegative, the Gauss norm is nonarchimedean.

    source
    theorem Polynomial.gaussNorm_mul_le {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) {c : ℝ} [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] [MulHomClass F R ℝ] (hna : IsNonarchimedean ⇑v) (p q : Polynomial R) (hc : 0 ≤ c) :
    gaussNorm v c (p * q) ≤ gaussNorm v c p * gaussNorm v c q

    If v is a nonnegative nonarchimedean multiplicative function with v 0 = 0 and c is nonnegative, then the Gauss norm is submultiplicative.

    source
    theorem Polynomial.gaussNorm_mul {c : ℝ} {R : Type u_3} [Ring R] {v : AbsoluteValue R ℝ} (hna : IsNonarchimedean ⇑v) (hc : 0 < c) (p q : Polynomial R) :
    gaussNorm v c (p * q) = gaussNorm v c p * gaussNorm v c q

    If v is a nonarchimedean absolute value, then the Gauss norm is multiplicative.

    source
    theorem Polynomial.gaussNorm_isAbsoluteValue {c : ℝ} {R : Type u_3} [Ring R] {v : AbsoluteValue R ℝ} (hna : IsNonarchimedean ⇑v) (hc : 0 < c) :
    IsAbsoluteValue (gaussNorm v c)

    If v is a nonarchimedean absolute value, then the Gauss norm is an absolute value.

    source
    @[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
    source
    @[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