mathlib documentation

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 times_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

def formal_multilinear_series (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] (F : Type u_3) [normed_group F] [normed_space π•œ 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
@[instance]
def formal_multilinear_series.add_comm_group (π•œ : Type u_1) [nondiscrete_normed_field π•œ] (E : Type u_2) [normed_group E] [normed_space π•œ E] (F : Type u_3) [normed_group F] [normed_space π•œ F] :
@[instance]
def formal_multilinear_series.inhabited {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] :
Equations
@[instance]
def formal_multilinear_series.module {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] :
module π•œ (formal_multilinear_series π•œ E F)
Equations
def formal_multilinear_series.shift {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (p : formal_multilinear_series π•œ E F) :
formal_multilinear_series π•œ E (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
def formal_multilinear_series.unshift {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (q : formal_multilinear_series π•œ E (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 formal_multilinear_series.remove_zero {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (p : formal_multilinear_series π•œ E F) :

Killing the zeroth coefficient in a formal multilinear series

Equations
@[simp]
theorem formal_multilinear_series.remove_zero_coeff_zero {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (p : formal_multilinear_series π•œ E F) :
@[simp]
theorem formal_multilinear_series.remove_zero_coeff_succ {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (p : formal_multilinear_series π•œ E F) (n : β„•) :
p.remove_zero (n + 1) = p (n + 1)
theorem formal_multilinear_series.remove_zero_of_pos {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (p : formal_multilinear_series π•œ E F) {n : β„•} (h : 0 < n) :
p.remove_zero n = p n
theorem formal_multilinear_series.congr {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] (p : formal_multilinear_series π•œ E 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} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] {G : Type u_4} [normed_group G] [normed_space π•œ G] (p : formal_multilinear_series π•œ F 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
@[simp]
theorem formal_multilinear_series.comp_continuous_linear_map_apply {π•œ : Type u_1} [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] {G : Type u_4} [normed_group G] [normed_space π•œ G] (p : formal_multilinear_series π•œ F G) (u : E β†’L[π•œ] F) (n : β„•) (v : fin n β†’ E) :
@[simp]
def formal_multilinear_series.restrict_scalars (π•œ : Type u_1) [nondiscrete_normed_field π•œ] {E : Type u_2} [normed_group E] [normed_space π•œ E] {F : Type u_3} [normed_group F] [normed_space π•œ F] {π•œ' : Type u_5} [nondiscrete_normed_field π•œ'] [normed_algebra π•œ π•œ'] [normed_space π•œ' E] [is_scalar_tower π•œ π•œ' E] [normed_space π•œ' F] [is_scalar_tower π•œ π•œ' F] (p : formal_multilinear_series π•œ' E F) :

Reinterpret a formal π•œ'-multilinear series as a formal π•œ-multilinear series, where π•œ' is a normed algebra over π•œ.

Equations