Mathlib.Analysis.Calculus.FormalMultilinearSeries

FormalMultilinearSeries definition

 (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E]
  [ContinuousConstSMul 𝕜 E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F]
  [ContinuousConstSMul 𝕜 F]

Full source

/-- 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`. -/
@[nolint unusedArguments]
def FormalMultilinearSeries (𝕜 : Type*) (E : Type*) (F : Type*) [Semiring 𝕜] [AddCommMonoid E]
    [Module 𝕜 E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousConstSMul 𝕜 E]
    [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] [ContinuousAdd F]
    [ContinuousConstSMul 𝕜 F] :=
  ∀ n : ℕ, E[×n]→L[𝕜] F

Formal multilinear series

Informal description

A formal multilinear series over a field $\mathbb{K}$, from a topological module $E$ to another topological module $F$, is a sequence of continuous $n$-multilinear maps from $E^n$ to $F$ for each natural number $n$. Here, $E$ and $F$ are required to be additive commutative monoids with a $\mathbb{K}$-module structure, equipped with a topology where addition and scalar multiplication are continuous operations.

instAddCommMonoidFormalMultilinearSeries instance

: AddCommMonoid (FormalMultilinearSeries 𝕜 E F)

Full source

instance : AddCommMonoid (FormalMultilinearSeries 𝕜 E F) :=
  inferInstanceAs <| AddCommMonoid <| ∀ n : ℕ, E[×n]→L[𝕜] F

Additive Commutative Monoid Structure on Formal Multilinear Series

Informal description

The space of formal multilinear series from $E$ to $F$ over the field $\mathbb{K}$ forms an additive commutative monoid, where addition is defined pointwise and the zero element is the constant zero series.

instInhabitedFormalMultilinearSeries instance

: Inhabited (FormalMultilinearSeries 𝕜 E F)

Full source

instance : Inhabited (FormalMultilinearSeries 𝕜 E F) :=
  ⟨0⟩

Nonemptiness of Formal Multilinear Series Space

Informal description

The space of formal multilinear series from $E$ to $F$ over the field $\mathbb{K}$ is nonempty, with the zero series as a canonical element.

instModuleFormalMultilinearSeriesOfContinuousConstSMulOfSMulCommClass instance

 (𝕜') [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] :
  Module 𝕜' (FormalMultilinearSeries 𝕜 E F)

Full source

instance (𝕜') [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] :
    Module 𝕜' (FormalMultilinearSeries 𝕜 E F) :=
  inferInstanceAs <| Module 𝕜' <| ∀ n : ℕ, E[×n]→L[𝕜] F

Module Structure on Formal Multilinear Series with Commuting Scalars

Informal description

For any semiring $\mathbb{K}'$ and topological $\mathbb{K}'$-module $F$ with continuous scalar multiplication, where $\mathbb{K}$ and $\mathbb{K}'$ commute in their action on $F$, the space of formal multilinear series from $E$ to $F$ over $\mathbb{K}$ forms a $\mathbb{K}'$-module. The module operations are defined pointwise.

FormalMultilinearSeries.zero_apply theorem

(n : ℕ) : (0 : FormalMultilinearSeries 𝕜 E F) n = 0

Full source

@[simp]
theorem zero_apply (n : ℕ) : (0 : FormalMultilinearSeries 𝕜 E F) n = 0 := rfl

Zero Formal Multilinear Series Evaluates to Zero Map

Informal description

For any natural number $n$, the $n$-th term of the zero formal multilinear series from $E$ to $F$ over the field $\mathbb{K}$ is the zero continuous multilinear map.

FormalMultilinearSeries.add_apply theorem

(p q : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (p + q) n = p n + q n

Full source

@[simp]
theorem add_apply (p q : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (p + q) n = p n + q n := rfl

Pointwise Addition of Formal Multilinear Series

Informal description

For any two formal multilinear series $p$ and $q$ from $E$ to $F$ over a field $\mathbb{K}$, and for any natural number $n$, the $n$-th term of the sum $p + q$ is equal to the sum of the $n$-th terms of $p$ and $q$, i.e., $(p + q)_n = p_n + q_n$.

FormalMultilinearSeries.smul_apply theorem

 [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F] (f : FormalMultilinearSeries 𝕜 E F)
  (n : ℕ) (a : 𝕜') : (a • f) n = a • f n

Full source

@[simp]
theorem smul_apply [Semiring 𝕜'] [Module 𝕜' F] [ContinuousConstSMul 𝕜' F] [SMulCommClass 𝕜 𝕜' F]
    (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (a : 𝕜') : (a • f) n = a • f n := rfl

Pointwise Scalar Multiplication of Formal Multilinear Series: $(a \cdot f)_n = a \cdot f_n$

Informal description

Let $\mathbb{K}$ and $\mathbb{K}'$ be semirings, and let $E$ and $F$ be topological modules over $\mathbb{K}$ with continuous addition and scalar multiplication. Suppose $F$ is also a module over $\mathbb{K}'$ with continuous scalar multiplication, and the actions of $\mathbb{K}$ and $\mathbb{K}'$ on $F$ commute. For any formal multilinear series $f$ from $E$ to $F$ over $\mathbb{K}$, any scalar $a \in \mathbb{K}'$, and any natural number $n$, the $n$-th term of the scaled series $a \cdot f$ is equal to the scalar multiple of the $n$-th term of $f$ by $a$, i.e., $$(a \cdot f)_n = a \cdot f_n.$$

FormalMultilinearSeries.ext theorem

{p q : FormalMultilinearSeries 𝕜 E F} (h : ∀ n, p n = q n) : p = q

Full source

@[ext]
protected theorem ext {p q : FormalMultilinearSeries 𝕜 E F} (h : ∀ n, p n = q n) : p = q :=
  funext h

Extensionality of Formal Multilinear Series

Informal description

Let $p$ and $q$ be two formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$. If for every natural number $n$, the $n$-th term of $p$ equals the $n$-th term of $q$ (i.e., $p_n = q_n$), then the two series are equal: $p = q$.

FormalMultilinearSeries.ne_iff theorem

{p q : FormalMultilinearSeries 𝕜 E F} : p ≠ q ↔ ∃ n, p n ≠ q n

Full source

protected theorem ne_iff {p q : FormalMultilinearSeries 𝕜 E F} : p ≠ qp ≠ q ↔ ∃ n, p n ≠ q n :=
  Function.ne_iff

Inequality of Formal Multilinear Series via Pointwise Inequality

Informal description

Two formal multilinear series $p$ and $q$ from $E$ to $F$ over the field $\mathbb{K}$ are not equal if and only if there exists a natural number $n$ such that their $n$-th multilinear maps differ, i.e., $p_n \neq q_n$.

FormalMultilinearSeries.prod definition

(p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) : FormalMultilinearSeries 𝕜 E (F × G)

Full source

/-- Cartesian product of two formal multilinear series (with the same field `𝕜` and the same source
space, but possibly different target spaces). -/
def prod (p : FormalMultilinearSeries 𝕜 E F) (q : FormalMultilinearSeries 𝕜 E G) :
    FormalMultilinearSeries 𝕜 E (F × G)
  | n => (p n).prod (q n)

Product of formal multilinear series

Informal description

Given two formal multilinear series $ p $ from $ E $ to $ F $ and $ q $ from $ E $ to $ G $ over a field $ \mathbb{K} $, their product $ p \times q $ is the formal multilinear series from $ E $ to $ F \times G $ defined by $(p \times q)_n = p_n \times q_n$ for each $ n $, where $ p_n \times q_n $ denotes the product of the $ n $-th multilinear maps of $ p $ and $ q $.

FormalMultilinearSeries.pi definition

 {ι : Type*} {F : ι → Type*} [∀ 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)

Full source

/-- Product of formal multilinear series (with the same field `𝕜` and the same source
space, but possibly different target spaces). -/
@[simp] def pi {ι : Type*} {F : ι → Type*}
    [∀ 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)
  | n => ContinuousMultilinearMap.pi (fun i ↦ p i n)

Product of formal multilinear series

Informal description

Given an index set $\iota$ and a family of topological modules $\{F_i\}_{i \in \iota}$ over a field $\mathbb{K}$, each equipped with an additive group structure and continuous scalar multiplication, and given a family of formal multilinear series $p_i : \text{FormalMultilinearSeries}\, \mathbb{K}\, E\, F_i$ for each $i \in \iota$, the function constructs a new formal multilinear series from $E$ to the product space $\prod_{i \in \iota} F_i$. For each natural number $n$, the $n$-th term of the resulting series is the continuous multilinear map formed by taking the product of the $n$-th terms of each $p_i$ series, i.e., $\lambda n, \text{ContinuousMultilinearMap.pi}\, (\lambda i, p_i\, n)$.

FormalMultilinearSeries.removeZero definition

(p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E F

Full source

/-- Killing the zeroth coefficient in a formal multilinear series -/
def removeZero (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E F
  | 0 => 0
  | n + 1 => p (n + 1)

Formal multilinear series with zeroth coefficient killed

Informal description

Given a formal multilinear series $ p $ from $ E $ to $ F $, the operation `removeZero` constructs a new formal multilinear series where the zeroth coefficient is set to zero and all other coefficients remain unchanged. Specifically, for $ n = 0 $, the coefficient is $ 0 $, and for $ n \geq 1 $, the coefficient is $ p(n) $.

FormalMultilinearSeries.removeZero_coeff_zero theorem

(p : FormalMultilinearSeries 𝕜 E F) : p.removeZero 0 = 0

Full source

@[simp]
theorem removeZero_coeff_zero (p : FormalMultilinearSeries 𝕜 E F) : p.removeZero 0 = 0 :=
  rfl

Zeroth Coefficient of `removeZero` is Zero

Informal description

For any formal multilinear series $p$ from $E$ to $F$, the zeroth coefficient of the series $p.\text{removeZero}$ is equal to the zero map, i.e., $p.\text{removeZero}(0) = 0$.

FormalMultilinearSeries.removeZero_coeff_succ theorem

(p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : p.removeZero (n + 1) = p (n + 1)

Full source

@[simp]
theorem removeZero_coeff_succ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) :
    p.removeZero (n + 1) = p (n + 1) :=
  rfl

Preservation of Higher Coefficients in `removeZero` Operation

Informal description

For any formal multilinear series $p$ from $E$ to $F$ and any natural number $n$, the $(n+1)$-th coefficient of the series $p.\text{removeZero}$ is equal to the $(n+1)$-th coefficient of $p$, i.e., $p.\text{removeZero}(n+1) = p(n+1)$.

FormalMultilinearSeries.removeZero_of_pos theorem

(p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (h : 0 < n) : p.removeZero n = p n

Full source

theorem removeZero_of_pos (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (h : 0 < n) :
    p.removeZero n = p n := by
  rw [← Nat.succ_pred_eq_of_pos h]
  rfl

Preservation of Non-Zero Coefficients in `removeZero` Operation

Informal description

For any formal multilinear series $p$ from $E$ to $F$ and any natural number $n > 0$, the $n$-th coefficient of the series $p.\text{removeZero}$ is equal to the $n$-th coefficient of $p$, i.e., $p.\text{removeZero}(n) = p(n)$.

FormalMultilinearSeries.congr theorem

 (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

Full source

/-- 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 congr (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 := by
  subst n
  congr with ⟨i, hi⟩
  exact h2 i hi hi

Congruence of Formal Multilinear Series Evaluations under Index and Component Equality

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$. For any natural numbers $m$ and $n$ with $m = n$, and any vectors $v \in E^m$ and $w \in E^n$ such that for all indices $i < m = n$ the components satisfy $v_i = w_i$, then the evaluation of the series satisfies $p(m)(v) = p(n)(w)$.

FormalMultilinearSeries.congr_zero theorem

(p : FormalMultilinearSeries 𝕜 E F) {k l : ℕ} (h : k = l) (h' : p k = 0) : p l = 0

Full source

lemma congr_zero (p : FormalMultilinearSeries 𝕜 E F) {k l : ℕ} (h : k = l) (h' : p k = 0) :
    p l = 0 := by
  subst h; exact h'

Zero Term Preservation in Formal Multilinear Series under Index Equality

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$. For any natural numbers $k$ and $l$ such that $k = l$, if the $k$-th term $p(k)$ is the zero map, then the $l$-th term $p(l)$ is also the zero map.

FormalMultilinearSeries.compContinuousLinearMap definition

(p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) : FormalMultilinearSeries 𝕜 E G

Full source

/-- 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`. -/
def compContinuousLinearMap (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) :
    FormalMultilinearSeries 𝕜 E G := fun n => (p n).compContinuousLinearMap fun _ : Fin n => u

