LexOrder of multivariate power series

Given an ordering of σ such that WellOrderGT σ, the lexicographic order on σ →₀ ℕ is a well ordering, which can be used to define a natural valuation lexOrder on the ring MvPowerSeries σ R: the smallest exponent in the support.

noncomputable def MvPowerSeries.lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ : MvPowerSeries σ R) : WithTop (Lex (σ →₀ ℕ))

The lex order on multivariate power series.

Equations

• φ.lexOrder = if h : φ = 0 then ⊤ else let_fun ne := ⋯; ↑(⋯.min (⇑toLex '' Function.support φ) ne)

theorem MvPowerSeries.lexOrder_def_of_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) : ∃ (ne : (⇑toLex '' Function.support φ).Nonempty), φ.lexOrder = ↑(⋯.min (⇑toLex '' Function.support φ) ne)

@[simp]

theorem MvPowerSeries.lexOrder_eq_top_iff_eq_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ : MvPowerSeries σ R) : φ.lexOrder = ⊤ ↔ φ = 0

theorem MvPowerSeries.lexOrder_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] : lexOrder 0 = ⊤

theorem MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} (hφ : φ ≠ 0) : ∃ (d : σ →₀ ℕ), φ.lexOrder = ↑(toLex d)

theorem MvPowerSeries.coeff_ne_zero_of_lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑(toLex d) = φ.lexOrder) : (coeff R d) φ ≠ 0

theorem MvPowerSeries.coeff_eq_zero_of_lt_lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : ↑(toLex d) < φ.lexOrder) : (coeff R d) φ = 0

theorem MvPowerSeries.lexOrder_le_of_coeff_ne_zero {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {d : σ →₀ ℕ} (h : (coeff R d) φ ≠ 0) : φ.lexOrder ≤ ↑(toLex d)

theorem MvPowerSeries.le_lexOrder_iff {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ : MvPowerSeries σ R} {w : WithTop (Lex (σ →₀ ℕ))} : w ≤ φ.lexOrder ↔ ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff R d) φ = 0

theorem MvPowerSeries.min_lexOrder_le {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ ψ : MvPowerSeries σ R} : φ.lexOrder ⊓ ψ.lexOrder ≤ (φ + ψ).lexOrder

theorem MvPowerSeries.coeff_mul_of_add_lexOrder {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] {φ ψ : MvPowerSeries σ R} {p q : σ →₀ ℕ} (hp : φ.lexOrder = ↑(toLex p)) (hq : ψ.lexOrder = ↑(toLex q)) : (coeff R (p + q)) (φ * ψ) = (coeff R p) φ * (coeff R q) ψ

theorem MvPowerSeries.le_lexOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ ψ : MvPowerSeries σ R) : φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder

theorem MvPowerSeries.lexOrder_mul_ge {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] (φ ψ : MvPowerSeries σ R) : φ.lexOrder + ψ.lexOrder ≤ (φ * ψ).lexOrder

Alias of MvPowerSeries.le_lexOrder_mul.

theorem MvPowerSeries.lexOrder_mul {σ : Type u_1} {R : Type u_2} [Semiring R] [LinearOrder σ] [WellFoundedGT σ] [NoZeroDivisors R] (φ ψ : MvPowerSeries σ R) : (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder