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
@[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} :
p = q ↔ βˆ€ (n : β„•), p n = q n
@[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} :
p β‰  q ↔ βˆƒ (n : β„•), p n β‰  q n
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_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) :

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} [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
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) :

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) :
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
@[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] :
0.order = 0
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) :
p.order = 0 ↔ p 0 β‰  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} :
p.order = 0 ↔ p = 0 ∨ p 0 β‰  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 β‰  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.

Equations
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 : β„•) :
@[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 β†’ π•œ} :
⇑(p n) y = finset.univ.prod (Ξ» (i : fin n), y i) β€’ p.coeff 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 : β„•} :
p.coeff n = 0 ↔ p n = 0
@[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 : π•œ} :
⇑(p n) (Ξ» (_x : fin n), z) = z ^ n β€’ p.coeff n
@[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.

Equations
@[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 : β„•} :
p.fslope.coeff n = p.coeff (n + 1)
@[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 : β„•) :