Composition of a formal multilinear series with a continuous linear map

Informal description

Given a formal multilinear series $ p $ from $ F $ to $ G $ over a field $ \mathbb{K} $ and a continuous linear map $ u : E \to F $, the composition $ p \circ u $ is a formal multilinear series from $ E $ to $ G $. Specifically, for each $ n $, the $ n $-th term of the composed series is obtained by composing the $ n $-th term of $ p $ with $ u $ applied to each component of the input tuple.

FormalMultilinearSeries.compContinuousLinearMap_apply theorem

 (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) (v : Fin n → E) :
  (p.compContinuousLinearMap u) n v = p n (u ∘ v)

Full source

@[simp]
theorem compContinuousLinearMap_apply (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ)
    (v : Fin n → E) : (p.compContinuousLinearMap u) n v = p n (u ∘ v) :=
  rfl

Evaluation of the Composition of a Formal Multilinear Series with a Continuous Linear Map

Informal description

Let $p$ be a formal multilinear series from $F$ to $G$ over a field $\mathbb{K}$, and let $u : E \to F$ be a continuous linear map. For any natural number $n$ and any tuple $v = (v_1, \ldots, v_n) \in E^n$, the $n$-th term of the composed series $p \circ u$ evaluated at $v$ equals the $n$-th term of $p$ evaluated at $(u(v_1), \ldots, u(v_n))$. In other words, $$(p \circ u)_n(v) = p_n(u \circ v).$$

