Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(RingTheory/PowerSeries/WellKnown): the power series of 1 / ((1 - x) ^ (d + 1)) with coefficients in a commutative ring S, where d : ℕ. #11255

Closed
wants to merge 12 commits into from
9 changes: 8 additions & 1 deletion Mathlib/Data/Nat/Choose/Sum.lean
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes, Patrick Stevens
Authors: Chris Hughes, Patrick Stevens, Fangming Li
-/
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.Ring
Expand Down Expand Up @@ -235,4 +235,11 @@ theorem sum_antidiagonal_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n
#align finset.sum_antidiagonal_choose_succ_mul Finset.sum_antidiagonal_choose_succ_mul

theorem sum_antidiagonal_choose_add (d n : ℕ) :
(Finset.sum (antidiagonal n) fun ij ↦ (Nat.choose (d + ij.2) d)) =
Nat.choose (d + n) d + Nat.choose (d + n) (succ d) := by
induction' n with n hn
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
· simp only [zero_eq, antidiagonal_zero, sum_singleton, add_zero, choose_self, choose_succ_self]
· rw [Nat.sum_antidiagonal_succ]; simp only [add_right_inj]; exact hn

end Finset
9 changes: 8 additions & 1 deletion Mathlib/RingTheory/PowerSeries/Inverse.lean
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
/-
Copyright (c) 2019 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Kenny Lau
Authors: Johan Commelin, Kenny Lau, Fangming Li
-/

import Mathlib.RingTheory.PowerSeries.Basic
Expand Down Expand Up @@ -198,6 +198,13 @@
MvPowerSeries.mul_inv_rev _ _
#align power_series.mul_inv_rev PowerSeries.mul_inv_rev

