Gauss norm for multivariate power series

This file defines the Gauss norm for power series. Given a multivariate power series f, a function v : R → ℝ and a tuple c of real numbers, the Gauss norm is defined as the supremum of the set of all values of v (coeff t f) * ∏ i : t.support, c i for all t : σ →₀ ℕ.

Main definitions and results

• MvPowerSeries.gaussNormC is the supremum of the set of all values of v (coeff t f) * ∏ i : t.support, c i for all t : σ →₀ ℕ, where f is a multivariate power series, v : R → ℝ is a function and c is a tuple of real numbers.

• MvPowerSeries.gaussNormC_nonneg: if v is a non-negative function, then the Gauss norm is non-negative.

• MvPowerSeries.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.

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

noncomputable def MvPowerSeries.gaussNorm {R : Type u_1} {σ : Type u_2} [Semiring R] (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) : ℝ

Given a multivariate power series f in, a function v : R → ℝ and a tuple c of real numbers, the Gauss norm is defined as the supremum of the set of all values of v (coeff t f) * ∏ i : t.support, c i for all t : σ →₀ ℕ.

Equations

• MvPowerSeries.gaussNorm v c f = ⨆ (t : σ →₀ ℕ), v ((MvPowerSeries.coeff t) f) * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2

@[reducible, inline]

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

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

Equations

• MvPowerSeries.HasGaussNorm v c f = BddAbove (Set.range fun (t : σ →₀ ℕ) => v ((MvPowerSeries.coeff t) f) * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2)

@[simp]

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

theorem MvPowerSeries.le_gaussNorm {R : Type u_1} {σ : Type u_2} [Semiring R] (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) (hbd : HasGaussNorm v c f) (t : σ →₀ ℕ) : (v ((coeff t) f) * t.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) ≤ gaussNorm v c f

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

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

theorem MvPowerSeries.gaussNorm_add_le_max {R : Type u_1} {σ : Type u_2} [Semiring R] (v : R → ℝ) (c : σ → ℝ) (f g : MvPowerSeries σ 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)