feat(MvPowerSeries.Order): order of multivariate power series (#14983)

Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

Author: AntoineChambert-Loir

Mathlib.lean

@@ -4266,6 +4266,7 @@ import Mathlib.RingTheory.MvPowerSeries.Basic
 import Mathlib.RingTheory.MvPowerSeries.Inverse
 import Mathlib.RingTheory.MvPowerSeries.LexOrder
 import Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
+import Mathlib.RingTheory.MvPowerSeries.Order
 import Mathlib.RingTheory.MvPowerSeries.Trunc
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.Nilpotent.Basic

Mathlib/Data/Finsupp/Weight.lean

@@ -3,7 +3,9 @@ Copyright (c) 2024 Antoine Chambert-Loir, María Inés de Frutos-Fernández. All
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández
 -/
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.Data.Finsupp.Antidiagonal
 import Mathlib.LinearAlgebra.Finsupp
 
 /-! # weights of Finsupp functions
@@ -34,6 +36,9 @@ for `OrderedAddCommMonoid M`, when `f s ≠ 0` and all `w i` are nonnegative.
 - `Finsupp.weight_eq_zero_iff_eq_zero` says that `f.weight w = 0` iff
 `f = 0` for `NonTorsion Weight w` and `CanonicallyOrderedAddCommMonoid M`.
 
+- For `w : σ → ℕ` and `Finite σ`, `Finsupp.finite_of_nat_weight_le` proves that
+there are finitely many `f : σ →₀ ℕ` of bounded weight.
+
 ## Degree
 
 - `Finsupp.degree`:  the weight when all components of `w` are equal to `1 : ℕ`.
@@ -46,6 +51,10 @@ The present choice is to have it defined as a plain function.
 - `Finsupp.degree_eq_weight_one` says `f.degree = f.weight 1`.
 This is useful to access the additivity properties of `Finsupp.degree`
 
+- For `Finite σ`, `Finsupp.finite_of_degree_le` proves that
+there are finitely many `f : σ →₀ ℕ` of bounded degree.
+
+
 
 ## TODO
 
@@ -159,6 +168,25 @@ theorem weight_eq_zero_iff_eq_zero
   · intro h
     rw [h, map_zero]
 
+theorem finite_of_nat_weight_le [Finite σ] (w : σ → ℕ) (hw : ∀ x, w x ≠ 0) (n : ℕ) :
+    {d : σ →₀ ℕ | weight w d ≤ n}.Finite := by
+  classical
+  set fg := Finset.antidiagonal (Finsupp.equivFunOnFinite.symm (Function.const σ n)) with hfg
+  suffices {d : σ →₀ ℕ | weight w d ≤ n} ⊆ ↑(fg.image fun uv => uv.fst) by
+    exact Set.Finite.subset (Finset.finite_toSet _) this
+  intro d hd
+  rw [hfg]
+  simp only [Finset.coe_image, Set.mem_image, Finset.mem_coe,
+    Finset.mem_antidiagonal, Prod.exists, exists_and_right, exists_eq_right]
+  use Finsupp.equivFunOnFinite.symm (Function.const σ n) - d
+  ext x
+  simp only [Finsupp.coe_add, Finsupp.coe_tsub, Pi.add_apply, Pi.sub_apply,
+    Finsupp.equivFunOnFinite_symm_apply_toFun, Function.const_apply]
+  rw [add_comm]
+  apply Nat.sub_add_cancel
+  apply le_trans (le_weight w (hw x) d)
+  simpa only [Set.mem_setOf_eq] using hd
+
 end CanonicallyOrderedAddCommMonoid
 
 /-- The degree of a finsupp function. -/
@@ -190,4 +218,11 @@ theorem le_degree (s : σ) (f : σ →₀ ℕ) : f s ≤ degree f  := by
   apply le_weight
   simp only [Pi.one_apply, ne_eq, one_ne_zero, not_false_eq_true]
 
+theorem finite_of_degree_le [Finite σ] (n : ℕ) :
+    {f : σ →₀ ℕ | degree f ≤ n}.Finite := by
+  simp_rw [degree_eq_weight_one]
+  refine finite_of_nat_weight_le (Function.const σ 1) ?_ n
+  intro _
+  simp only [Function.const_apply, ne_eq, one_ne_zero, not_false_eq_true]
+
 end Finsupp

Mathlib/RingTheory/MvPowerSeries/Basic.lean

@@ -134,6 +134,9 @@ def monomial (n : σ →₀ ℕ) : R →ₗ[R] MvPowerSeries σ R :=
 def coeff (n : σ →₀ ℕ) : MvPowerSeries σ R →ₗ[R] R :=
   LinearMap.proj n
 
+theorem coeff_apply (f : MvPowerSeries σ R) (d : σ →₀ ℕ) : coeff R d f = f d :=
+  rfl
+
 variable {R}
 
 /-- Two multivariate formal power series are equal if all their coefficients are equal. -/
@@ -181,6 +184,14 @@ theorem coeff_comp_monomial (n : σ →₀ ℕ) : (coeff R n).comp (monomial R n
 theorem coeff_zero (n : σ →₀ ℕ) : coeff R n (0 : MvPowerSeries σ R) = 0 :=
   rfl
 
+theorem eq_zero_iff_forall_coeff_zero {f : MvPowerSeries σ R} :
+    f = 0 ↔ (∀ d : σ →₀ ℕ, coeff R d f = 0) :=
+  MvPowerSeries.ext_iff
+
+theorem ne_zero_iff_exists_coeff_ne_zero (f : MvPowerSeries σ R) :
+    f ≠ 0 ↔ (∃ d : σ →₀ ℕ, coeff R d f ≠ 0) := by
+  simp only [MvPowerSeries.ext_iff, ne_eq, coeff_zero, not_forall]
+
 variable (m n : σ →₀ ℕ) (φ ψ : MvPowerSeries σ R)
 
 instance : One (MvPowerSeries σ R) :=