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.gaussNorm 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.gaussNorm_nonneg: if v is a non-negative function, then the Gauss norm is non-negative.

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

• 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 (similarly for g), then the Gauss norm has the non-archimedean property.

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

We say f HasGaussNorm if the values v (coeff t f) * ∏ i : t.support, c i is bounded above, that is gaussNorm 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} (v : R → ℝ) (c : σ → ℝ) [Semiring R] (vZero : v 0 = 0) : gaussNorm v c 0 = 0

theorem MvPowerSeries.le_gaussNorm {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [Semiring 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} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [Semiring 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} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [Semiring 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} (v : R → ℝ) (c : σ → ℝ) [Semiring R] (f g : MvPowerSeries σ R) (hc : 0 ≤ c) (vNonneg : ∀ (a : R), v a ≥ 0) (hv : IsNonarchimedean v) (hbfd : HasGaussNorm v c f) (hbgd : HasGaussNorm v c g) : gaussNorm v c (f + g) ≤ max (gaussNorm v c f) (gaussNorm v c g)

theorem MvPowerSeries.gaussNorm_mul_le {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [Semiring R] (f g : MvPowerSeries σ R) (hc : 0 ≤ c) (vNonneg : ∀ (a : R), v a ≥ 0) (vMul : ∀ (a b : R), v (a * b) ≤ v a * v b) (vna : IsNonarchimedean v) (vZero : v 0 = 0) (hbfd : HasGaussNorm v c f) (hbgd : HasGaussNorm v c g) : gaussNorm v c (f * g) ≤ gaussNorm v c f * gaussNorm v c g

@[reducible, inline]

abbrev MvPowerSeries.AchievesGaussNorm {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) (f : MvPowerSeries σ R) [Ring R] (i : σ →₀ ℕ) : Prop

Predicate for when the gaussNorm is achieved by an index.

Equations

• MvPowerSeries.AchievesGaussNorm v c f i = ((v ((MvPowerSeries.coeff i) f) * i.prod fun (x1 : σ) (x2 : ℕ) => c x1 ^ x2) = MvPowerSeries.gaussNorm v c f)

theorem MvPowerSeries.ultrametric_strict {α : Type u_3} {S : Type u_4} [LinearOrder S] [AddCommGroup α] (f : α → S) (na : IsNonarchimedean f) (Neg : ∀ (a : α), f a = f (-a)) {a b : α} (hne : f a ≠ f b) : f (a + b) = max (f a) (f b)

theorem MvPowerSeries.Finset.Nonempty.map_sum_le_sup'_map {α : Type u_5} {S : Type u_6} [Semiring S] [LinearOrder S] [AddCommMonoid α] (g : α → S) {ι : Type u_7} {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (na : ∀ (a b : α), g (a + b) ≤ max (g a) (g b)) : g (∑ i ∈ s, f i) ≤ s.sup' hs fun (x : ι) => g (f x)

theorem MvPowerSeries.antidiagonal_dominant {R : Type u_1} {σ : Type u_2} (v : R → ℝ) [Ring R] [DecidableEq σ] (f g : MvPowerSeries σ R) (i j : σ →₀ ℕ) (vna : IsNonarchimedean v) (vMulEq : ∀ (a b : R), v (a * b) = v a * v b) (vNeg : ∀ (a : R), v a = v (-a)) (hdom : ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)) : v ((coeff (i + j)) (f * g)) = v ((coeff i) f * (coeff j) g)

theorem MvPowerSeries.gaussNorm_le_mul {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [Ring R] [DecidableEq σ] (f g : MvPowerSeries σ R) (vMulEq : ∀ (a b : R), v (a * b) = v a * v b) (vna : IsNonarchimedean v) (vNeg : ∀ (a : R), v a = v (-a)) (hbfg : HasGaussNorm v c (f * g)) (hdom : ∃ (i : σ →₀ ℕ) (j : σ →₀ ℕ), AchievesGaussNorm v c f i ∧ AchievesGaussNorm v c g j ∧ ∀ p ∈ Finset.antidiagonal (i + j), p ≠ (i, j) → v ((coeff p.1) f * (coeff p.2) g) < v ((coeff i) f) * v ((coeff j) g)) : gaussNorm v c f * gaussNorm v c g ≤ gaussNorm v c (f * g)