FormalMultilinearSeries.restrictScalars definition

(p : FormalMultilinearSeries 𝕜' E F) : FormalMultilinearSeries 𝕜 E F

Full source

/-- Reinterpret a formal `𝕜'`-multilinear series as a formal `𝕜`-multilinear series. -/
@[simp]
protected def restrictScalars (p : FormalMultilinearSeries 𝕜' E F) :
    FormalMultilinearSeries 𝕜 E F := fun n => (p n).restrictScalars 𝕜

Restriction of scalars for formal multilinear series

Informal description

Given a formal $\mathbb{K}'$-multilinear series $p$ from $E$ to $F$, the function `restrictScalars` reinterprets $p$ as a formal $\mathbb{K}$-multilinear series, where $\mathbb{K}$ is a subring of $\mathbb{K}'$. For each natural number $n$, the $n$-th term of the resulting series is obtained by restricting the scalars of the $n$-th term of $p$ from $\mathbb{K}'$ to $\mathbb{K}$.

FormalMultilinearSeries.instAddCommGroup instance

: AddCommGroup (FormalMultilinearSeries 𝕜 E F)

Full source

instance : AddCommGroup (FormalMultilinearSeries 𝕜 E F) :=
  inferInstanceAs <| AddCommGroup <| ∀ n : ℕ, E[×n]→L[𝕜] F

Additive Commutative Group Structure on Formal Multilinear Series

Informal description

The space of formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$ forms an additive commutative group, where addition and negation are defined pointwise for each term in the series.

FormalMultilinearSeries.neg_apply theorem

(f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (-f) n = -f n

Full source

@[simp]
theorem neg_apply (f : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (-f) n = - f n := rfl

Pointwise Negation of Formal Multilinear Series

Informal description

For any formal multilinear series $f$ from $E$ to $F$ over a field $\mathbb{K}$ and any natural number $n$, the $n$-th term of the negation of $f$ is equal to the negation of the $n$-th term of $f$, i.e., $(-f)_n = -f_n$.

FormalMultilinearSeries.sub_apply theorem

(f g : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (f - g) n = f n - g n

Full source

@[simp]
theorem sub_apply (f g : FormalMultilinearSeries 𝕜 E F) (n : ℕ) : (f - g) n = f n - g n := rfl

Pointwise Subtraction of Formal Multilinear Series

Informal description

For any two formal multilinear series $f$ and $g$ from $E$ to $F$ over a field $\mathbb{K}$, and for any natural number $n$, the $n$-th term of the series $f - g$ is equal to the difference of the $n$-th terms of $f$ and $g$, i.e., $(f - g)_n = f_n - g_n$.

FormalMultilinearSeries.shift definition

: FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)

Full source

/-- 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 shift : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) := fun n => (p n.succ).curryRight

Shifted formal multilinear series

Informal description

Given a formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, the shifted series $p.\text{shift}$ is obtained by removing the zeroth term and interpreting each subsequent term $p_{n+1}$ as a continuous multilinear map from $E^n$ to the space of continuous linear maps from $E$ to $F$ (denoted $E \toL[\mathbb{K}] F$). More precisely, for each $n \in \mathbb{N}$, the $n$-th term of $p.\text{shift}$ is the right-curried version of $p_{n+1}$, which takes $n$ arguments in $E$ and returns a continuous linear map from $E$ to $F$.

FormalMultilinearSeries.unshift definition

(q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : FormalMultilinearSeries 𝕜 E F

Full source

/-- 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. -/
def unshift (q : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)) (z : F) : FormalMultilinearSeries 𝕜 E F
  | 0 => (continuousMultilinearCurryFin0 𝕜 E F).symm z
  | n + 1 => (continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm (q n)

Unshifting a formal multilinear series with a base element

Informal description

Given a formal multilinear series $ q $ from $ E $ to $ E \toL[\mathbb{K}] F $ and an element $ z \in F $, the operation `unshift` constructs a new formal multilinear series from $ E $ to $ F $. The zeroth term of this new series is $ z $ (interpreted as a constant multilinear map), and the $(n+1)$-th term is obtained by uncurrying the $n$-th term of $ q $ (which is a continuous multilinear map from $ E^{n+1} $ to $ F $ via $ E \toL[\mathbb{K}] F $).

FormalMultilinearSeries.unshift_shift theorem

{p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {z : F} : (p.unshift z).shift = p

Full source

theorem unshift_shift {p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {z : F} :
    (p.unshift z).shift = p := by
  ext1 n
  simp [shift, unshift]
  exact LinearIsometryEquiv.apply_symm_apply (continuousMultilinearCurryRightEquiv' 𝕜 n E F) (p n)

Shift-Unshift Identity for Formal Multilinear Series: $(p.\text{unshift}~z).\text{shift} = p$

Informal description

Let $p$ be a formal multilinear series from $E$ to $E \toL[\mathbb{K}] F$ over a field $\mathbb{K}$, and let $z \in F$. Then the shift of the unshifted series $(p.\text{unshift}~z).\text{shift}$ equals the original series $p$.

ContinuousLinearMap.compFormalMultilinearSeries definition

(f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) : FormalMultilinearSeries 𝕜 E G

Full source

/-- 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ₙ`. -/
def compFormalMultilinearSeries (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) :
    FormalMultilinearSeries 𝕜 E G := fun n => f.compContinuousMultilinearMap (p n)

Composition of a continuous linear map with a formal multilinear series

Informal description

Given a continuous linear map $ f : F \to G $ and a formal multilinear series $ p $ from $ E $ to $ F $, the composition $ f \circ p $ is a formal multilinear series from $ E $ to $ G $ whose $ n $-th term is the composition of $ f $ with the $ n $-th term of $ p $.

ContinuousLinearMap.compFormalMultilinearSeries_apply theorem

 (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) :
  (f.compFormalMultilinearSeries p) n = f.compContinuousMultilinearMap (p n)

Full source

@[simp]
theorem compFormalMultilinearSeries_apply (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F)
    (n : ℕ) : (f.compFormalMultilinearSeries p) n = f.compContinuousMultilinearMap (p n) :=
  rfl

Composition of Continuous Linear Map with Formal Multilinear Series Termwise

Informal description

Given a continuous linear map $f : F \to G$ and a formal multilinear series $p$ from $E$ to $F$, the $n$-th term of the composed formal multilinear series $f \circ p$ is equal to the composition of $f$ with the $n$-th term of $p$, i.e., $$(f \circ p)_n = f \circ p_n.$$

ContinuousLinearMap.compFormalMultilinearSeries_apply' theorem

 (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (v : Fin n → E) :
  (f.compFormalMultilinearSeries p) n v = f (p n v)

Full source

theorem compFormalMultilinearSeries_apply' (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F)
    (n : ℕ) (v : Fin n → E) : (f.compFormalMultilinearSeries p) n v = f (p n v) :=
  rfl

Evaluation of Composed Formal Multilinear Series: $(f \circ p)_n(v) = f(p_n(v))$

Informal description

Let $f : F \to G$ be a continuous linear map between topological modules over a field $\mathbb{K}$, and let $p$ be a formal multilinear series from $E$ to $F$. For any natural number $n$ and any vector $v \in E^n$, the $n$-th term of the composed formal multilinear series $f \circ p$ evaluated at $v$ satisfies $(f \circ p)_n(v) = f(p_n(v))$.

ContinuousMultilinearMap.toFormalMultilinearSeries definition

: FormalMultilinearSeries 𝕜 (∀ i, E i) F

Full source

/-- Realize a ContinuousMultilinearMap on `∀ i : ι, E i` as the evaluation of a
FormalMultilinearSeries by choosing an arbitrary identification `ι ≃ Fin (Fintype.card ι)`. -/
noncomputable def toFormalMultilinearSeries : FormalMultilinearSeries 𝕜 (∀ i, E i) F :=
  fun n ↦ if h : Fintype.card ι = n then
    (f.compContinuousLinearMap .proj).domDomCongr (Fintype.equivFinOfCardEq h)
  else 0

Formal multilinear series induced by a continuous multilinear map

Informal description

Given a continuous multilinear map $f$ from $\prod_{i \in \iota} E_i$ to $F$, the function constructs a formal multilinear series where the $n$-th term is obtained by reindexing the domain of $f$ to match the cardinality $n$ of the index set $\iota$ (if such a cardinality exists), and is zero otherwise. Specifically, for each natural number $n$, if the cardinality of $\iota$ equals $n$, then the $n$-th term of the series is the composition of $f$ with the projection maps, reindexed via the equivalence between $\iota$ and $\mathrm{Fin}(n)$. If the cardinality does not match, the term is zero.

FormalMultilinearSeries.order definition

(p : FormalMultilinearSeries 𝕜 E F) : ℕ

Full source

/-- 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. -/
noncomputable def order (p : FormalMultilinearSeries 𝕜 E F) : ℕ :=
  sInf { n | p n ≠ 0 }

Order of a formal multilinear series

Informal description

Given a formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, the order of $p$ is defined as the smallest natural number $n$ for which the $n$-th coefficient $p_n$ is nonzero. If all coefficients are zero, the order is defined to be zero. This corresponds to the order of an isolated zero in the context of analytic functions when $p$ represents the Taylor series of such a function.

FormalMultilinearSeries.order_zero theorem

: (0 : FormalMultilinearSeries 𝕜 E F).order = 0

Full source

@[simp]
theorem order_zero : (0 : FormalMultilinearSeries 𝕜 E F).order = 0 := by simp [order]

Order of the Zero Formal Multilinear Series is Zero

Informal description

The order of the zero formal multilinear series is zero, i.e., $\text{order}(0) = 0$.

FormalMultilinearSeries.ne_zero_of_order_ne_zero theorem

(hp : p.order ≠ 0) : p ≠ 0

Full source

theorem ne_zero_of_order_ne_zero (hp : p.order ≠ 0) : p ≠ 0 := fun h => by simp [h] at hp

Nonzero Order Implies Nonzero Series

Informal description

If the order of a formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$ is nonzero, then $p$ is not the zero series.

FormalMultilinearSeries.order_eq_find theorem

[DecidablePred fun n => p n ≠ 0] (hp : ∃ n, p n ≠ 0) : p.order = Nat.find hp

Full source

theorem order_eq_find [DecidablePred fun n => p n ≠ 0] (hp : ∃ n, p n ≠ 0) :
    p.order = Nat.find hp := by convert Nat.sInf_def hp

Order of Formal Multilinear Series as Minimal Nonzero Index

Informal description

Let $p$ be a formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$, and assume there exists some $n$ for which the $n$-th coefficient $p_n$ is nonzero. Then the order of $p$ is equal to the smallest natural number $n$ such that $p_n \neq 0$.

FormalMultilinearSeries.order_eq_find' theorem

[DecidablePred fun n => p n ≠ 0] (hp : p ≠ 0) : p.order = Nat.find (FormalMultilinearSeries.ne_iff.mp hp)

Full source

theorem order_eq_find' [DecidablePred fun n => p n ≠ 0] (hp : p ≠ 0) :
    p.order = Nat.find (FormalMultilinearSeries.ne_iff.mp hp) :=
  order_eq_find _

Order of Nonzero Formal Multilinear Series as Minimal Nonzero Index

Informal description

Let $p$ be a nonzero formal multilinear series from $E$ to $F$ over a field $\mathbb{K}$. Then the order of $p$ is equal to the smallest natural number $n$ such that the $n$-th coefficient $p_n$ is nonzero.

FormalMultilinearSeries.order_eq_zero_iff' theorem

: p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0

Full source

theorem order_eq_zero_iff' : p.order = 0 ↔ p = 0 ∨ p 0 ≠ 0 := by
  simpa [order, Nat.sInf_eq_zero, FormalMultilinearSeries.ext_iff, eq_empty_iff_forall_not_mem]
    using or_comm

Characterization of Zero Order in Formal Multilinear Series: $p.\text{order} = 0 \leftrightarrow p = 0 \lor p_0 \neq 0$

Informal description

For a formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, the order of $p$ is zero if and only if either $p$ is identically zero or its zeroth coefficient $p_0$ is nonzero.

FormalMultilinearSeries.order_eq_zero_iff theorem

(hp : p ≠ 0) : p.order = 0 ↔ p 0 ≠ 0

Full source

theorem order_eq_zero_iff (hp : p ≠ 0) : p.order = 0 ↔ p 0 ≠ 0 := by
  simp [order_eq_zero_iff', hp]

Order Zero Criterion for Formal Multilinear Series: $p.\text{order} = 0 \leftrightarrow p_0 \neq 0$

Informal description

For a nonzero formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, the order of $p$ is zero if and only if the zeroth coefficient $p_0$ is nonzero.

FormalMultilinearSeries.apply_order_ne_zero theorem

(hp : p ≠ 0) : p p.order ≠ 0

Full source

theorem apply_order_ne_zero (hp : p ≠ 0) : p p.order ≠ 0 :=
  Nat.sInf_mem (FormalMultilinearSeries.ne_iff.1 hp)

Nonvanishing of Leading Coefficient in Formal Multilinear Series

Informal description

For any nonzero formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, the coefficient $p_n$ at the order $n = \text{order}(p)$ is nonzero.

FormalMultilinearSeries.apply_order_ne_zero' theorem

(hp : p.order ≠ 0) : p p.order ≠ 0

Full source

theorem apply_order_ne_zero' (hp : p.order ≠ 0) : p p.order ≠ 0 :=
  apply_order_ne_zero (ne_zero_of_order_ne_zero hp)

Nonvanishing of Leading Coefficient for Nonzero Order in Formal Multilinear Series

Informal description

For a formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, if the order of $p$ is nonzero, then the coefficient $p_n$ at $n = \text{order}(p)$ is nonzero.

FormalMultilinearSeries.apply_eq_zero_of_lt_order theorem

(hp : n < p.order) : p n = 0

Full source

theorem apply_eq_zero_of_lt_order (hp : n < p.order) : p n = 0 :=
  by_contra <| Nat.not_mem_of_lt_sInf hp

Vanishing of Coefficients Below Order in Formal Multilinear Series

Informal description

For a formal multilinear series $p$ from $E$ to $F$ over a field $\mathbb{K}$, if a natural number $n$ is less than the order of $p$, then the $n$-th coefficient $p_n$ is zero.

FormalMultilinearSeries.coeff definition

(p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : E

Full source

/-- The `n`th coefficient of `p` when seen as a power series. -/
def coeff (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : E :=
  p n 1

Coefficient of formal multilinear series as power series

Informal description

For a formal multilinear series $p$ from $\mathbb{K}$ to $E$ over a field $\mathbb{K}$, the coefficient $p_n$ evaluated at the constant tuple $1 \in \mathbb{K}^n$ gives the $n$-th coefficient of $p$ when viewed as a power series.

FormalMultilinearSeries.mkPiRing_coeff_eq theorem

(p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) : ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n

Full source

theorem mkPiRing_coeff_eq (p : FormalMultilinearSeries 𝕜 𝕜 E) (n : ℕ) :
    ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (p.coeff n) = p n :=
  (p n).mkPiRing_apply_one_eq_self

Reconstruction of Formal Multilinear Series via $\text{mkPiRing}$ and Coefficients

Informal description

For any formal multilinear series $p$ from $\mathbb{K}$ to $E$ over a field $\mathbb{K}$ and any natural number $n$, the continuous multilinear map constructed by $\text{mkPiRing}_{\mathbb{K}}^{\text{Fin}(n)}$ applied to the $n$-th coefficient of $p$ is equal to the $n$-th term of $p$. That is, \[ \text{mkPiRing}_{\mathbb{K}}^{\text{Fin}(n)}(p_n) = p_n. \]

FormalMultilinearSeries.apply_eq_prod_smul_coeff theorem

: p n y = (∏ i, y i) • p.coeff n

Full source

@[simp]
theorem apply_eq_prod_smul_coeff : p n y = (∏ i, y i) • p.coeff n := by
  convert (p n).toMultilinearMap.map_smul_univ y 1
  simp only [Pi.one_apply, Algebra.id.smul_eq_mul, mul_one]

Evaluation of Formal Multilinear Series as Product Times Coefficient

Informal description

Let $p$ be a formal multilinear series over a field $\mathbb{K}$ from $\mathbb{K}$ to a topological module $E$, and let $n$ be a natural number. For any vector $y \in \mathbb{K}^n$, the evaluation of the $n$-th term $p_n$ at $y$ is equal to the product of the components of $y$ multiplied by the $n$-th coefficient of $p$, i.e., \[ p_n(y) = \left(\prod_{i=1}^n y_i\right) \cdot p_n(1, \dots, 1). \]

FormalMultilinearSeries.coeff_eq_zero theorem

: p.coeff n = 0 ↔ p n = 0

Full source

theorem coeff_eq_zero : p.coeff n = 0 ↔ p n = 0 := by
  rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.mkPiRing_eq_zero_iff]

Vanishing of Coefficient in Formal Multilinear Series if and only if Term is Zero

Informal description

For a formal multilinear series $p$ from $\mathbb{K}$ to $E$ and any natural number $n$, the $n$-th coefficient of $p$ is zero if and only if the $n$-th term of $p$ is the zero multilinear map. That is, \[ p_n(1, \dots, 1) = 0 \leftrightarrow p_n = 0. \]

FormalMultilinearSeries.apply_eq_pow_smul_coeff theorem

: (p n fun _ => z) = z ^ n • p.coeff n

Full source

theorem apply_eq_pow_smul_coeff : (p n fun _ => z) = z ^ n • p.coeff n := by simp

Evaluation of Formal Multilinear Series on Constant Vector as Power Times Coefficient

Informal description

Let $p$ be a formal multilinear series over a field $\mathbb{K}$ from $\mathbb{K}$ to a topological module $E$. For any natural number $n$ and any element $z \in \mathbb{K}$, the evaluation of the $n$-th term $p_n$ at the constant vector $(z, \dots, z) \in \mathbb{K}^n$ is equal to $z^n$ multiplied by the $n$-th coefficient of $p$, i.e., \[ p_n(z, \dots, z) = z^n \cdot p_n(1, \dots, 1). \]

FormalMultilinearSeries.norm_apply_eq_norm_coef theorem

: ‖p n‖ = ‖coeff p n‖

Full source

@[simp]
theorem norm_apply_eq_norm_coef : ‖p n‖ = ‖coeff p n‖ := by
  rw [← mkPiRing_coeff_eq p, ContinuousMultilinearMap.norm_mkPiRing]

Operator Norm of Formal Multilinear Series Term Equals Norm of Its Coefficient: $\|p_n\| = \|p_n(1, \dots, 1)\|$

Informal description

For any formal multilinear series $p$ over a field $\mathbb{K}$ from $\mathbb{K}$ to a topological module $E$, the operator norm of the $n$-th term $p_n$ is equal to the norm of its coefficient $p_n(1, \dots, 1)$. That is, \[ \|p_n\| = \|p_n(1, \dots, 1)\|. \]

FormalMultilinearSeries.fslope definition

(p : FormalMultilinearSeries 𝕜 𝕜 E) : FormalMultilinearSeries 𝕜 𝕜 E

Full source

/-- 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. -/
noncomputable def fslope (p : FormalMultilinearSeries 𝕜 𝕜 E) : FormalMultilinearSeries 𝕜 𝕜 E :=
  fun n => (p (n + 1)).curryLeft 1

Formal slope of a multilinear series

Informal description

Given a formal multilinear series $p$ over a field $\mathbb{K}$ from $\mathbb{K}$ to a topological module $E$, the *formal slope* of $p$ is the formal multilinear series defined by $(p.\text{fslope})_n = (p_{n+1}).\text{curryLeft}(1)$ for each $n$, where $\text{curryLeft}(1)$ denotes the partial application of the first argument to $1 \in \mathbb{K}$. This operation corresponds to the expansion of $(f(z) - f(0))/z$ in power series, where if $f$ has $p$ as its power series expansion, then $\text{dslope}(f)$ has $p.\text{fslope}$ as its power series expansion.

FormalMultilinearSeries.coeff_fslope theorem

: p.fslope.coeff n = p.coeff (n + 1)

Full source

@[simp]
theorem coeff_fslope : p.fslope.coeff n = p.coeff (n + 1) := by
  simp only [fslope, coeff, ContinuousMultilinearMap.curryLeft_apply]
  congr 1
  exact Fin.cons_self_tail (fun _ => (1 : 𝕜))

Coefficient relation between formal slope and original series: $(p.\text{fslope})_n = p_{n+1}$

Informal description

For any formal multilinear series $p$ over a field $\mathbb{K}$ from $\mathbb{K}$ to a topological module $E$, the $n$-th coefficient of the formal slope of $p$ is equal to the $(n+1)$-th coefficient of $p$. In other words, $(p.\text{fslope})_n(1, \dots, 1) = p_{n+1}(1, \dots, 1)$ for all $n \in \mathbb{N}$.

FormalMultilinearSeries.coeff_iterate_fslope theorem

(k n : ℕ) : (fslope^[k] p).coeff n = p.coeff (n + k)

Full source

@[simp]
theorem coeff_iterate_fslope (k n : ℕ) : (fslopefslope^[k] p).coeff n = p.coeff (n + k) := by
  induction k generalizing p with
  | zero => rfl
  | succ k ih => simp [ih, add_assoc]

Iterated Formal Slope Coefficient Relation: $(p.\text{fslope}^k)_n = p_{n+k}$

Informal description

For any natural numbers $k$ and $n$, the $n$-th coefficient of the $k$-th iterate of the formal slope of a formal multilinear series $p$ over a field $\mathbb{K}$ from $\mathbb{K}$ to a topological module $E$ is equal to the $(n+k)$-th coefficient of $p$. That is, $(p.\text{fslope}^k)_n(1, \dots, 1) = p_{n+k}(1, \dots, 1)$.

constFormalMultilinearSeries definition

 (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*) [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ContinuousConstSMul 𝕜 E]
  [IsTopologicalAddGroup E] {F : Type*} [NormedAddCommGroup F] [IsTopologicalAddGroup F] [NormedSpace 𝕜 F]
  [ContinuousConstSMul 𝕜 F] (c : F) : FormalMultilinearSeries 𝕜 E F

Full source

/-- 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. -/
def constFormalMultilinearSeries (𝕜 : Type*) [NontriviallyNormedField 𝕜] (E : Type*)
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [ContinuousConstSMul 𝕜 E] [IsTopologicalAddGroup E]
    {F : Type*} [NormedAddCommGroup F] [IsTopologicalAddGroup F] [NormedSpace 𝕜 F]
    [ContinuousConstSMul 𝕜 F] (c : F) : FormalMultilinearSeries 𝕜 E F
  | 0 => ContinuousMultilinearMap.uncurry0 _ _ c
  | _ => 0

Constant formal multilinear series

Informal description

The constant formal multilinear series over a nontrivially normed field $\mathbb{K}$, from a normed space $E$ to another normed space $F$, is defined such that its zeroth term is the constant multilinear map sending any input to $c \in F$, and all higher-degree terms are identically zero. More precisely: - For $n = 0$, it is the constant map $c$ (viewed as a 0-multilinear map). - For $n > 0$, it is the zero map. This represents the power series expansion of the constant function $f(x) = c$.

constFormalMultilinearSeries_apply theorem

 [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F}
  {n : ℕ} (hn : n ≠ 0) : constFormalMultilinearSeries 𝕜 E c n = 0

Full source

@[simp]
theorem constFormalMultilinearSeries_apply [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {c : F} {n : ℕ} (hn : n ≠ 0) :
    constFormalMultilinearSeries 𝕜 E c n = 0 :=
  Nat.casesOn n (fun hn => (hn rfl).elim) (fun _ _ => rfl) hn

Vanishing of Higher Terms in Constant Formal Multilinear Series

Informal description

For any nontrivially normed field $\mathbb{K}$, normed spaces $E$ and $F$ over $\mathbb{K}$, and element $c \in F$, the $n$-th term of the constant formal multilinear series $\text{constFormalMultilinearSeries}_{\mathbb{K},E}(c)$ is the zero map for all $n \neq 0$.

constFormalMultilinearSeries_zero theorem

 [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] :
  constFormalMultilinearSeries 𝕜 E (0 : F) = 0

Full source

@[simp]
lemma constFormalMultilinearSeries_zero [NontriviallyNormedField 𝕜] [NormedAddCommGroup E ]
    [NormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] :
    constFormalMultilinearSeries 𝕜 E (0 : F) = 0 := by
  ext n x
  simp only [FormalMultilinearSeries.zero_apply, ContinuousMultilinearMap.zero_apply,
    constFormalMultilinearSeries]
  induction n
  · simp only [ContinuousMultilinearMap.uncurry0_apply]
  · simp only [constFormalMultilinearSeries.match_1.eq_2, ContinuousMultilinearMap.zero_apply]

Vanishing of Constant Formal Multilinear Series at Zero

Informal description

The constant formal multilinear series from a normed space $E$ to a normed space $F$ over a nontrivially normed field $\mathbb{K}$, evaluated at the zero element $0 \in F$, is identically zero. That is, $\text{constFormalMultilinearSeries}_{\mathbb{K},E}(0) = 0$.

ContinuousLinearMap.fpowerSeries definition

(f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F

Full source

/-- Formal power series of a continuous linear map `f : E →L[𝕜] F` at `x : E`:
`f y = f x + f (y - x)`. -/
def fpowerSeries (f : E →L[𝕜] F) (x : E) : FormalMultilinearSeries 𝕜 E F
  | 0 => ContinuousMultilinearMap.uncurry0 𝕜 _ (f x)
  | 1 => (continuousMultilinearCurryFin1 𝕜 E F).symm f
  | _ => 0

Formal multilinear series of a continuous linear map at a point

Informal description

Given a continuous linear map $ f : E \to F $ between normed spaces over a field $ \mathbb{K} $ and a point $ x \in E $, the formal multilinear series $ f.\text{fpowerSeries} \, x $ is defined as follows: - For $ n = 0 $, it is the constant map $ \text{uncurry0} \, (f x) $, which takes no arguments and returns $ f x $. - For $ n = 1 $, it is the linear map $ f $ itself (viewed as a 1-multilinear map via currying). - For $ n \geq 2 $, it is the zero map. This series models the derivatives of $ f $ at $ x $, where only the constant and linear terms are non-zero.

ContinuousLinearMap.fpowerSeries_apply_zero theorem

(f : E →L[𝕜] F) (x : E) : f.fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ (f x)

Full source

@[simp]
theorem fpowerSeries_apply_zero (f : E →L[𝕜] F) (x : E) :
    f.fpowerSeries x 0 = ContinuousMultilinearMap.uncurry0 𝕜 _ (f x) :=
  rfl

Zeroth Term of Formal Multilinear Series for Continuous Linear Map

Informal description

For any continuous linear map $f \colon E \to F$ between normed spaces over a field $\mathbb{K}$ and any point $x \in E$, the zeroth term of the formal multilinear series associated to $f$ at $x$ is equal to the constant multilinear map that takes no arguments and returns $f(x)$. In other words, $(f.\text{fpowerSeries}\,x)_0 = \text{uncurry0}\,(f x)$.

ContinuousLinearMap.fpowerSeries_apply_one theorem

(f : E →L[𝕜] F) (x : E) : f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f

Full source

@[simp]
theorem fpowerSeries_apply_one (f : E →L[𝕜] F) (x : E) :
    f.fpowerSeries x 1 = (continuousMultilinearCurryFin1 𝕜 E F).symm f :=
  rfl

First Term of Formal Multilinear Series for Continuous Linear Map

Informal description

For any continuous linear map $ f : E \to F $ between normed spaces over a field $ \mathbb{K} $ and any point $ x \in E $, the first term of the formal multilinear series $ f.\text{fpowerSeries} \, x $ at index 1 is equal to the inverse of the continuous multilinear currying isomorphism applied to $ f $. In other words, the linear term of the series corresponds to $ f $ itself viewed as a 1-multilinear map.

ContinuousLinearMap.fpowerSeries_apply_add_two theorem

(f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fpowerSeries x (n + 2) = 0

Full source

@[simp]
theorem fpowerSeries_apply_add_two (f : E →L[𝕜] F) (x : E) (n : ℕ) : f.fpowerSeries x (n + 2) = 0 :=
  rfl

Vanishing of Higher Order Terms in Formal Multilinear Series of a Continuous Linear Map

Informal description

For any continuous linear map $f \colon E \to F$ between normed spaces over a field $\mathbb{K}$, any point $x \in E$, and any natural number $n$, the $(n+2)$-th term of the formal multilinear series associated to $f$ at $x$ is the zero map, i.e., $f.\text{fpowerSeries}\, x\, (n + 2) = 0$.

Mathlib.Analysis.Calculus.FormalMultilinearSeries

Notations

Tags