# mathlibdocumentation

analysis.calculus.formal_multilinear_series

# Formal multilinear series #

In this file we define formal_multilinear_series π E F to be a family of n-multilinear maps for all n, designed to model the sequence of derivatives of a function. In other files we use this notion to define C^n functions (called cont_diff in mathlib) and analytic functions.

## Notations #

We use the notation E [Γn]βL[π] F for the space of continuous multilinear maps on E^n with values in F. This is the space in which the n-th derivative of a function from E to F lives.

## Tags #

multilinear, formal series

@[nolint]
def formal_multilinear_series (π : Type u_1) (E : Type u_2) (F : Type u_3) [ring π] [module π E] [ E] [module π F] [ F] :
Type (max u_2 u_3)

A formal multilinear series over a field π, from E to F, is given by a family of multilinear maps from E^n to F for all n.

Equations
Instances for formal_multilinear_series
@[protected, instance]
def formal_multilinear_series.add_comm_group (π : Type u_1) (E : Type u_2) (F : Type u_3) [ring π] [module π E] [ E] [module π F] [ F] :
@[protected, instance]
def formal_multilinear_series.inhabited {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] :
Equations
@[protected, instance]
def formal_multilinear_series.module {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] :
module π E F)
Equations
def formal_multilinear_series.remove_zero {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] (p : F) :
F

Killing the zeroth coefficient in a formal multilinear series

Equations
@[simp]
theorem formal_multilinear_series.remove_zero_coeff_zero {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] (p : F) :
@[simp]
theorem formal_multilinear_series.remove_zero_coeff_succ {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] (p : F) (n : β) :
p.remove_zero (n + 1) = p (n + 1)
theorem formal_multilinear_series.remove_zero_of_pos {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] (p : F) {n : β} (h : 0 < n) :
p.remove_zero n = p n
theorem formal_multilinear_series.congr {π : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] (p : F) {m n : β} {v : fin m β E} {w : fin n β E} (h1 : m = n) (h2 : β (i : β) (him : i < m) (hin : i < n), v β¨i, himβ© = w β¨i, hinβ©) :
β(p m) v = β(p n) w

Convenience congruence lemma stating in a dependent setting that, if the arguments to a formal multilinear series are equal, then the values are also equal.

def formal_multilinear_series.comp_continuous_linear_map {π : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π] [module π E] [ E] [module π F] [ F] [module π G] [ G] (p : G) (u : E βL[π] F) :
G

Composing each term pβ in a formal multilinear series with (u, ..., u) where u is a fixed continuous linear map, gives a new formal multilinear series p.comp_continuous_linear_map u.

Equations
@[simp]
theorem formal_multilinear_series.comp_continuous_linear_map_apply {π : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π] [module π E] [ E] [module π F] [ F] [module π G] [ G] (p : G) (u : E βL[π] F) (n : β) (v : fin n β E) :
β n) v = β(p n) (βu β v)
@[protected, simp]
def formal_multilinear_series.restrict_scalars (π : Type u_1) {π' : Type u_2} {E : Type u_3} {F : Type u_4} [comm_ring π] [module π E] [ E] [module π F] [ F] [comm_ring π'] [has_smul π π'] [module π' E] [ E] [is_scalar_tower π π' E] [module π' F] [ F] [is_scalar_tower π π' F] (p : E F) :
F

Reinterpret a formal π'-multilinear series as a formal π-multilinear series.

Equations
noncomputable def formal_multilinear_series.shift {π : Type u_1} {E : Type u_3} {F : Type u_4} [normed_space π E] [normed_space π F] (p : F) :
(E βL[π] F)

Forgetting the zeroth term in a formal multilinear series, and interpreting the following terms as multilinear maps into E βL[π] F. If p corresponds to the Taylor series of a function, then p.shift is the Taylor series of the derivative of the function.

Equations
noncomputable def formal_multilinear_series.unshift {π : Type u_1} {E : Type u_3} {F : Type u_4} [normed_space π E] [normed_space π F] (q : (E βL[π] F)) (z : F) :
F

Adding a zeroth term to a formal multilinear series taking values in E βL[π] F. This corresponds to starting from a Taylor series for the derivative of a function, and building a Taylor series for the function itself.

Equations
def continuous_linear_map.comp_formal_multilinear_series {π : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π] [module π E] [ E] [module π F] [ F] [module π G] [ G] (f : F βL[π] G) (p : F) :
G

Composing each term pβ in a formal multilinear series with a continuous linear map f on the left gives a new formal multilinear series f.comp_formal_multilinear_series p whose general term is f β pβ.

Equations
@[simp]
theorem continuous_linear_map.comp_formal_multilinear_series_apply {π : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π] [module π E] [ E] [module π F] [ F] [module π G] [ G] (f : F βL[π] G) (p : F) (n : β) :
theorem continuous_linear_map.comp_formal_multilinear_series_apply' {π : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π] [module π E] [ E] [module π F] [ F] [module π G] [ G] (f : F βL[π] G) (p : F) (n : β) (v : fin n β E) :
v = βf (β(p n) v)