Gauss norm for power series

This file defines the Gauss norm for power series using the gaussNorm for multivariate 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

• Using PowerSeries.gaussNorm_eq, 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.

• PowerSeries.gaussNormC_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.

• PowerSeries.gaussNorm_add_le_max: if v is a non-negative non-archimedean function and the set of values v (coeff t f) * c ^ t is bounded above (similarily for g), then the Gauss norm has the non-archimedean property.

@[reducible, inline]

noncomputable abbrev PowerSeries.gaussNorm {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) : ℝ

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

Equations

• PowerSeries.gaussNorm v c f = MvPowerSeries.gaussNorm v (fun (x : Unit) => c) f

theorem PowerSeries.gaussNorm_eq {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) : gaussNorm v c f = ⨆ (i : ℕ), v ((coeff i) f) * c ^ i

@[reducible, inline]

abbrev PowerSeries.HasGaussNorm {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) : Prop

We say f HasGaussNorm if the values v (coeff t f) * c ^ t is bounded above, that is gaussNormC f is finite.

Equations

• PowerSeries.HasGaussNorm v c f = BddAbove (Set.range fun (t : ℕ) => v ((PowerSeries.coeff t) f) * c ^ t)

theorem PowerSeries.HasGaussNorm.HasMvGaussNorm {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) (h : HasGaussNorm v c f) : MvPowerSeries.HasGaussNorm v (fun (x : Unit) => c) f

theorem PowerSeries.gaussNorm_zero {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (vZero : v 0 = 0) : gaussNorm v c 0 = 0

theorem PowerSeries.le_gaussNorm {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) (hbd : HasGaussNorm v c f) (t : ℕ) : v ((coeff t) f) * c ^ t ≤ gaussNorm v c f

theorem PowerSeries.gaussNorm_nonneg {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) (vNonneg : ∀ (a : R), v a ≥ 0) : 0 ≤ gaussNorm v c f

theorem PowerSeries.gaussNorm_eq_zero_iff {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f : PowerSeries R) (vZero : v 0 = 0) (vNonneg : ∀ (a : R), v a ≥ 0) (h_eq_zero : ∀ (x : R), v x = 0 → x = 0) (hc : 0 < c) (hbd : HasGaussNorm v c f) : gaussNorm v c f = 0 ↔ f = 0

theorem PowerSeries.gaussNorm_add_le_max {R : Type u_1} [Semiring R] (v : R → ℝ) (c : ℝ) (f g : PowerSeries R) (hc : 0 ≤ c) (vNonneg : ∀ (a : R), v a ≥ 0) (hv : ∀ (x y : R), v (x + y) ≤ max (v x) (v y)) (hbfd : HasGaussNorm v c f) (hbgd : HasGaussNorm v c g) : gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)