# 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 𝕜] [ E] [ 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
• = Π (n : ), (λ (i : fin n), E) F
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 𝕜] [ E] [ F]  :
@[protected, instance]
def formal_multilinear_series.inhabited {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring 𝕜] [ E] [ F]  :
Equations
@[protected, instance]
def formal_multilinear_series.module {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring 𝕜] [ E] [ F]  :
F)
Equations
def formal_multilinear_series.remove_zero {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring 𝕜] [ E] [ F] (p : 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 𝕜] [ E] [ 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 𝕜] [ E] [ 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 𝕜] [ E] [ 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 𝕜] [ E] [ 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 𝕜] [ E] [ F] [ G] (p : G) (u : E →L[𝕜] F) :

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
• = λ (n : ), (λ (i : fin n), u)
@[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 𝕜] [ E] [ F] [ 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 𝕜] [ E] [ F] [comm_ring 𝕜'] [ 𝕜'] [module 𝕜' E] [ 𝕜' E] [module 𝕜' F] [ 𝕜' F] (p : 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_group E] [ E] [normed_group F] [ 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_group E] [ E] [normed_group F] [ F] (q : (E →L[𝕜] F)) (z : 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 𝕜] [ E] [ F] [ G] (f : F →L[𝕜] G) (p : F) :

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 𝕜] [ E] [ F] [ 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 𝕜] [ E] [ F] [ G] (f : F →L[𝕜] G) (p : F) (n : ) (v : fin n → E) :
v = f ((p n) v)