theorem pow_inv_eq_inv_pow (φ : PowerSeries k) (d : ℕ) : (φ ^ d)⁻¹ = φ⁻¹ ^ d := by
induction' d with d hd
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
· rw [inv_eq_iff_mul_eq_one]
simp only [Nat.zero_eq, pow_zero, mul_one]
exact ne_zero_of_eq_one rfl
· rw [show φ⁻¹ ^ (d + 1) = φ⁻¹ * (φ⁻¹ ^ d) by rfl, ←hd, ←PowerSeries.mul_inv_rev, pow_succ']

Check failure on line 206 in Mathlib/RingTheory/PowerSeries/Inverse.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/Inverse.lean#L206: ERR_ARR: Missing space after '←'.

Check failure on line 206 in Mathlib/RingTheory/PowerSeries/Inverse.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/Inverse.lean#L206: ERR_ARR: Missing space after '←'.
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved

instance : InvOneClass (PowerSeries k) :=
{ inferInstanceAs <| InvOneClass <| MvPowerSeries Unit k with }

Expand Down
51 changes: 49 additions & 2 deletions Mathlib/RingTheory/PowerSeries/WellKnown.lean
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
/-
Copyright (c) 2020 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov
Authors: Yury G. Kudryashov, Fangming Li
-/
import Mathlib.RingTheory.PowerSeries.Basic
import Mathlib.RingTheory.PowerSeries.Inverse
import Mathlib.Data.Nat.Parity
import Mathlib.Data.Nat.Choose.Sum
import Mathlib.Algebra.BigOperators.NatAntidiagonal

#align_import ring_theory.power_series.well_known from "leanprover-community/mathlib"@"8199f6717c150a7fe91c4534175f4cf99725978f"
Expand Down Expand Up @@ -64,6 +65,52 @@

#align power_series.map_inv_units_sub PowerSeries.map_invUnitsSub

/-- Give `d : ℕ`. The power series for `1 / ((1 - x) ^ (d + 1))`. -/
def invOneSubPow (d : ℕ) : PowerSeries R :=
mk fun n => Nat.choose (d + n) d

theorem invOneSubPow_zero_eq_invUnitsSub_one : invOneSubPow 0 = invUnitsSub (1 : Rˣ) := by
rw [invOneSubPow, invUnitsSub]
simp only [zero_add, Nat.choose_zero_right, Nat.cast_one, one_pow, divp_one]
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved

theorem one_sub_inv_eq_invOneSubPow_zero {k : Type _} [Field k] :
(1 - X : PowerSeries k)⁻¹ = invOneSubPow 0 := Eq.symm <| by
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
rw [@eq_inv_iff_mul_eq_one k _ (invOneSubPow 0) (1 - X) <| show (constantCoeff k)
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
(1 - X) ≠ 0 by simp only [map_sub, map_one, constantCoeff_X, sub_zero, ne_eq, one_ne_zero,
not_false_eq_true], invOneSubPow_zero_eq_invUnitsSub_one]; exact invUnitsSub_mul_sub 1

theorem one_sub_inv {k : Type _} [Field k] :
(1 - X : PowerSeries k)⁻¹ = mk fun (_ : ℕ) => 1 := by
rw [one_sub_inv_eq_invOneSubPow_zero, invOneSubPow]
simp only [zero_add, Nat.choose_zero_right, Nat.cast_one]

theorem one_sub_inv_pow_eq {k : Type _} [Field k] (d : ℕ) :
(1 - X)⁻¹ ^ (d + 1) = (mk fun (n : ℕ) => Nat.choose (d + n) d : PowerSeries k) := by
induction' d with d hd
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
· simp only [Nat.zero_eq, zero_add, pow_one, Nat.choose_zero_right, Nat.cast_one]
exact one_sub_inv
· ring_nf; rw [hd, one_sub_inv, ext_iff]; exact λ n ↦ by
rw [coeff_mul]; simp only [coeff_mk, one_mul]; rw [Nat.succ_add, Nat.choose_succ_succ,
←Finset.sum_antidiagonal_choose_add]; exact (Nat.cast_sum (Finset.antidiagonal n) fun x

Check failure on line 94 in Mathlib/RingTheory/PowerSeries/WellKnown.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/WellKnown.lean#L94: ERR_ARR: Missing space after '←'.

Check failure on line 94 in Mathlib/RingTheory/PowerSeries/WellKnown.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/WellKnown.lean#L94: ERR_ARR: Missing space after '←'.
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
↦ Nat.choose (d + x.2) d).symm

theorem one_sub_inv_pow_eq_invOneSubPow {k : Type _} [Field k] (d : ℕ) :
(1 - X)⁻¹ ^ (d + 1) = (invOneSubPow d : PowerSeries k) := by
rw [one_sub_inv_pow_eq]; rfl

theorem one_sub_pow_inv_eq {k : Type _} [Field k] (d : ℕ) :
((1 - X) ^ (d + 1))⁻¹ = (mk fun (n : ℕ) => Nat.choose (d + n) d : PowerSeries k) := by
rw [←one_sub_inv_pow_eq, pow_inv_eq_inv_pow]

Check failure on line 103 in Mathlib/RingTheory/PowerSeries/WellKnown.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/WellKnown.lean#L103: ERR_ARR: Missing space after '←'.

Check failure on line 103 in Mathlib/RingTheory/PowerSeries/WellKnown.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/WellKnown.lean#L103: ERR_ARR: Missing space after '←'.
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved

theorem one_sub_pow_inv_eq_invOneSubPow {k : Type _} [Field k] (d : ℕ) :
((1 - X) ^ (d + 1))⁻¹ = (invOneSubPow d : PowerSeries k) := by
rw [one_sub_pow_inv_eq]; rfl

theorem invOneSubPow_mul_one_sub_pow {k : Type _} [Field k] (d : ℕ) :
(invOneSubPow d : PowerSeries k) * ((1 - X) ^ (d + 1)) = 1 := by
rw [←one_sub_pow_inv_eq_invOneSubPow]; simp only [map_pow, map_sub, map_one, constantCoeff_X,

Check failure on line 111 in Mathlib/RingTheory/PowerSeries/WellKnown.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/WellKnown.lean#L111: ERR_ARR: Missing space after '←'.

Check failure on line 111 in Mathlib/RingTheory/PowerSeries/WellKnown.lean

View workflow job for this annotation

GitHub Actions / Lint style

Mathlib/RingTheory/PowerSeries/WellKnown.lean#L111: ERR_ARR: Missing space after '←'.
FMLJohn marked this conversation as resolved.
Show resolved Hide resolved
sub_zero, one_pow, ne_eq, one_ne_zero, not_false_eq_true, PowerSeries.inv_mul_cancel]

end Ring

section Field
Expand Down
Loading