Formal multilinear series #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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) π
@[protected]
theorem
formal_multilinear_series.ext_iff
{π : 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 q : formal_multilinear_series π E F} :
@[protected]
theorem
formal_multilinear_series.ne_iff
{π : 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 q : formal_multilinear_series π 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)
noncomputable
def
formal_multilinear_series.order
{π : 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) :
The index of the first non-zero coefficient in p (or 0 if all coefficients are zero). This
is the order of the isolated zero of an analytic function f at a point if p is the Taylor
series of f at that point.
Equations
- p.order = has_Inf.Inf {n : β | p n β 0}
@[simp]
theorem
formal_multilinear_series.order_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] :
theorem
formal_multilinear_series.ne_zero_of_order_ne_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}
(hp : p.order β 0) :
p β 0
theorem
formal_multilinear_series.order_eq_find
{π : 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}
[decidable_pred (Ξ» (n : β), p n β 0)]
(hp : β (n : β), p n β 0) :
theorem
formal_multilinear_series.order_eq_find'
{π : 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}
[decidable_pred (Ξ» (n : β), p n β 0)]
(hp : p β 0) :
theorem
formal_multilinear_series.order_eq_zero_iff
{π : 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}
(hp : p β 0) :
theorem
formal_multilinear_series.order_eq_zero_iff'
{π : 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} :
theorem
formal_multilinear_series.apply_order_ne_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}
(hp : p β 0) :
theorem
formal_multilinear_series.apply_order_ne_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}
(hp : p.order β 0) :
theorem
formal_multilinear_series.apply_eq_zero_of_lt_order
{π : Type u_1}
{E : Type u_3}
{F : Type u_4}
[comm_ring π]
{n : β}
[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}
(hp : n < p.order) :
p n = 0
def
formal_multilinear_series.coeff
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
(p : formal_multilinear_series π π E)
(n : β) :
E
The nth coefficient of p when seen as a power series.
theorem
formal_multilinear_series.mk_pi_field_coeff_eq
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
(p : formal_multilinear_series π π E)
(n : β) :
continuous_multilinear_map.mk_pi_field π (fin n) (p.coeff n) = p n
@[simp]
theorem
formal_multilinear_series.apply_eq_prod_smul_coeff
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{p : formal_multilinear_series π π E}
{n : β}
{y : fin n β π} :
theorem
formal_multilinear_series.coeff_eq_zero
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{p : formal_multilinear_series π π E}
{n : β} :
@[simp]
theorem
formal_multilinear_series.apply_eq_pow_smul_coeff
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{p : formal_multilinear_series π π E}
{n : β}
{z : π} :
@[simp]
theorem
formal_multilinear_series.norm_apply_eq_norm_coef
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{p : formal_multilinear_series π π E}
{n : β} :
noncomputable
def
formal_multilinear_series.fslope
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
(p : formal_multilinear_series π π E) :
formal_multilinear_series π π E
The formal counterpart of dslope, corresponding to the expansion of (f z - f 0) / z. If f
has p as a power series, then dslope f has fslope p as a power series.
@[simp]
theorem
formal_multilinear_series.coeff_fslope
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{p : formal_multilinear_series π π E}
{n : β} :
@[simp]
theorem
formal_multilinear_series.coeff_iterate_fslope
{π : Type u_1}
{E : Type u_3}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_space π E]
{p : formal_multilinear_series π π E}
(k n : β) :
def
const_formal_multilinear_series
(π : Type u_1)
[nontrivially_normed_field π]
(E : Type u_2)
[normed_add_comm_group E]
[normed_space π E]
[has_continuous_const_smul π E]
[topological_add_group E]
{F : Type u_3}
[normed_add_comm_group F]
[topological_add_group F]
[normed_space π F]
[has_continuous_const_smul π F]
(c : F) :
formal_multilinear_series π E F
The formal multilinear series where all terms of positive degree are equal to zero, and the term
of degree zero is c. It is the power series expansion of the constant function equal to c
everywhere.
Equations
- const_formal_multilinear_series π E c n.succ = 0
- const_formal_multilinear_series π E c 0 = continuous_multilinear_map.curry0 π E c
@[simp]
theorem
const_formal_multilinear_series_apply
{π : Type u_1}
{E : Type u_3}
{F : Type u_4}
[nontrivially_normed_field π]
[normed_add_comm_group E]
[normed_add_comm_group F]
[normed_space π E]
[normed_space π F]
{c : F}
{n : β}
(hn : n β 0) :
const_formal_multilinear_series π E c n = 0