Gauss norm for power series

This file defines the Gauss norm for power series. Given a power series f 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 (f.coeff i) * c ^ i for all i : ℕ.

In case f is a polynomial, v is a non-negative function with v 0 = 0 and c ≥ 0, f.gaussNorm v c reduces to the Gauss norm defined in Mathlib/RingTheory/Polynomial/GaussNorm.lean, see Polynomial.gaussNorm_coe_powerSeries.

Main Definitions and Results

• PowerSeries.gaussNorm is the supremum of the set of all values of v (f.coeff i) * c ^ i for all i : ℕ, where f is a power series in R⟦X⟧, v : R → ℝ is a function and c is a real number.
• PowerSeries.gaussNorm_nonneg: if v is a non-negative function, then the Gauss norm is non-negative.
• PowerSeries.gaussNorm_eq_zero_iff: if v is a non-negative function and v x = 0 ↔ x = 0 for all x : R and c is positive, then the Gauss norm is zero if and only if the power series is zero.

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

Given a power series f 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 (f.coeff i) * c ^ i for all i : ℕ.

Equations

• PowerSeries.gaussNorm v c f = ⨆ (i : ℕ), v ((PowerSeries.coeff i) f) * c ^ i

theorem PowerSeries.le_gaussNorm {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] (v : F) (c : ℝ) (f : PowerSeries R) (hbd : BddAbove {x : ℝ | ∃ (i : ℕ), v ((coeff i) f) * c ^ i = x}) (i : ℕ) : v ((coeff i) f) * c ^ i ≤ gaussNorm v c f

@[simp]

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

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

@[simp]

theorem PowerSeries.gaussNorm_eq_zero_iff {R : Type u_1} {F : Type u_2} [Semiring R] [FunLike F R ℝ] [ZeroHomClass F R ℝ] [NonnegHomClass F R ℝ] {v : F} (h_eq_zero : ∀ (x : R), v x = 0 → x = 0) {f : PowerSeries R} {c : ℝ} (hc : 0 < c) (hbd : BddAbove (Set.range fun (i : ℕ) => v ((coeff i) f) * c ^ i)) : gaussNorm v c f = 0 ↔ f = 0