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 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 π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ 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 π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] :
@[protected, instance]
def formal_multilinear_series.inhabited {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] :
Equations
@[protected, instance]
def formal_multilinear_series.module {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] :
module π•œ (formal_multilinear_series π•œ E F)
Equations
def formal_multilinear_series.remove_zero {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ 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} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] (p : formal_multilinear_series π•œ E F) :
@[simp]
theorem formal_multilinear_series.remove_zero_coeff_succ {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ 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} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ 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} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ 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} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] [add_comm_group G] [module π•œ G] [topological_space G] [topological_add_group G] [has_continuous_const_smul π•œ 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} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] [add_comm_group G] [module π•œ G] [topological_space G] [topological_add_group G] [has_continuous_const_smul π•œ G] (p : formal_multilinear_series π•œ F G) (u : E β†’L[π•œ] F) (n : β„•) (v : fin n β†’ E) :
@[protected, simp]
def formal_multilinear_series.restrict_scalars (π•œ : Type u_1) {π•œ' : Type u_2} {E : Type u_3} {F : Type u_4} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] [comm_ring π•œ'] [has_scalar π•œ π•œ'] [module π•œ' E] [has_continuous_const_smul π•œ' E] [is_scalar_tower π•œ π•œ' E] [module π•œ' F] [has_continuous_const_smul π•œ' F] [is_scalar_tower π•œ π•œ' F] (p : formal_multilinear_series π•œ' E 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} [nondiscrete_normed_field π•œ] [normed_group E] [normed_space π•œ E] [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
noncomputable def formal_multilinear_series.unshift {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} [nondiscrete_normed_field π•œ] [normed_group E] [normed_space π•œ E] [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 continuous_linear_map.comp_formal_multilinear_series {π•œ : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [comm_ring π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] [add_comm_group G] [module π•œ G] [topological_space G] [topological_add_group G] [has_continuous_const_smul π•œ G] (f : F β†’L[π•œ] G) (p : formal_multilinear_series π•œ E 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 π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] [add_comm_group G] [module π•œ G] [topological_space G] [topological_add_group G] [has_continuous_const_smul π•œ G] (f : F β†’L[π•œ] G) (p : formal_multilinear_series π•œ E 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 π•œ] [add_comm_group E] [module π•œ E] [topological_space E] [topological_add_group E] [has_continuous_const_smul π•œ E] [add_comm_group F] [module π•œ F] [topological_space F] [topological_add_group F] [has_continuous_const_smul π•œ F] [add_comm_group G] [module π•œ G] [topological_space G] [topological_add_group G] [has_continuous_const_smul π•œ G] (f : F β†’L[π•œ] G) (p : formal_multilinear_series π•œ E F) (n : β„•) (v : fin n β†’ E) :