feat(RingTheory/MvPowerSeries): some inequalities related to order (#33872)

Some inequalities related to order of (mv) power series.

Co-authored-by: WenrongZou <wenrongzou@outlook.com>

Author: WenrongZou

Mathlib/RingTheory/MvPowerSeries/Order.lean

@@ -306,6 +306,20 @@ theorem le_weightedOrder_prod {R : Type*} [CommSemiring R] {ι : Type*} (w : σ
 
 alias weightedOrder_mul_ge := le_weightedOrder_mul
 
+theorem le_weightedOrder_smul {a : R} :
+    f.weightedOrder w ≤ (a • f).weightedOrder w :=
+  le_weightedOrder _ fun i hi => by simp [coeff_eq_zero_of_lt_weightedOrder _ hi]
+
+section
+
+variable {S : Type*} [Semiring S]
+
+theorem le_weightedOrder_map (φ : R →+* S) :
+    f.weightedOrder w ≤ (f.map φ).weightedOrder w :=
+  le_weightedOrder w fun i hi => by simp [coeff_eq_zero_of_lt_weightedOrder _ hi]
+
+end
+
 section Ring
 
 variable {R : Type*} [Ring R] {f g : MvPowerSeries σ R}
@@ -461,17 +475,37 @@ theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*}
     (f : ι → MvPowerSeries σ R) (s : Finset ι) : ∑ i ∈ s, (f i).order ≤ (∏ i ∈ s, f i).order :=
   le_weightedOrder_prod _ _ _
 
-theorem order_ne_zero_iff_constCoeff_eq_zero :
-    f.order ≠ 0 ↔ f.constantCoeff = 0 := by
+theorem one_le_order_iff_constCoeff_eq_zero :
+    1 ≤ f.order ↔ f.constantCoeff = 0 := by
   constructor
   · intro h
     apply coeff_of_lt_order
-    simpa using pos_of_ne_zero h
+    simpa using Order.one_le_iff_pos.mp h
   · intro h
-    refine ENat.one_le_iff_ne_zero.mp <| MvPowerSeries.le_order fun d hd ↦ ?_
+    refine MvPowerSeries.le_order fun d hd ↦ ?_
     rw [Nat.cast_lt_one] at hd
     simp [(degree_eq_zero_iff d).mp hd, h]
 
+theorem order_ne_zero_iff_constCoeff_eq_zero :
+    f.order ≠ 0 ↔ f.constantCoeff = 0 := by
+  rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]
+
+theorem le_order_pow_of_constantCoeff_eq_zero (n : ℕ) (hf : f.constantCoeff = 0) :
+    n ≤ (f ^ n).order := by
+  refine .trans ?_ (le_order_pow n)
+  simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)
+
+theorem le_order_smul {a : R} : f.order ≤ (a • f).order := le_weightedOrder_smul _
+
+section
+
+variable {S : Type*} [Semiring S]
+
+theorem le_order_map (f : R →+* S) {φ : MvPowerSeries σ R} : φ.order ≤ (φ.map f).order :=
+  le_weightedOrder_map _ _
+
+end
+
 section Ring
 
 variable {R : Type*} [Ring R] {f g : MvPowerSeries σ R}

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -178,6 +178,14 @@ theorem order_add_of_order_ne (φ ψ : R⟦X⟧) (h : order φ ≠ order ψ) :
 
 @[deprecated (since := "2025-09-17")] alias order_add_of_order_eq := order_add_of_order_ne
 
+theorem le_order_map {S : Type*} [Semiring S] (f : R →+* S) :
+    φ.order ≤ (φ.map f).order :=
+  le_order _ _ fun i hi => by simp [coeff_of_lt_order i hi]
+
+theorem le_order_smul {a : R} :
+    φ.order ≤ (a • φ).order :=
+  le_order _ φ.order fun i hi => by simp [coeff_of_lt_order i hi]
+
 /-- The order of the product of two formal power series
 is at least the sum of their orders. -/
 theorem le_order_mul (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ) := by
