Laurent expansions of rational functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main declarations #

ratfunc.laurent: the Laurent expansion of the rational function f at r, as an alg_hom.
ratfunc.laurent_injective: the Laurent expansion at r is unique

Implementation details #

Implemented as the quotient of two Taylor expansions, over domains. An auxiliary definition is provided first to make the construction of the alg_hom easier, which works on comm_ring which are not necessarily domains.

source

theorem ratfunc.taylor_mem_non_zero_divisors {R : Type u} [comm_ring R] (r : R) (p : polynomial R) (hp : p ∈ non_zero_divisors (polynomial R)) :

⇑(polynomial.taylor r) p ∈ non_zero_divisors (polynomial R)

source

noncomputable def ratfunc.laurent_aux {R : Type u} [comm_ring R] (r : R) :

ratfunc R →+* ratfunc R

The Laurent expansion of rational functions about a value. Auxiliary definition, usage when over integral domains should prefer ratfunc.laurent.

Equations

ratfunc.laurent_aux r = ratfunc.map_ring_hom {to_fun := ⇑(polynomial.taylor r), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _} _

source

theorem ratfunc.laurent_aux_of_fraction_ring_mk {R : Type u} [comm_ring R] (r : R) (p : polynomial R) (q : ↥(non_zero_divisors (polynomial R))) :

⇑(ratfunc.laurent_aux r) {to_fraction_ring := localization.mk p q} = {to_fraction_ring := localization.mk (⇑(polynomial.taylor r) p) ⟨⇑(polynomial.taylor r) ↑q, _⟩}

source

theorem ratfunc.laurent_aux_div {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p q : polynomial R) :

⇑(ratfunc.laurent_aux r) (⇑(algebra_map (polynomial R) (ratfunc R)) p / ⇑(algebra_map (polynomial R) (ratfunc R)) q) = ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑(polynomial.taylor r) p) / ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑(polynomial.taylor r) q)

source

@[simp]

theorem ratfunc.laurent_aux_algebra_map {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p : polynomial R) :

⇑(ratfunc.laurent_aux r) (⇑(algebra_map (polynomial R) (ratfunc R)) p) = ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑(polynomial.taylor r) p)

source

noncomputable def ratfunc.laurent {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :

ratfunc R →ₐ[R] ratfunc R

The Laurent expansion of rational functions about a value.

Equations

ratfunc.laurent r = ratfunc.map_alg_hom {to_fun := ⇑(polynomial.taylor r), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _} _

source

theorem ratfunc.laurent_div {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p q : polynomial R) :

⇑(ratfunc.laurent r) (⇑(algebra_map (polynomial R) (ratfunc R)) p / ⇑(algebra_map (polynomial R) (ratfunc R)) q) = ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑(polynomial.taylor r) p) / ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑(polynomial.taylor r) q)

source

@[simp]

theorem ratfunc.laurent_algebra_map {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) (p : polynomial R) :

⇑(ratfunc.laurent r) (⇑(algebra_map (polynomial R) (ratfunc R)) p) = ⇑(algebra_map (polynomial R) (ratfunc R)) (⇑(polynomial.taylor r) p)

source

@[simp]

theorem ratfunc.laurent_X {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :

⇑(ratfunc.laurent r) ratfunc.X = ratfunc.X + ⇑ratfunc.C r

source

@[simp]

theorem ratfunc.laurent_C {R : Type u} [comm_ring R] [hdomain : is_domain R] (r x : R) :

⇑(ratfunc.laurent r) (⇑ratfunc.C x) = ⇑ratfunc.C x

source

@[simp]

theorem ratfunc.laurent_at_zero {R : Type u} [comm_ring R] [hdomain : is_domain R] (f : ratfunc R) :

⇑(ratfunc.laurent 0) f = f

source

theorem ratfunc.laurent_laurent {R : Type u} [comm_ring R] [hdomain : is_domain R] (r s : R) (f : ratfunc R) :

⇑(ratfunc.laurent r) (⇑(ratfunc.laurent s) f) = ⇑(ratfunc.laurent (r + s)) f

source

theorem ratfunc.laurent_injective {R : Type u} [comm_ring R] [hdomain : is_domain R] (r : R) :

function.injective ⇑(ratfunc.laurent r)