feat(RingTheory/MvPowerSeries): some theorems about expand (leanprover-community#33885)

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

Author: WenrongZou

Mathlib/RingTheory/MvPowerSeries/Expand.lean

@@ -78,6 +78,10 @@ theorem expand_substAlgHom {f : σ → MvPowerSeries τ S} (hf : HasSubst f) {φ
     expand p hp (substAlgHom hf φ) = substAlgHom (HasSubst.expand p hp hf) φ := by
   rw [← AlgHom.comp_apply, expand_comp_substAlgHom]
 
+theorem expand_subst {f : σ → MvPowerSeries τ R} (hf : HasSubst f) {φ : MvPowerSeries σ R} :
+    expand p hp (subst f φ) = subst (fun i ↦ (f i).expand p hp) φ := by
+  rw [← substAlgHom_apply hf, expand_substAlgHom, substAlgHom_apply]
+
 end
 
 /- TODO : In the original file of multi variate polynomial, there are two theorem about rename
@@ -109,6 +113,12 @@ theorem coeff_expand_smul (φ : MvPowerSeries σ R) (m : σ →₀ ℕ) :
     rw [this, coeff_monomial, if_neg _, mul_zero]
     simp [nsmul_right_inj hp, hd.symm]
 
+@[simp]
+theorem constantCoeff_expand (φ : MvPowerSeries σ R) :
+    (φ.expand p hp).constantCoeff = φ.constantCoeff := by
+  conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← smul_zero p, coeff_expand_smul]
+  simp
+
 theorem coeff_expand_of_not_dvd (φ : MvPowerSeries σ R) {m : σ →₀ ℕ} {i : σ} (h : ¬ p ∣ m i) :
     (expand p hp φ).coeff m = 0 := by
   classical
@@ -148,6 +158,26 @@ theorem support_expand (φ : MvPowerSeries σ R) :
   rw [Function.mem_support, ← coeff_apply φ, ← coeff_expand_smul p hp, coeff_apply, hc] at hn₁
   contradiction
 
+@[simp]
+theorem order_expand (φ : MvPowerSeries σ R) :
+    (φ.expand p hp).order = p • φ.order := by
+  by_cases! hφ : φ = 0
+  · simpa [hφ] using (ENat.mul_top (by norm_cast)).symm
+  · apply eq_of_le_of_ge
+    · obtain ⟨d, hd₁, hd₂⟩ := exists_coeff_ne_zero_and_order (ne_zero_iff_order_finite.mp hφ)
+      have : p • φ.order = (p • d).degree := by simp [← hd₂]
+      rw [this]
+      exact order_le <| (coeff_expand_smul p hp φ _) ▸ hd₁
+    · refine MvPowerSeries.le_order fun d hd => by
+        by_cases! h : ∀ i, p ∣ d i
+        · obtain ⟨m, hm⟩ : ∃ m, d = p • m := ⟨Finsupp.equivFunOnFinite.symm fun i => d i / p,
+            by ext i; simp [(Nat.mul_div_cancel' (h i))]⟩
+          rw [hm, coeff_expand_smul, coeff_of_lt_order]
+          simp only [hm, map_nsmul, smul_eq_mul, Nat.cast_mul, nsmul_eq_mul] at hd
+          exact lt_of_mul_lt_mul_left' hd
+        · obtain ⟨i, hi⟩ := h
+          exact coeff_expand_of_not_dvd p hp φ hi
+
 section MvPolynomial
 
 /-- For any multivariate polynomial `φ`, then `MvPolynomial.expand p φ` and

Mathlib/RingTheory/MvPowerSeries/Substitution.lean

@@ -283,6 +283,21 @@ theorem constantCoeff_subst (ha : HasSubst a) (f : MvPowerSeries σ R) :
       finsum (fun d ↦ coeff d f • (constantCoeff (d.prod fun s e => (a s) ^ e))) := by
   simp only [← coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]
 
+theorem constantCoeff_subst_eq_zero (ha : HasSubst a) (ha' : ∀ i, (a i).constantCoeff = 0)
+    {f : MvPowerSeries σ R} (hf : f.constantCoeff = 0) :
+    MvPowerSeries.constantCoeff (subst a f) = 0 := by
+  rw [constantCoeff_subst ha, finsum_eq_zero_of_forall_eq_zero]
+  intro d
+  by_cases hd : d = 0
+  · simp [hd, hf]
+  · have : constantCoeff (d.prod fun s e ↦ a s ^ e) = 0 := by
+      obtain ⟨i, hi⟩ : ∃ i : σ, d i ≠ 0 := by
+        by_contra! hc
+        exact hd <| Finsupp.ext hc
+      simpa [map_finsuppProd, ha'] using
+        Finset.prod_eq_zero (i := i) (by simp [hi]) (by simp [zero_pow hi])
+    rw [this, smul_zero]
+
 theorem map_algebraMap_eq_subst_X (f : MvPowerSeries σ R) :
     map (algebraMap R S) f = subst X f := by
   ext e

Mathlib/RingTheory/PowerSeries/Expand.lean

@@ -48,6 +48,9 @@ theorem expand_mul (q : ℕ) (hq : q ≠ 0) (φ : PowerSeries R) :
     φ.expand (p * q) (p.mul_ne_zero hp hq) = (φ.expand q hq).expand p hp :=
   DFunLike.congr_fun (expand_mul_eq_comp p hp q hq) φ
 
+theorem expand_smul (a : R) (φ : PowerSeries R) :
+    expand p hp (a • φ) = a • φ.expand p hp := AlgHom.map_smul_of_tower _ _ _
+
 @[simp]
 theorem expand_X : expand p hp (X (R := R)) = X ^ p :=
   substAlgHom_X (HasSubst.X_pow hp)
@@ -68,28 +71,50 @@ theorem map_expand (f : R →+* S) (φ : PowerSeries R) :
     map f (expand p hp φ) = expand p hp (map f φ) := by
   simp [map, expand, MvPowerSeries.map_expand]
 
+theorem expand_subst {f : MvPowerSeries τ S} [Finite τ] (hf : HasSubst f) (φ : PowerSeries S) :
+    (subst f φ).expand p hp = subst (f.expand p hp) φ := by
+  rw [PowerSeries.subst, MvPowerSeries.expand_subst _ hp (HasSubst.const hf) (φ := φ)]
+  rfl
+
 /- TODO : In the original file of multi variate polynomial, there are two theorem about rename
 here, but we don't have rename for multi variate power series. And for `eval₂Hom`, `eval₂`
 and `aevel`, the expression does't look good. -/
 
-variable (q : ℕ) (hq : 0 < q)
+variable (φ : PowerSeries R) (q : ℕ) (hq : 0 < q)
 
 @[simp]
-theorem coeff_expand_mul (φ : PowerSeries R) (m : ℕ) :
+theorem coeff_expand_mul (m : ℕ) :
     (expand p hp φ).coeff (p * m) = φ.coeff m := by
   rw [coeff, coeff, expand, ← smul_eq_mul, ← Finsupp.smul_single, MvPowerSeries.coeff_expand_smul]
 
-theorem coeff_expand_of_not_dvd (φ : PowerSeries R) {m : ℕ} (h : ¬ p ∣ m) :
+@[simp]
+theorem constantCoeff_expand (φ : PowerSeries R) :
+    (φ.expand p hp).constantCoeff = φ.constantCoeff := by
+  conv_lhs => rw [← coeff_zero_eq_constantCoeff, ← mul_zero p, coeff_expand_mul]
+  simp
+
+theorem coeff_expand_of_not_dvd {m : ℕ} (h : ¬ p ∣ m) :
     (expand p hp φ).coeff m = 0 := by
   rw [coeff, expand, MvPowerSeries.coeff_expand_of_not_dvd (i := ())]
   simpa
 
-theorem support_expand_subset (φ : PowerSeries R) :
+theorem support_expand_subset :
     (expand p hp φ).support ⊆ φ.support.image (p • ·) := by
   rw [expand, MvPowerSeries.support_expand]
 
-theorem support_expand (φ : PowerSeries R) :
+theorem support_expand :
     (expand p hp φ).support = φ.support.image (p • ·) := by
   rw [expand, MvPowerSeries.support_expand]
 
+theorem coeff_expand {n : ℕ} :
+    (φ.expand p hp).coeff n = if p ∣ n then φ.coeff (n / p) else 0 := by
+  split_ifs with h
+  · obtain ⟨q, hq⟩ := h
+    rw [hq, coeff_expand_mul, Nat.mul_div_cancel_left _ (p.pos_of_ne_zero hp)]
+  exact coeff_expand_of_not_dvd p hp _ h
+
+@[simp]
+theorem order_expand : (φ.expand p hp).order = p • φ.order := by
+  simp_rw [expand, order_eq_order, MvPowerSeries.order_expand p hp φ]
+
 end PowerSeries

Mathlib/RingTheory/PowerSeries/Substitution.lean

@@ -222,6 +222,14 @@ theorem constantCoeff_subst (ha : HasSubst a) (f : PowerSeries R) :
       finsum (fun d ↦ coeff d f • MvPowerSeries.constantCoeff (a ^ d)) := by
   simp only [← MvPowerSeries.coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]
 
+theorem constantCoeff_subst_eq_zero (ha : a.constantCoeff = 0) (f : PowerSeries R)
+    (hf : f.constantCoeff = 0) : MvPowerSeries.constantCoeff (subst a f) = 0 := by
+  rw [constantCoeff_subst (HasSubst.of_constantCoeff_zero ha), finsum_eq_zero_of_forall_eq_zero]
+  intro d
+  by_cases hd : d = 0
+  · simp [hd, hf]
+  · simp [ha, zero_pow hd]
+
 theorem map_algebraMap_eq_subst_X (f : R⟦X⟧) :
     map (algebraMap R S) f = subst X f :=
   MvPowerSeries.map_algebraMap_eq_subst_X f