feat(ring_theory/power_series/basic): add api for coeffs of shifts (#…

…11082)

Based on the corresponding API for polynomials

src/ring_theory/power_series/basic.lean

@@ -1000,6 +1000,60 @@ lemma coeff_zero_mul_X (φ : power_series R) : coeff R 0 (φ * X) = 0 := by simp
 
 lemma coeff_zero_X_mul (φ : power_series R) : coeff R 0 (X * φ) = 0 := by simp
 
+-- The following section duplicates the api of `data.polynomial.coeff` and should attempt to keep
+-- up to date with that
+section
+lemma coeff_C_mul_X (x : R) (k n : ℕ) :
+  coeff R n (C R x * X ^ k : power_series R) = if n = k then x else 0 :=
+by simp [X_pow_eq, coeff_monomial]
+
+@[simp]
+theorem coeff_mul_X_pow (p : power_series R) (n d : ℕ) :
+  coeff R (d + n) (p * X ^ n) = coeff R d p :=
+begin
+  rw [coeff_mul, finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one],
+  { rintros ⟨i,j⟩ h1 h2, rw [coeff_X_pow, if_neg, mul_zero], rintro rfl, apply h2,
+    rw [finset.nat.mem_antidiagonal, add_right_cancel_iff] at h1, subst h1 },
+  { exact λ h1, (h1 (finset.nat.mem_antidiagonal.2 rfl)).elim }
+end
+
+@[simp]
+theorem coeff_X_pow_mul (p : power_series R) (n d : ℕ) :
+  coeff R (d + n) (X ^ n * p) = coeff R d p :=
+begin
+  rw [coeff_mul, finset.sum_eq_single (n,d), coeff_X_pow, if_pos rfl, one_mul],
+  { rintros ⟨i,j⟩ h1 h2, rw [coeff_X_pow, if_neg, zero_mul], rintro rfl, apply h2,
+    rw [finset.nat.mem_antidiagonal, add_comm, add_right_cancel_iff] at h1, subst h1 },
+  { rw add_comm,
+    exact λ h1, (h1 (finset.nat.mem_antidiagonal.2 rfl)).elim }
+end
+
+lemma coeff_mul_X_pow' (p : power_series R) (n d : ℕ) :
+  coeff R d (p * X ^ n) = ite (n ≤ d) (coeff R (d - n) p) 0 :=
+begin
+  split_ifs,
+  { rw [← tsub_add_cancel_of_le h, coeff_mul_X_pow, add_tsub_cancel_right] },
+  { refine (coeff_mul _ _ _).trans (finset.sum_eq_zero (λ x hx, _)),
+    rw [coeff_X_pow, if_neg, mul_zero],
+    exact ne_of_lt (lt_of_le_of_lt (nat.le_of_add_le_right
+      (le_of_eq (finset.nat.mem_antidiagonal.mp hx))) (not_le.mp h)) },
+end
+
+lemma coeff_X_pow_mul' (p : power_series R) (n d : ℕ) :
+  coeff R d (X ^ n * p) = ite (n ≤ d) (coeff R (d - n) p) 0 :=
+begin
+  split_ifs,
+  { rw [← tsub_add_cancel_of_le h, coeff_X_pow_mul], simp, },
+  { refine (coeff_mul _ _ _).trans (finset.sum_eq_zero (λ x hx, _)),
+    rw [coeff_X_pow, if_neg, zero_mul],
+    have := finset.nat.mem_antidiagonal.mp hx,
+    rw add_comm at this,
+    exact ne_of_lt (lt_of_le_of_lt (nat.le_of_add_le_right
+      (le_of_eq this)) (not_le.mp h)) },
+end
+
+end
+
 /-- If a formal power series is invertible, then so is its constant coefficient.-/
 lemma is_unit_constant_coeff (φ : power_series R) (h : is_unit φ) :
   is_unit (constant_coeff R φ) :=