Formal multilinear series

In this file we define FormalMultilinearSeries 𝕜 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 contDiff 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 FormalMultilinearSeries (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] : Type (max (max u_3 u_2) 0)

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.

instance instAddCommMonoidFormalMultilinearSeries {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] : AddCommMonoid (FormalMultilinearSeries 𝕜 E F)

instance instInhabitedFormalMultilinearSeries {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] : Inhabited (FormalMultilinearSeries 𝕜 E F)

instance instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (𝕜' : Type u_1) [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] : Module 𝕜' (FormalMultilinearSeries 𝕜 E F)

@[simp]

theorem FormalMultilinearSeries.zero_apply {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (n : ℕ) : 0 n = 0

@[simp]

theorem FormalMultilinearSeries.add_apply {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p q : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (p + q) n = p n + q n

@[simp]

theorem FormalMultilinearSeries.smul_apply {𝕜 : Type u} {𝕜' : Type u'} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (a : 𝕜') : (a • f) n = a • f n

theorem FormalMultilinearSeries.ext {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p q : FormalMultilinearSeries 𝕜 E F} (h : ∀ (n : ℕ), p n = q n) : p = q

theorem FormalMultilinearSeries.ext_iff {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p q : FormalMultilinearSeries 𝕜 E F} : p = q ↔ ∀ (n : ℕ), p n = q n

theorem FormalMultilinearSeries.ne_iff {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p q : FormalMultilinearSeries 𝕜 E F} : p ≠ q ↔ ∃ (n : ℕ), p n ≠ q n

def FormalMultilinearSeries.prod {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) : FormalMultilinearSeries 𝕜 E (F × G)

Cartesian product of two formal multilinear series (with the same field 𝕜 and the same source space, but possibly different target spaces).

def FormalMultilinearSeries.pi {𝕜 : Type u} {E : Type v} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] {ι : Type u_1} {F : ι → Type u_2} [(i : ι) → AddCommGroup (F i)] [(i : ι) → Module 𝕜 (F i)] [(i : ι) → TopologicalSpace (F i)] [∀ (i : ι), IsTopologicalAddGroup (F i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] (p : (i : ι) → FormalMultilinearSeries 𝕜 E (F i)) : FormalMultilinearSeries 𝕜 E ((i : ι) → F i)

Product of formal multilinear series (with the same field 𝕜 and the same source space, but possibly different target spaces).

def FormalMultilinearSeries.removeZero {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E F

Killing the zeroth coefficient in a formal multilinear series

@[simp]

theorem FormalMultilinearSeries.removeZero_coeff_zero {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : p.removeZero 0 = 0

@[simp]

theorem FormalMultilinearSeries.removeZero_coeff_succ {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : p.removeZero (n + 1) = p (n + 1)

theorem FormalMultilinearSeries.removeZero_of_pos {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (h : 0 < n) : p.removeZero n = p n

theorem FormalMultilinearSeries.congr {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 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.

theorem FormalMultilinearSeries.congr_zero {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) {k l : ℕ} (h : k = l) (h' : p k = 0) : p l = 0

def FormalMultilinearSeries.compContinuousLinearMap {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) : FormalMultilinearSeries 𝕜 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.compContinuousLinearMap u.

@[simp]

theorem FormalMultilinearSeries.compContinuousLinearMap_apply {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) (v : Fin n → E) : (p.compContinuousLinearMap u n) v = (p n) (⇑u ∘ v)

@[simp]

theorem FormalMultilinearSeries.compContinuousLinearMap_id {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : p.compContinuousLinearMap (ContinuousLinearMap.id 𝕜 E) = p

theorem FormalMultilinearSeries.compContinuousLinearMap_comp {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} {H : Type y} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] [AddCommMonoid H] [Module 𝕜 H] [TopologicalSpace H] [ContinuousAdd H] [ContinuousConstSMul 𝕜 H] (p : FormalMultilinearSeries 𝕜 G H) (u₁ : F →L[𝕜] G) (u₂ : E →L[𝕜] F) : (p.compContinuousLinearMap u₁).compContinuousLinearMap u₂ = p.compContinuousLinearMap (u₁.comp u₂)

def FormalMultilinearSeries.restrictScalars (𝕜 : Type u) {𝕜' : Type u'} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [Semiring 𝕜'] [SMul 𝕜 𝕜'] [Module 𝕜' E] [ContinuousConstSMul 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] (p : FormalMultilinearSeries 𝕜' E F) : FormalMultilinearSeries 𝕜 E F

Reinterpret a formal 𝕜'-multilinear series as a formal 𝕜-multilinear series.

instance FormalMultilinearSeries.instAddCommGroup {𝕜 : Type u} {E : Type v} {F : Type w} [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : AddCommGroup (FormalMultilinearSeries 𝕜 E F)

@[simp]

theorem FormalMultilinearSeries.neg_apply {𝕜 : Type u} {E : Type v} {F : Type w} [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (-f) n = -f n

@[simp]

theorem FormalMultilinearSeries.sub_apply {𝕜 : Type u} {E : Type v} {F : Type w} [Ring 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (f g : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (f - g) n = f n - g n

def FormalMultilinearSeries.shift {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 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 is the Taylor series (HasFTaylorSeriesUpTo) of a function, then p.shift is the Taylor series of the derivative of the function. Note that the p.sum of a Taylor series p does not give the original function; for a formal multilinear series that sums to the derivative of p.sum, see HasFPowerSeriesOnBall.fderiv.

def FormalMultilinearSeries.unshift {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : FormalMultilinearSeries 𝕜 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 (HasFTaylorSeriesUpTo) for the derivative of a function, and building a Taylor series for the function itself.

theorem FormalMultilinearSeries.unshift_shift {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {z : F} : (p.unshift z).shift = p

def ContinuousLinearMap.compFormalMultilinearSeries {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 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.compFormalMultilinearSeries p whose general term is f ∘ pₙ.

@[simp]

theorem ContinuousLinearMap.compFormalMultilinearSeries_apply {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : f.compFormalMultilinearSeries p n = f.compContinuousMultilinearMap (p n)

theorem ContinuousLinearMap.compFormalMultilinearSeries_apply' {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] [AddCommMonoid G] [Module 𝕜 G] [TopologicalSpace G] [ContinuousAdd G] [ContinuousConstSMul 𝕜 G] (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (v : Fin n → E) : (f.compFormalMultilinearSeries p n) v = f ((p n) v)

noncomputable def ContinuousMultilinearMap.toFormalMultilinearSeries {𝕜 : Type u} {F : Type w} [Semiring 𝕜] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {ι : Type u_1} {E : ι → Type u_2} [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] [∀ (i : ι), IsTopologicalAddGroup (E i)] [∀ (i : ι), ContinuousConstSMul 𝕜 (E i)] [Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) : FormalMultilinearSeries 𝕜 ((i : ι) → E i) F

Realize a ContinuousMultilinearMap on ∀ i : ι, E i as the evaluation of a FormalMultilinearSeries by choosing an arbitrary identification ι ≃ Fin (Fintype.card ι).

noncomputable def FormalMultilinearSeries.order {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 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.

@[simp]

theorem FormalMultilinearSeries.order_zero {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] : order 0 = 0

theorem FormalMultilinearSeries.ne_zero_of_order_ne_zero {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} (hp : p.order ≠ 0) : p ≠ 0

theorem FormalMultilinearSeries.order_eq_find {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} [DecidablePred fun (n : ℕ) => p n ≠ 0] (hp : ∃ (n : ℕ), p n ≠ 0) : p.order = Nat.find hp

theorem FormalMultilinearSeries.order_eq_find' {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} [DecidablePred fun (n : ℕ) => p n ≠ 0] (hp : p ≠ 0) : p.order = Nat.find ⋯

theorem FormalMultilinearSeries.order_eq_zero_iff' {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} : p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0

theorem FormalMultilinearSeries.order_eq_zero_iff {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} (hp : p ≠ 0) : p.order = 0 ↔ p 0 ≠ 0

theorem FormalMultilinearSeries.apply_order_ne_zero {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} (hp : p ≠ 0) : p p.order ≠ 0

theorem FormalMultilinearSeries.apply_order_ne_zero' {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} (hp : p.order ≠ 0) : p p.order ≠ 0

theorem FormalMultilinearSeries.apply_eq_zero_of_lt_order {𝕜 : Type u} {E : Type v} {F : Type w} [Semiring 𝕜] {n : ℕ} [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F] [ContinuousConstSMul 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} (hp : n < p.order) : p n = 0

def FormalMultilinearSeries.coeff {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : E

The nth coefficient of p when seen as a power series.

theorem FormalMultilinearSeries.mkPiRing_coeff_eq {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n

@[simp]

theorem FormalMultilinearSeries.apply_eq_prod_smul_coeff {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} {y : Fin n → 𝕜} : (p n) y = (∏ i : Fin n, y i) • p.coeff n

theorem FormalMultilinearSeries.coeff_eq_zero {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} : p.coeff n = 0 ↔ p n = 0

theorem FormalMultilinearSeries.apply_eq_pow_smul_coeff {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} {z : 𝕜} : ((p n) fun (x : Fin n) => z) = z ^ n • p.coeff n

@[simp]

theorem FormalMultilinearSeries.norm_apply_eq_norm_coef {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} : ‖p n‖ = ‖p.coeff n‖

noncomputable def FormalMultilinearSeries.fslope {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (p : FormalMultilinearSeries 𝕜 𝕜 E) : FormalMultilinearSeries 𝕜 𝕜 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 FormalMultilinearSeries.coeff_fslope {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ} : p.fslope.coeff n = p.coeff (n + 1)

@[simp]

theorem FormalMultilinearSeries.coeff_iterate_fslope {𝕜 : Type u} {E : Type v} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} (k n : ℕ) : (fslope^[k] p).coeff n = p.coeff (n + k)

def constFormalMultilinearSeries (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ContinuousConstSMul 𝕜 E] [IsTopologicalAddGroup E] {F : Type u_3} [NormedAddCommGroup F] [IsTopologicalAddGroup F] [NormedSpace 𝕜 F] [ContinuousConstSMul 𝕜 F] (c : F) : FormalMultilinearSeries 𝕜 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.

@[simp]

theorem constFormalMultilinearSeries_apply_zero {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} : constFormalMultilinearSeries 𝕜 E c 0 = ContinuousMultilinearMap.uncurry0 𝕜 E c

@[simp]

theorem constFormalMultilinearSeries_apply_succ {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} {n : ℕ} : constFormalMultilinearSeries 𝕜 E c (n + 1) = 0

theorem constFormalMultilinearSeries_apply_of_nonzero {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} {n : ℕ} (hn : n ≠ 0) : constFormalMultilinearSeries 𝕜 E c n = 0

@[deprecated constFormalMultilinearSeries_apply_of_nonzero (since := "2025-06-23")]

theorem constFormalMultilinearSeries_apply {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} {n : ℕ} (hn : n ≠ 0) : constFormalMultilinearSeries 𝕜 E c n = 0

Alias of constFormalMultilinearSeries_apply_of_nonzero.

@[simp]

theorem constFormalMultilinearSeries_zero {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] : constFormalMultilinearSeries 𝕜 E 0 = 0

@[simp]

theorem compContinuousLinearMap_zero {𝕜 : Type u} {E : Type v} {F : Type w} {G : Type x} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) : p.compContinuousLinearMap 0 = constFormalMultilinearSeries 𝕜 E ((p 0) 0)

def ContinuousLinearMap.fpowerSeries {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F

Formal power series of a continuous linear map f : E →L[𝕜] F at x : E: f y = f x + f (y - x).

@[simp]

theorem ContinuousLinearMap.fpowerSeries_apply_zero {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : f.fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 E (f x)

@[simp]

theorem ContinuousLinearMap.fpowerSeries_apply_one {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f

@[simp]

theorem ContinuousLinearMap.fpowerSeries_apply_add_two {𝕜 : Type u} {E : Type v} {F : Type w} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fpowerSeries x (n + 2) = 0