@@ -206,18 +214,27 @@ theorem le_order_prod {R : Type*} [CommSemiring R] {ι : Type*} (φ : ι → R
 
 alias order_mul_ge := le_order_mul
 
-theorem order_ne_zero_iff_constCoeff_eq_zero {φ : R⟦X⟧} :
-    φ.order ≠ 0 ↔ φ.constantCoeff = 0 := by
+theorem one_le_order_iff_constCoeff_eq_zero :
+    1 ≤ φ.order ↔ φ.constantCoeff = 0 := by
   constructor
   · intro h
-    rw [← PowerSeries.coeff_zero_eq_constantCoeff]
+    rw [← coeff_zero_eq_constantCoeff]
     apply coeff_of_lt_order
-    simpa using pos_of_ne_zero h
+    simpa using Order.one_le_iff_pos.mp h
   · intro h
-    refine ENat.one_le_iff_ne_zero.mp <| PowerSeries.le_order _ _ fun d hd ↦ ?_
+    refine le_order _ _ fun d hd ↦ ?_
     rw [Nat.cast_lt_one] at hd
     simp [hd, h]
 
+theorem order_ne_zero_iff_constCoeff_eq_zero {φ : R⟦X⟧} :
+    φ.order ≠ 0 ↔ φ.constantCoeff = 0 := by
+  rw [← ENat.one_le_iff_ne_zero, one_le_order_iff_constCoeff_eq_zero]
+
+theorem le_order_pow_of_constantCoeff_eq_zero (n : ℕ) (hf : φ.constantCoeff = 0) :
+    n ≤ (φ ^ n).order := by
+  refine .trans ?_ (le_order_pow _ n)
+  simpa using le_mul_of_one_le_right' (one_le_order_iff_constCoeff_eq_zero.mpr hf)
+
 /-- The order of the monomial `a*X^n` is infinite if `a = 0` and `n` otherwise. -/
 theorem order_monomial (n : ℕ) (a : R) [Decidable (a = 0)] :
     order (monomial n a) = if a = 0 then (⊤ : ℕ∞) else n := by

Mathlib/RingTheory/PowerSeries/Substitution.lean

@@ -291,6 +291,26 @@ theorem le_order_subst (a : MvPowerSeries τ S) (ha : HasSubst a) (f : PowerSeri
   refine .trans ?_ (MvPowerSeries.le_order_subst (PowerSeries.hasSubst_iff.mp ha) _)
   simp [order_eq_order]
 
+theorem le_order_subst_left {f : MvPowerSeries τ R} {φ : PowerSeries R}
+    (hf : f.constantCoeff = 0) : φ.order ≤ (φ.subst f).order :=
+  .trans (ENat.self_le_mul_left φ.order (f.order_ne_zero_iff_constCoeff_eq_zero.mpr hf))
+    (PowerSeries.le_order_subst f (HasSubst.of_constantCoeff_zero hf) _)
+
+theorem le_order_subst_right {f : MvPowerSeries τ R} {φ : PowerSeries R}
+    (hf : f.constantCoeff = 0) (hφ : φ.constantCoeff = 0) : f.order ≤ (φ.subst f).order :=
+  .trans (ENat.self_le_mul_right _ (order_ne_zero_iff_constCoeff_eq_zero.mpr hφ))
+    (PowerSeries.le_order_subst f (HasSubst.of_constantCoeff_zero hf) _)
+
+theorem le_order_subst_left' {f φ : PowerSeries R} (hf : f.constantCoeff = 0) :
+    φ.order ≤ PowerSeries.order (φ.subst f) := by
+  conv_rhs => rw [order_eq_order]
+  exact le_order_subst_left hf
+
+theorem le_order_subst_right' {f φ : PowerSeries R} (hf : f.constantCoeff = 0)
+    (hφ : φ.constantCoeff = 0) : f.order ≤ PowerSeries.order (φ.subst f) := by
+  simp_rw [order_eq_order]
+  exact le_order_subst_right hf hφ
+
 end
 
 theorem HasSubst.comp