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
- formal_multilinear_series π E F = Ξ (n : β), continuous_multilinear_map π (Ξ» (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 π]
[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 (formal_multilinear_series π E 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] :
inhabited (formal_multilinear_series π E 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
- formal_multilinear_series.module = let _inst : Ξ (n : β), module π (continuous_multilinear_map π (Ξ» (i : fin n), E) F) := Ξ» (n : β), continuous_multilinear_map.module in pi.module β (Ξ» (n : β), continuous_multilinear_map π (Ξ» (i : fin n), E) F) π
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) :
formal_multilinear_series π E F
Killing the zeroth coefficient in a formal multilinear series
Equations
- p.remove_zero (n + 1) = p (n + 1)
- p.remove_zero 0 = 0
@[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) :
p.remove_zero 0 = 0
@[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β©) :
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) :
formal_multilinear_series π E 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
- p.comp_continuous_linear_map u = Ξ» (n : β), (p n).comp_continuous_linear_map (Ξ» (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 π]
[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_smul π π']
[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) :
formal_multilinear_series π E F
Reinterpret a formal π'-multilinear series as a formal π-multilinear series.
Equations
- formal_multilinear_series.restrict_scalars π p = Ξ» (n : β), continuous_multilinear_map.restrict_scalars π (p n)
noncomputable
def
formal_multilinear_series.shift
{π : Type u_1}
{E : Type u_3}
{F : Type u_4}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
[normed_add_comm_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
- p.shift = Ξ» (n : β), (p n.succ).curry_right
noncomputable
def
formal_multilinear_series.unshift
{π : Type u_1}
{E : Type u_3}
{F : Type u_4}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
[normed_add_comm_group F]
[normed_space π F]
(q : formal_multilinear_series π E (E βL[π] F))
(z : F) :
formal_multilinear_series π E 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
- q.unshift z (n + 1) = β(continuous_multilinear_curry_right_equiv' π n E F) (q n)
- q.unshift z 0 = β((continuous_multilinear_curry_fin0 π E F).symm) z
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) :
formal_multilinear_series π E 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
- f.comp_formal_multilinear_series p = Ξ» (n : β), f.comp_continuous_multilinear_map (p n)
@[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 : β) :
f.comp_formal_multilinear_series p n = f.comp_continuous_multilinear_map (p 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) :
β(f.comp_formal_multilinear_series p n) v = βf (β(p n) v)