Formal power series
This file defines (multivariate) formal power series and develops the basic properties of these objects.
A formal power series is to a polynomial like an infinite sum is to a finite sum.
We provide the natural inclusion from polynomials to formal power series.
Generalities
The file starts with setting up the (semi)ring structure on multivariate power series.
trunc n φ truncates a formal power series to the polynomial
that has the same coefficients as φ, for all m ≤ n, and 0 otherwise.
If the constant coefficient of a formal power series is invertible, then this formal power series is invertible.
Formal power series over a local ring form a local ring.
Formal power series in one variable
We prove that if the ring of coefficients is an integral domain, then formal power series in one variable form an integral domain.
The order of a formal power series φ is the multiplicity of the variable X in φ.
If the coefficients form an integral domain, then order is a valuation
(order_mul, le_order_add).
Implementation notes
In this file we define multivariate formal power series with
variables indexed by σ and coefficients in α as
mv_power_series σ α := (σ →₀ ℕ) → α.
Unfortunately there is not yet enough API to show that they are the completion
of the ring of multivariate polynomials. However, we provide most of the infrastructure
that is needed to do this. Once I-adic completion (topological or algebraic) is available
it should not be hard to fill in the details.
Formal power series in one variable are defined as power_series α := mv_power_series unit α.
This allows us to port a lot of proofs and properties from the multivariate case to the single variable case. However, it means that formal power series are indexed by (unit →₀ ℕ), which is of course canonically isomorphic to ℕ. We then build some glue to treat formal power series as if they are indexed by ℕ. Occasionally this leads to proofs that are uglier than expected.
Multivariate formal power series, where σ is the index set of the variables
and α is the coefficient ring.
Equations
- mv_power_series σ α = ((σ →₀ ℕ) → α)
@[instance]
def
mv_power_series.inhabited
{σ : Type u_1}
{α : Type u_2}
[inhabited α] :
inhabited (mv_power_series σ α)
Equations
- mv_power_series.inhabited = {default := λ (_x : σ →₀ ℕ), inhabited.default α}
@[instance]
def
mv_power_series.has_zero
{σ : Type u_1}
{α : Type u_2}
[has_zero α] :
has_zero (mv_power_series σ α)
Equations
@[instance]
def
mv_power_series.add_monoid
{σ : Type u_1}
{α : Type u_2}
[add_monoid α] :
add_monoid (mv_power_series σ α)
Equations
@[instance]
def
mv_power_series.add_group
{σ : Type u_1}
{α : Type u_2}
[add_group α] :
add_group (mv_power_series σ α)
Equations
@[instance]
@[instance]
Equations
@[instance]
def
mv_power_series.nontrivial
{σ : Type u_1}
{α : Type u_2}
[nontrivial α] :
nontrivial (mv_power_series σ α)
Equations
def
mv_power_series.monomial
{σ : Type u_1}
(α : Type u_2)
[add_monoid α] :
(σ →₀ ℕ) → α →+ mv_power_series σ α
The nth monomial with coefficient a as multivariate formal power series.
def
mv_power_series.coeff
{σ : Type u_1}
(α : Type u_2)
[add_monoid α] :
(σ →₀ ℕ) → mv_power_series σ α →+ α
The nth coefficient of a multivariate formal power series.
Equations
- mv_power_series.coeff α n = {to_fun := λ (φ : mv_power_series σ α), φ n, map_zero' := _, map_add' := _}
@[ext]
theorem
mv_power_series.ext
{σ : Type u_1}
{α : Type u_2}
[add_monoid α]
{φ ψ : mv_power_series σ α} :
(∀ (n : σ →₀ ℕ), ⇑(mv_power_series.coeff α n) φ = ⇑(mv_power_series.coeff α n) ψ) → φ = ψ
Two multivariate formal power series are equal if all their coefficients are equal.
theorem
mv_power_series.ext_iff
{σ : Type u_1}
{α : Type u_2}
[add_monoid α]
{φ ψ : mv_power_series σ α} :
φ = ψ ↔ ∀ (n : σ →₀ ℕ), ⇑(mv_power_series.coeff α n) φ = ⇑(mv_power_series.coeff α n) ψ
Two multivariate formal power series are equal if and only if all their coefficients are equal.
theorem
mv_power_series.coeff_monomial
{σ : Type u_1}
{α : Type u_2}
[add_monoid α]
(m n : σ →₀ ℕ)
(a : α) :
⇑(mv_power_series.coeff α m) (⇑(mv_power_series.monomial α n) a) = ite (m = n) a 0
@[simp]
theorem
mv_power_series.coeff_monomial'
{σ : Type u_1}
{α : Type u_2}
[add_monoid α]
(n : σ →₀ ℕ)
(a : α) :
⇑(mv_power_series.coeff α n) (⇑(mv_power_series.monomial α n) a) = a
@[simp]
theorem
mv_power_series.coeff_comp_monomial
{σ : Type u_1}
{α : Type u_2}
[add_monoid α]
(n : σ →₀ ℕ) :
(mv_power_series.coeff α n).comp (mv_power_series.monomial α n) = add_monoid_hom.id α
@[simp]
theorem
mv_power_series.coeff_zero
{σ : Type u_1}
{α : Type u_2}
[add_monoid α]
(n : σ →₀ ℕ) :
⇑(mv_power_series.coeff α n) 0 = 0
@[instance]
def
mv_power_series.has_one
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
has_one (mv_power_series σ α)
Equations
- mv_power_series.has_one = {one := ⇑(mv_power_series.monomial α 0) 1}
theorem
mv_power_series.coeff_one
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(n : σ →₀ ℕ) :
⇑(mv_power_series.coeff α n) 1 = ite (n = 0) 1 0
theorem
mv_power_series.coeff_zero_one
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
⇑(mv_power_series.coeff α 0) 1 = 1
@[instance]
def
mv_power_series.has_mul
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
has_mul (mv_power_series σ α)
theorem
mv_power_series.coeff_mul
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(n : σ →₀ ℕ)
(φ ψ : mv_power_series σ α) :
⇑(mv_power_series.coeff α n) (φ * ψ) = n.antidiagonal.support.sum (λ (p : (σ →₀ ℕ) × (σ →₀ ℕ)), ⇑(mv_power_series.coeff α p.fst) φ * ⇑(mv_power_series.coeff α p.snd) ψ)
theorem
mv_power_series.zero_mul
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α) :
theorem
mv_power_series.mul_zero
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α) :
theorem
mv_power_series.one_mul
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α) :
theorem
mv_power_series.mul_one
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α) :
theorem
mv_power_series.mul_add
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ₁ φ₂ φ₃ : mv_power_series σ α) :
theorem
mv_power_series.add_mul
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ₁ φ₂ φ₃ : mv_power_series σ α) :
theorem
mv_power_series.mul_assoc
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ₁ φ₂ φ₃ : mv_power_series σ α) :
@[instance]
def
mv_power_series.semiring
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
semiring (mv_power_series σ α)
Equations
- mv_power_series.semiring = {add := add_comm_monoid.add mv_power_series.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero mv_power_series.add_comm_monoid, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul mv_power_series.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[instance]
def
mv_power_series.comm_semiring
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α] :
comm_semiring (mv_power_series σ α)
Equations
- mv_power_series.comm_semiring = {add := semiring.add mv_power_series.semiring, add_assoc := _, zero := semiring.zero mv_power_series.semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul mv_power_series.semiring, mul_assoc := _, one := semiring.one mv_power_series.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Equations
- mv_power_series.ring = {add := semiring.add mv_power_series.semiring, add_assoc := _, zero := semiring.zero mv_power_series.semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg mv_power_series.add_comm_group, add_left_neg := _, add_comm := _, mul := semiring.mul mv_power_series.semiring, mul_assoc := _, one := semiring.one mv_power_series.semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}
@[instance]
def
mv_power_series.comm_ring
{σ : Type u_1}
{α : Type u_2}
[comm_ring α] :
comm_ring (mv_power_series σ α)
Equations
- mv_power_series.comm_ring = {add := comm_semiring.add mv_power_series.comm_semiring, add_assoc := _, zero := comm_semiring.zero mv_power_series.comm_semiring, zero_add := _, add_zero := _, neg := add_comm_group.neg mv_power_series.add_comm_group, add_left_neg := _, add_comm := _, mul := comm_semiring.mul mv_power_series.comm_semiring, mul_assoc := _, one := comm_semiring.one mv_power_series.comm_semiring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}
theorem
mv_power_series.monomial_mul_monomial
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(m n : σ →₀ ℕ)
(a b : α) :
⇑(mv_power_series.monomial α m) a * ⇑(mv_power_series.monomial α n) b = ⇑(mv_power_series.monomial α (m + n)) (a * b)
The constant multivariate formal power series.
Equations
- mv_power_series.C σ α = {to_fun := (mv_power_series.monomial α 0).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
mv_power_series.monomial_zero_eq_C
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
mv_power_series.monomial α 0 = ↑(mv_power_series.C σ α)
theorem
mv_power_series.monomial_zero_eq_C_apply
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(a : α) :
⇑(mv_power_series.monomial α 0) a = ⇑(mv_power_series.C σ α) a
theorem
mv_power_series.coeff_C
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(n : σ →₀ ℕ)
(a : α) :
⇑(mv_power_series.coeff α n) (⇑(mv_power_series.C σ α) a) = ite (n = 0) a 0
theorem
mv_power_series.coeff_zero_C
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(a : α) :
⇑(mv_power_series.coeff α 0) (⇑(mv_power_series.C σ α) a) = a
The variables of the multivariate formal power series ring.
Equations
- mv_power_series.X s = ⇑(mv_power_series.monomial α (finsupp.single s 1)) 1
theorem
mv_power_series.coeff_X
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(n : σ →₀ ℕ)
(s : σ) :
⇑(mv_power_series.coeff α n) (mv_power_series.X s) = ite (n = finsupp.single s 1) 1 0
theorem
mv_power_series.coeff_index_single_X
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(s t : σ) :
⇑(mv_power_series.coeff α (finsupp.single t 1)) (mv_power_series.X s) = ite (t = s) 1 0
@[simp]
theorem
mv_power_series.coeff_index_single_self_X
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(s : σ) :
⇑(mv_power_series.coeff α (finsupp.single s 1)) (mv_power_series.X s) = 1
theorem
mv_power_series.coeff_zero_X
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(s : σ) :
⇑(mv_power_series.coeff α 0) (mv_power_series.X s) = 0
theorem
mv_power_series.X_def
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(s : σ) :
mv_power_series.X s = ⇑(mv_power_series.monomial α (finsupp.single s 1)) 1
theorem
mv_power_series.X_pow_eq
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(s : σ)
(n : ℕ) :
mv_power_series.X s ^ n = ⇑(mv_power_series.monomial α (finsupp.single s n)) 1
theorem
mv_power_series.coeff_X_pow
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(m : σ →₀ ℕ)
(s : σ)
(n : ℕ) :
⇑(mv_power_series.coeff α m) (mv_power_series.X s ^ n) = ite (m = finsupp.single s n) 1 0
@[simp]
theorem
mv_power_series.coeff_mul_C
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(n : σ →₀ ℕ)
(φ : mv_power_series σ α)
(a : α) :
⇑(mv_power_series.coeff α n) (φ * ⇑(mv_power_series.C σ α) a) = ⇑(mv_power_series.coeff α n) φ * a
theorem
mv_power_series.coeff_zero_mul_X
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α)
(s : σ) :
⇑(mv_power_series.coeff α 0) (φ * mv_power_series.X s) = 0
def
mv_power_series.constant_coeff
(σ : Type u_1)
(α : Type u_2)
[semiring α] :
mv_power_series σ α →+* α
The constant coefficient of a formal power series.
Equations
- mv_power_series.constant_coeff σ α = {to_fun := ⇑(mv_power_series.coeff α 0), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
mv_power_series.coeff_zero_eq_constant_coeff_apply
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α) :
⇑(mv_power_series.coeff α 0) φ = ⇑(mv_power_series.constant_coeff σ α) φ
@[simp]
theorem
mv_power_series.constant_coeff_C
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(a : α) :
⇑(mv_power_series.constant_coeff σ α) (⇑(mv_power_series.C σ α) a) = a
@[simp]
theorem
mv_power_series.constant_coeff_comp_C
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
(mv_power_series.constant_coeff σ α).comp (mv_power_series.C σ α) = ring_hom.id α
@[simp]
theorem
mv_power_series.constant_coeff_zero
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
⇑(mv_power_series.constant_coeff σ α) 0 = 0
@[simp]
theorem
mv_power_series.constant_coeff_one
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
⇑(mv_power_series.constant_coeff σ α) 1 = 1
@[simp]
theorem
mv_power_series.constant_coeff_X
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(s : σ) :
⇑(mv_power_series.constant_coeff σ α) (mv_power_series.X s) = 0
theorem
mv_power_series.is_unit_constant_coeff
{σ : Type u_1}
{α : Type u_2}
[semiring α]
(φ : mv_power_series σ α) :
is_unit φ → is_unit (⇑(mv_power_series.constant_coeff σ α) φ)
If a multivariate formal power series is invertible, then so is its constant coefficient.
@[instance]
def
mv_power_series.semimodule
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
semimodule α (mv_power_series σ α)
Equations
- mv_power_series.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (a : α) (φ : mv_power_series σ α), ⇑(mv_power_series.C σ α) a * φ}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
theorem
mv_power_series.X_inj
{σ : Type u_1}
{α : Type u_2}
[semiring α]
[nontrivial α]
{s t : σ} :
mv_power_series.X s = mv_power_series.X t ↔ s = t
@[instance]
def
mv_power_series.algebra
{σ : Type u_1}
{α : Type u_2}
[comm_ring α] :
algebra α (mv_power_series σ α)
Equations
- mv_power_series.algebra = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := (mv_power_series.C σ α).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
def
mv_power_series.map
(σ : Type u_1)
{α : Type u_2}
{β : Type u_3}
[semiring α]
[semiring β] :
(α →+* β) → mv_power_series σ α →+* mv_power_series σ β
The map between multivariate formal power series induced by a map on the coefficients.
Equations
- mv_power_series.map σ f = {to_fun := λ (φ : mv_power_series σ α) (n : σ →₀ ℕ), ⇑f (⇑(mv_power_series.coeff α n) φ), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
@[simp]
theorem
mv_power_series.map_id
{σ : Type u_1}
{α : Type u_2}
[semiring α] :
mv_power_series.map σ (ring_hom.id α) = ring_hom.id (mv_power_series σ α)
theorem
mv_power_series.map_comp
{σ : Type u_1}
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[semiring α]
[semiring β]
[semiring γ]
(f : α →+* β)
(g : β →+* γ) :
mv_power_series.map σ (g.comp f) = (mv_power_series.map σ g).comp (mv_power_series.map σ f)
@[simp]
theorem
mv_power_series.coeff_map
{σ : Type u_1}
{α : Type u_2}
{β : Type u_3}
[semiring α]
[semiring β]
(f : α →+* β)
(n : σ →₀ ℕ)
(φ : mv_power_series σ α) :
⇑(mv_power_series.coeff β n) (⇑(mv_power_series.map σ f) φ) = ⇑f (⇑(mv_power_series.coeff α n) φ)
@[simp]
theorem
mv_power_series.constant_coeff_map
{σ : Type u_1}
{α : Type u_2}
{β : Type u_3}
[semiring α]
[semiring β]
(f : α →+* β)
(φ : mv_power_series σ α) :
⇑(mv_power_series.constant_coeff σ β) (⇑(mv_power_series.map σ f) φ) = ⇑f (⇑(mv_power_series.constant_coeff σ α) φ)
def
mv_power_series.trunc_fun
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α] :
(σ →₀ ℕ) → mv_power_series σ α → mv_polynomial σ α
Auxiliary definition for the truncation function.
Equations
- mv_power_series.trunc_fun n φ = {support := finset.filter (λ (m : σ →₀ ℕ), ⇑(mv_power_series.coeff α m) φ ≠ 0) (finset.image prod.fst n.antidiagonal.support), to_fun := λ (m : σ →₀ ℕ), ite (m ≤ n) (⇑(mv_power_series.coeff α m) φ) 0, mem_support_to_fun := _}
def
mv_power_series.trunc
{σ : Type u_1}
(α : Type u_2)
[comm_semiring α] :
(σ →₀ ℕ) → mv_power_series σ α →+ mv_polynomial σ α
The nth truncation of a multivariate formal power series to a multivariate polynomial
Equations
- mv_power_series.trunc α n = {to_fun := mv_power_series.trunc_fun n, map_zero' := _, map_add' := _}
theorem
mv_power_series.coeff_trunc
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(n m : σ →₀ ℕ)
(φ : mv_power_series σ α) :
mv_polynomial.coeff m (⇑(mv_power_series.trunc α n) φ) = ite (m ≤ n) (⇑(mv_power_series.coeff α m) φ) 0
@[simp]
theorem
mv_power_series.trunc_one
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(n : σ →₀ ℕ) :
⇑(mv_power_series.trunc α n) 1 = 1
@[simp]
theorem
mv_power_series.trunc_C
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(n : σ →₀ ℕ)
(a : α) :
⇑(mv_power_series.trunc α n) (⇑(mv_power_series.C σ α) a) = ⇑mv_polynomial.C a
theorem
mv_power_series.X_pow_dvd_iff
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
{s : σ}
{n : ℕ}
{φ : mv_power_series σ α} :
theorem
mv_power_series.X_dvd_iff
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
{s : σ}
{φ : mv_power_series σ α} :
mv_power_series.X s ∣ φ ↔ ∀ (m : σ →₀ ℕ), ⇑m s = 0 → ⇑(mv_power_series.coeff α m) φ = 0
def
mv_power_series.inv.aux
{σ : Type u_1}
{α : Type u_2}
[ring α] :
α → mv_power_series σ α → mv_power_series σ α
Auxiliary definition that unifies
the totalised inverse formal power series (_)⁻¹ and
the inverse formal power series that depends on
an inverse of the constant coefficient inv_of_unit.
theorem
mv_power_series.coeff_inv_aux
{σ : Type u_1}
{α : Type u_2}
[ring α]
(n : σ →₀ ℕ)
(a : α)
(φ : mv_power_series σ α) :
⇑(mv_power_series.coeff α n) (mv_power_series.inv.aux a φ) = ite (n = 0) a (-a * n.antidiagonal.support.sum (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)), ite (x.snd < n) (⇑(mv_power_series.coeff α x.fst) φ * ⇑(mv_power_series.coeff α x.snd) (mv_power_series.inv.aux a φ)) 0))
def
mv_power_series.inv_of_unit
{σ : Type u_1}
{α : Type u_2}
[ring α] :
mv_power_series σ α → units α → mv_power_series σ α
A multivariate formal power series is invertible if the constant coefficient is invertible.
Equations
- φ.inv_of_unit u = mv_power_series.inv.aux ↑u⁻¹ φ
theorem
mv_power_series.coeff_inv_of_unit
{σ : Type u_1}
{α : Type u_2}
[ring α]
(n : σ →₀ ℕ)
(φ : mv_power_series σ α)
(u : units α) :
@[simp]
theorem
mv_power_series.constant_coeff_inv_of_unit
{σ : Type u_1}
{α : Type u_2}
[ring α]
(φ : mv_power_series σ α)
(u : units α) :
⇑(mv_power_series.constant_coeff σ α) (φ.inv_of_unit u) = ↑u⁻¹
theorem
mv_power_series.mul_inv_of_unit
{σ : Type u_1}
{α : Type u_2}
[ring α]
(φ : mv_power_series σ α)
(u : units α) :
⇑(mv_power_series.constant_coeff σ α) φ = ↑u → φ * φ.inv_of_unit u = 1
@[instance]
def
mv_power_series.is_local_ring
{σ : Type u_1}
{α : Type u_2}
[comm_ring α]
[local_ring α] :
local_ring (mv_power_series σ α)
Multivariate formal power series over a local ring form a local ring.
Equations
@[instance]
def
mv_power_series.map.is_local_ring_hom
{σ : Type u_1}
{α : Type u_2}
{β : Type u_3}
[comm_ring α]
[comm_ring β]
(f : α →+* β)
[is_local_ring_hom f] :
The map A[[X]] → B[[X]] induced by a local ring hom A → B is local
Equations
- _ = _
@[instance]
def
mv_power_series.local_ring
{σ : Type u_1}
{α : Type u_2}
[comm_ring α]
[local_ring α] :
local_ring (mv_power_series σ α)
Equations
def
mv_power_series.inv
{σ : Type u_1}
{α : Type u_2}
[field α] :
mv_power_series σ α → mv_power_series σ α
The inverse 1/f of a multivariable power series f over a field
Equations
- φ.inv = mv_power_series.inv.aux (⇑(mv_power_series.constant_coeff σ α) φ)⁻¹ φ
@[instance]
def
mv_power_series.has_inv
{σ : Type u_1}
{α : Type u_2}
[field α] :
has_inv (mv_power_series σ α)
Equations
- mv_power_series.has_inv = {inv := mv_power_series.inv _inst_1}
theorem
mv_power_series.coeff_inv
{σ : Type u_1}
{α : Type u_2}
[field α]
(n : σ →₀ ℕ)
(φ : mv_power_series σ α) :
@[simp]
theorem
mv_power_series.constant_coeff_inv
{σ : Type u_1}
{α : Type u_2}
[field α]
(φ : mv_power_series σ α) :
⇑(mv_power_series.constant_coeff σ α) φ⁻¹ = (⇑(mv_power_series.constant_coeff σ α) φ)⁻¹
theorem
mv_power_series.inv_eq_zero
{σ : Type u_1}
{α : Type u_2}
[field α]
{φ : mv_power_series σ α} :
@[simp]
theorem
mv_power_series.inv_of_unit_eq
{σ : Type u_1}
{α : Type u_2}
[field α]
(φ : mv_power_series σ α)
(h : ⇑(mv_power_series.constant_coeff σ α) φ ≠ 0) :
φ.inv_of_unit (units.mk0 (⇑(mv_power_series.constant_coeff σ α) φ) h) = φ⁻¹
@[simp]
theorem
mv_power_series.inv_of_unit_eq'
{σ : Type u_1}
{α : Type u_2}
[field α]
(φ : mv_power_series σ α)
(u : units α) :
⇑(mv_power_series.constant_coeff σ α) φ = ↑u → φ.inv_of_unit u = φ⁻¹
@[simp]
theorem
mv_power_series.mul_inv
{σ : Type u_1}
{α : Type u_2}
[field α]
(φ : mv_power_series σ α) :
@[simp]
theorem
mv_power_series.inv_mul
{σ : Type u_1}
{α : Type u_2}
[field α]
(φ : mv_power_series σ α) :
@[instance]
def
mv_polynomial.coe_to_mv_power_series
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α] :
has_coe (mv_polynomial σ α) (mv_power_series σ α)
The natural inclusion from multivariate polynomials into multivariate formal power series.
Equations
- mv_polynomial.coe_to_mv_power_series = {coe := λ (φ : mv_polynomial σ α) (n : σ →₀ ℕ), mv_polynomial.coeff n φ}
@[simp]
theorem
mv_polynomial.coeff_coe
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(φ : mv_polynomial σ α)
(n : σ →₀ ℕ) :
⇑(mv_power_series.coeff α n) ↑φ = mv_polynomial.coeff n φ
@[simp]
theorem
mv_polynomial.coe_monomial
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(n : σ →₀ ℕ)
(a : α) :
↑(mv_polynomial.monomial n a) = ⇑(mv_power_series.monomial α n) a
@[simp]
@[simp]
@[simp]
theorem
mv_polynomial.coe_add
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(φ ψ : mv_polynomial σ α) :
@[simp]
theorem
mv_polynomial.coe_mul
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(φ ψ : mv_polynomial σ α) :
@[simp]
theorem
mv_polynomial.coe_C
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α]
(a : α) :
↑(⇑mv_polynomial.C a) = ⇑(mv_power_series.C σ α) a
@[simp]
def
mv_polynomial.coe_to_mv_power_series.ring_hom
{σ : Type u_1}
{α : Type u_2}
[comm_semiring α] :
mv_polynomial σ α →+* mv_power_series σ α
The coercion from multivariable polynomials to multivariable power series as a ring homomorphism.
Equations
- mv_polynomial.coe_to_mv_power_series.ring_hom = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Formal power series over the coefficient ring α.
Equations
@[instance]
Equations
@[instance]
@[instance]
Equations
@[instance]
@[instance]
@[instance]
Equations
@[instance]
@[instance]
Equations
@[instance]
Equations
@[instance]
@[instance]
@[instance]
Equations
The nth coefficient of a formal power series.
Equations
- power_series.coeff α n = mv_power_series.coeff α (finsupp.single () n)
The nth monomial with coefficient a as formal power series.
Equations
theorem
power_series.coeff_def
{α : Type u_1}
[add_monoid α]
{s : unit →₀ ℕ}
{n : ℕ} :
⇑s () = n → power_series.coeff α n = mv_power_series.coeff α s
@[ext]
theorem
power_series.ext
{α : Type u_1}
[add_monoid α]
{φ ψ : power_series α} :
(∀ (n : ℕ), ⇑(power_series.coeff α n) φ = ⇑(power_series.coeff α n) ψ) → φ = ψ
Two formal power series are equal if all their coefficients are equal.
theorem
power_series.ext_iff
{α : Type u_1}
[add_monoid α]
{φ ψ : power_series α} :
φ = ψ ↔ ∀ (n : ℕ), ⇑(power_series.coeff α n) φ = ⇑(power_series.coeff α n) ψ
Two formal power series are equal if all their coefficients are equal.
Constructor for formal power series.
@[simp]
theorem
power_series.coeff_mk
{α : Type u_1}
[add_monoid α]
(n : ℕ)
(f : ℕ → α) :
⇑(power_series.coeff α n) (power_series.mk f) = f n
theorem
power_series.coeff_monomial
{α : Type u_1}
[add_monoid α]
(m n : ℕ)
(a : α) :
⇑(power_series.coeff α m) (⇑(power_series.monomial α n) a) = ite (m = n) a 0
theorem
power_series.monomial_eq_mk
{α : Type u_1}
[add_monoid α]
(n : ℕ)
(a : α) :
⇑(power_series.monomial α n) a = power_series.mk (λ (m : ℕ), ite (m = n) a 0)
@[simp]
theorem
power_series.coeff_monomial'
{α : Type u_1}
[add_monoid α]
(n : ℕ)
(a : α) :
⇑(power_series.coeff α n) (⇑(power_series.monomial α n) a) = a
@[simp]
theorem
power_series.coeff_comp_monomial
{α : Type u_1}
[add_monoid α]
(n : ℕ) :
(power_series.coeff α n).comp (power_series.monomial α n) = add_monoid_hom.id α
The constant coefficient of a formal power series.
Equations
The constant formal power series.
Equations
The variable of the formal power series ring.
Equations
@[simp]
theorem
power_series.coeff_zero_eq_constant_coeff_apply
{α : Type u_1}
[semiring α]
(φ : power_series α) :
⇑(power_series.coeff α 0) φ = ⇑(power_series.constant_coeff α) φ
@[simp]
theorem
power_series.monomial_zero_eq_C
{α : Type u_1}
[semiring α] :
power_series.monomial α 0 = ↑(power_series.C α)
theorem
power_series.monomial_zero_eq_C_apply
{α : Type u_1}
[semiring α]
(a : α) :
⇑(power_series.monomial α 0) a = ⇑(power_series.C α) a
theorem
power_series.coeff_C
{α : Type u_1}
[semiring α]
(n : ℕ)
(a : α) :
⇑(power_series.coeff α n) (⇑(power_series.C α) a) = ite (n = 0) a 0
theorem
power_series.coeff_zero_C
{α : Type u_1}
[semiring α]
(a : α) :
⇑(power_series.coeff α 0) (⇑(power_series.C α) a) = a
theorem
power_series.X_eq
{α : Type u_1}
[semiring α] :
power_series.X = ⇑(power_series.monomial α 1) 1
theorem
power_series.coeff_X
{α : Type u_1}
[semiring α]
(n : ℕ) :
⇑(power_series.coeff α n) power_series.X = ite (n = 1) 1 0
theorem
power_series.coeff_zero_X
{α : Type u_1}
[semiring α] :
⇑(power_series.coeff α 0) power_series.X = 0
@[simp]
theorem
power_series.coeff_one_X
{α : Type u_1}
[semiring α] :
⇑(power_series.coeff α 1) power_series.X = 1
theorem
power_series.X_pow_eq
{α : Type u_1}
[semiring α]
(n : ℕ) :
power_series.X ^ n = ⇑(power_series.monomial α n) 1
theorem
power_series.coeff_X_pow
{α : Type u_1}
[semiring α]
(m n : ℕ) :
⇑(power_series.coeff α m) (power_series.X ^ n) = ite (m = n) 1 0
@[simp]
theorem
power_series.coeff_X_pow_self
{α : Type u_1}
[semiring α]
(n : ℕ) :
⇑(power_series.coeff α n) (power_series.X ^ n) = 1
@[simp]
theorem
power_series.coeff_one
{α : Type u_1}
[semiring α]
(n : ℕ) :
⇑(power_series.coeff α n) 1 = ite (n = 0) 1 0
theorem
power_series.coeff_mul
{α : Type u_1}
[semiring α]
(n : ℕ)
(φ ψ : power_series α) :
⇑(power_series.coeff α n) (φ * ψ) = (finset.nat.antidiagonal n).sum (λ (p : ℕ × ℕ), ⇑(power_series.coeff α p.fst) φ * ⇑(power_series.coeff α p.snd) ψ)
@[simp]
theorem
power_series.coeff_mul_C
{α : Type u_1}
[semiring α]
(n : ℕ)
(φ : power_series α)
(a : α) :
⇑(power_series.coeff α n) (φ * ⇑(power_series.C α) a) = ⇑(power_series.coeff α n) φ * a
@[simp]
theorem
power_series.coeff_succ_mul_X
{α : Type u_1}
[semiring α]
(n : ℕ)
(φ : power_series α) :
⇑(power_series.coeff α (n + 1)) (φ * power_series.X) = ⇑(power_series.coeff α n) φ
@[simp]
theorem
power_series.constant_coeff_C
{α : Type u_1}
[semiring α]
(a : α) :
⇑(power_series.constant_coeff α) (⇑(power_series.C α) a) = a
@[simp]
@[simp]
theorem
power_series.constant_coeff_zero
{α : Type u_1}
[semiring α] :
⇑(power_series.constant_coeff α) 0 = 0
@[simp]
theorem
power_series.constant_coeff_one
{α : Type u_1}
[semiring α] :
⇑(power_series.constant_coeff α) 1 = 1
@[simp]
theorem
power_series.coeff_zero_mul_X
{α : Type u_1}
[semiring α]
(φ : power_series α) :
⇑(power_series.coeff α 0) (φ * power_series.X) = 0
theorem
power_series.is_unit_constant_coeff
{α : Type u_1}
[semiring α]
(φ : power_series α) :
is_unit φ → is_unit (⇑(power_series.constant_coeff α) φ)
If a formal power series is invertible, then so is its constant coefficient.
def
power_series.map
{α : Type u_1}
[semiring α]
{β : Type u_2}
[semiring β] :
(α →+* β) → power_series α →+* power_series β
The map between formal power series induced by a map on the coefficients.
Equations
@[simp]
theorem
power_series.map_comp
{α : Type u_1}
[semiring α]
{β : Type u_2}
{γ : Type u_3}
[semiring β]
[semiring γ]
(f : α →+* β)
(g : β →+* γ) :
power_series.map (g.comp f) = (power_series.map g).comp (power_series.map f)
@[simp]
theorem
power_series.coeff_map
{α : Type u_1}
[semiring α]
{β : Type u_2}
[semiring β]
(f : α →+* β)
(n : ℕ)
(φ : power_series α) :
⇑(power_series.coeff β n) (⇑(power_series.map f) φ) = ⇑f (⇑(power_series.coeff α n) φ)
theorem
power_series.X_pow_dvd_iff
{α : Type u_1}
[comm_semiring α]
{n : ℕ}
{φ : power_series α} :
power_series.X ^ n ∣ φ ↔ ∀ (m : ℕ), m < n → ⇑(power_series.coeff α m) φ = 0
theorem
power_series.X_dvd_iff
{α : Type u_1}
[comm_semiring α]
{φ : power_series α} :
power_series.X ∣ φ ↔ ⇑(power_series.constant_coeff α) φ = 0
The nth truncation of a formal power series to a polynomial
Equations
- power_series.trunc n φ = {support := finset.filter (λ (m : ℕ), ⇑(power_series.coeff α m) φ ≠ 0) (finset.image prod.fst (finset.nat.antidiagonal n)), to_fun := λ (m : ℕ), ite (m ≤ n) (⇑(power_series.coeff α m) φ) 0, mem_support_to_fun := _}
theorem
power_series.coeff_trunc
{α : Type u_1}
[comm_semiring α]
(m n : ℕ)
(φ : power_series α) :
(power_series.trunc n φ).coeff m = ite (m ≤ n) (⇑(power_series.coeff α m) φ) 0
@[simp]
theorem
power_series.trunc_zero
{α : Type u_1}
[comm_semiring α]
(n : ℕ) :
power_series.trunc n 0 = 0
@[simp]
theorem
power_series.trunc_one
{α : Type u_1}
[comm_semiring α]
(n : ℕ) :
power_series.trunc n 1 = 1
@[simp]
theorem
power_series.trunc_C
{α : Type u_1}
[comm_semiring α]
(n : ℕ)
(a : α) :
power_series.trunc n (⇑(power_series.C α) a) = ⇑polynomial.C a
@[simp]
theorem
power_series.trunc_add
{α : Type u_1}
[comm_semiring α]
(n : ℕ)
(φ ψ : power_series α) :
power_series.trunc n (φ + ψ) = power_series.trunc n φ + power_series.trunc n ψ
Auxiliary function used for computing inverse of a power series
Equations
theorem
power_series.coeff_inv_aux
{α : Type u_1}
[ring α]
(n : ℕ)
(a : α)
(φ : power_series α) :
⇑(power_series.coeff α n) (power_series.inv.aux a φ) = ite (n = 0) a (-a * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ), ite (x.snd < n) (⇑(power_series.coeff α x.fst) φ * ⇑(power_series.coeff α x.snd) (power_series.inv.aux a φ)) 0))
A formal power series is invertible if the constant coefficient is invertible.
Equations
- φ.inv_of_unit u = mv_power_series.inv_of_unit φ u
theorem
power_series.coeff_inv_of_unit
{α : Type u_1}
[ring α]
(n : ℕ)
(φ : power_series α)
(u : units α) :
⇑(power_series.coeff α n) (φ.inv_of_unit u) = ite (n = 0) ↑u⁻¹ (-↑u⁻¹ * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ), ite (x.snd < n) (⇑(power_series.coeff α x.fst) φ * ⇑(power_series.coeff α x.snd) (φ.inv_of_unit u)) 0))
@[simp]
theorem
power_series.constant_coeff_inv_of_unit
{α : Type u_1}
[ring α]
(φ : power_series α)
(u : units α) :
⇑(power_series.constant_coeff α) (φ.inv_of_unit u) = ↑u⁻¹
theorem
power_series.mul_inv_of_unit
{α : Type u_1}
[ring α]
(φ : power_series α)
(u : units α) :
⇑(power_series.constant_coeff α) φ = ↑u → φ * φ.inv_of_unit u = 1
theorem
power_series.eq_zero_or_eq_zero_of_mul_eq_zero
{α : Type u_1}
[integral_domain α]
(φ ψ : power_series α) :
@[instance]
Equations
- power_series.integral_domain = {add := comm_ring.add power_series.comm_ring, add_assoc := _, zero := comm_ring.zero power_series.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg power_series.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul power_series.comm_ring, mul_assoc := _, one := comm_ring.one power_series.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
The ideal spanned by the variable in the power series ring over an integral domain is a prime ideal.
The variable of the power series ring over an integral domain is prime.
@[instance]
def
power_series.map.is_local_ring_hom
{α : Type u_1}
{β : Type u_2}
[comm_ring α]
[comm_ring β]
(f : α →+* β)
[is_local_ring_hom f] :
Equations
- _ = _
@[instance]
The inverse 1/f of a power series f defined over a field
Equations
@[instance]
Equations
- power_series.has_inv = {inv := power_series.inv _inst_1}
theorem
power_series.inv_eq_inv_aux
{α : Type u_1}
[field α]
(φ : power_series α) :
φ⁻¹ = power_series.inv.aux (⇑(power_series.constant_coeff α) φ)⁻¹ φ
theorem
power_series.coeff_inv
{α : Type u_1}
[field α]
(n : ℕ)
(φ : power_series α) :
⇑(power_series.coeff α n) φ⁻¹ = ite (n = 0) (⇑(power_series.constant_coeff α) φ)⁻¹ (-(⇑(power_series.constant_coeff α) φ)⁻¹ * (finset.nat.antidiagonal n).sum (λ (x : ℕ × ℕ), ite (x.snd < n) (⇑(power_series.coeff α x.fst) φ * ⇑(power_series.coeff α x.snd) φ⁻¹) 0))
@[simp]
theorem
power_series.constant_coeff_inv
{α : Type u_1}
[field α]
(φ : power_series α) :
⇑(power_series.constant_coeff α) φ⁻¹ = (⇑(power_series.constant_coeff α) φ)⁻¹
@[simp]
theorem
power_series.inv_of_unit_eq
{α : Type u_1}
[field α]
(φ : power_series α)
(h : ⇑(power_series.constant_coeff α) φ ≠ 0) :
φ.inv_of_unit (units.mk0 (⇑(power_series.constant_coeff α) φ) h) = φ⁻¹
@[simp]
theorem
power_series.inv_of_unit_eq'
{α : Type u_1}
[field α]
(φ : power_series α)
(u : units α) :
⇑(power_series.constant_coeff α) φ = ↑u → φ.inv_of_unit u = φ⁻¹
@[simp]
@[simp]
The order of a formal power series φ is the smallest n : enat
such that X^n divides φ. The order is ⊤ if and only if φ = 0.
Equations
theorem
power_series.order_finite_of_coeff_ne_zero
{α : Type u_1}
[comm_semiring α]
(φ : power_series α) :
theorem
power_series.coeff_order
{α : Type u_1}
[comm_semiring α]
(φ : power_series α)
(h : φ.order.dom) :
⇑(power_series.coeff α (φ.order.get h)) φ ≠ 0
If the order of a formal power series is finite, then the coefficient indexed by the order is nonzero.
If the nth coefficient of a formal power series is nonzero,
then the order of the power series is less than or equal to n.
theorem
power_series.coeff_of_lt_order
{α : Type u_1}
[comm_semiring α]
(φ : power_series α)
(n : ℕ) :
The nth coefficient of a formal power series is 0 if n is strictly
smaller than the order of the power series.
The 0 power series is the unique power series with infinite order.
@[simp]
The order of the 0 power series is infinite.
The order of a formal power series is at least n if
the ith coefficient is 0 for all i < n.
The order of a formal power series is at least n if
the ith coefficient is 0 for all i < n.
The order of a formal power series is exactly n if the nth coefficient is nonzero,
and the ith coefficient is 0 for all i < n.
The order of a formal power series is exactly n if the nth coefficient is nonzero,
and the ith coefficient is 0 for all i < n.
The order of the sum of two formal power series is at least the minimum of their orders.
theorem
power_series.order_add_of_order_eq
{α : Type u_1}
[comm_semiring α]
(φ ψ : power_series α) :
The order of the sum of two formal power series is the minimum of their orders if their orders differ.
The order of the product of two formal power series is at least the sum of their orders.
The order of the monomial a*X^n is infinite if a = 0 and n otherwise.
The order of the monomial a*X^n is n if a ≠ 0.
@[simp]
The order of the formal power series 1 is 0.
@[simp]
The order of the formal power series X is 1.
@[simp]
theorem
power_series.order_X_pow
{α : Type u_1}
[comm_semiring α]
[nontrivial α]
(n : ℕ) :
(power_series.X ^ n).order = ↑n
The order of the formal power series X^n is n.
The order of the product of two formal power series over an integral domain is the sum of their orders.
@[instance]
def
polynomial.coe_to_power_series
{α : Type u_2}
[comm_semiring α] :
has_coe (polynomial α) (power_series α)
The natural inclusion from polynomials into formal power series.
Equations
- polynomial.coe_to_power_series = {coe := λ (φ : polynomial α), power_series.mk (λ (n : ℕ), φ.coeff n)}
@[simp]
theorem
polynomial.coeff_coe
{α : Type u_2}
[comm_semiring α]
(φ : polynomial α)
(n : ℕ) :
⇑(power_series.coeff α n) ↑φ = φ.coeff n
@[simp]
theorem
polynomial.coe_monomial
{α : Type u_2}
[comm_semiring α]
(n : ℕ)
(a : α) :
↑(polynomial.monomial n a) = ⇑(power_series.monomial α n) a
@[simp]
@[simp]
@[simp]
theorem
polynomial.coe_C
{α : Type u_2}
[comm_semiring α]
(a : α) :
↑(⇑polynomial.C a) = ⇑(power_series.C α) a
@[simp]
The coercion from polynomials to power series as a ring homomorphism.
Equations
- polynomial.coe_to_power_series.ring_hom = {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}