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)
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup 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.
Equations
- FormalMultilinearSeries 𝕜 E F = ((n : ℕ) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F)
Instances For
instance
instAddCommGroupFormalMultilinearSeries
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
:
AddCommGroup (FormalMultilinearSeries 𝕜 E F)
Equations
- instAddCommGroupFormalMultilinearSeries = inferInstanceAs (AddCommGroup ((n : ℕ) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F))
instance
instInhabitedFormalMultilinearSeries
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
:
Inhabited (FormalMultilinearSeries 𝕜 E F)
Equations
- instInhabitedFormalMultilinearSeries = { default := 0 }
instance
instModuleFormalMultilinearSeriesToAddCommMonoidInstAddCommGroupFormalMultilinearSeries
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(𝕜' : Type u_1)
[Semiring 𝕜']
[Module 𝕜' F]
[ContinuousConstSMul 𝕜' F]
[SMulCommClass 𝕜 𝕜' F]
:
Module 𝕜' (FormalMultilinearSeries 𝕜 E F)
Equations
- instModuleFormalMultilinearSeriesToAddCommMonoidInstAddCommGroupFormalMultilinearSeries 𝕜' = inferInstanceAs (Module 𝕜' ((n : ℕ) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F))
@[simp]
theorem
FormalMultilinearSeries.zero_apply
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(n : ℕ)
:
0 n = 0
@[simp]
theorem
FormalMultilinearSeries.neg_apply
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(f : FormalMultilinearSeries 𝕜 E F)
(n : ℕ)
:
theorem
FormalMultilinearSeries.ext
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E F}
(h : ∀ (n : ℕ), p n = q n)
:
p = q
theorem
FormalMultilinearSeries.ext_iff
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E F}
:
theorem
FormalMultilinearSeries.ne_iff
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
{q : FormalMultilinearSeries 𝕜 E F}
:
def
FormalMultilinearSeries.prod
{𝕜 : Type u}
{E : Type v}
{F : Type w}
{G : Type x}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[AddCommGroup G]
[Module 𝕜 G]
[TopologicalSpace G]
[TopologicalAddGroup 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).
Equations
- FormalMultilinearSeries.prod p q x = let n := x; ContinuousMultilinearMap.prod (p n) (q n)
Instances For
def
FormalMultilinearSeries.removeZero
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F)
:
FormalMultilinearSeries 𝕜 E F
Killing the zeroth coefficient in a formal multilinear series
Equations
- FormalMultilinearSeries.removeZero p x = match x with | 0 => 0 | Nat.succ n => p (n + 1)
Instances For
@[simp]
theorem
FormalMultilinearSeries.removeZero_coeff_zero
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F)
:
@[simp]
theorem
FormalMultilinearSeries.removeZero_coeff_succ
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F)
(n : ℕ)
:
FormalMultilinearSeries.removeZero p (n + 1) = p (n + 1)
theorem
FormalMultilinearSeries.removeZero_of_pos
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
(p : FormalMultilinearSeries 𝕜 E F)
{n : ℕ}
(h : 0 < n)
:
FormalMultilinearSeries.removeZero p n = p n
theorem
FormalMultilinearSeries.congr
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup 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 { val := i, isLt := him } = w { val := i, isLt := 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
FormalMultilinearSeries.compContinuousLinearMap
{𝕜 : Type u}
{E : Type v}
{F : Type w}
{G : Type x}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[AddCommGroup G]
[Module 𝕜 G]
[TopologicalSpace G]
[TopologicalAddGroup 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.
Equations
- FormalMultilinearSeries.compContinuousLinearMap p u n = ContinuousMultilinearMap.compContinuousLinearMap (p n) fun (x : Fin n) => u
Instances For
@[simp]
theorem
FormalMultilinearSeries.compContinuousLinearMap_apply
{𝕜 : Type u}
{E : Type v}
{F : Type w}
{G : Type x}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[AddCommGroup G]
[Module 𝕜 G]
[TopologicalSpace G]
[TopologicalAddGroup G]
[ContinuousConstSMul 𝕜 G]
(p : FormalMultilinearSeries 𝕜 F G)
(u : E →L[𝕜] F)
(n : ℕ)
(v : Fin n → E)
:
(FormalMultilinearSeries.compContinuousLinearMap p u n) v = (p n) (⇑u ∘ v)
def
FormalMultilinearSeries.restrictScalars
(𝕜 : Type u)
{𝕜' : Type u'}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[Ring 𝕜']
[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.
Equations
Instances For
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.
Equations
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ContinuousLinearMap.compFormalMultilinearSeries
{𝕜 : Type u}
{E : Type v}
{F : Type w}
{G : Type x}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[AddCommGroup G]
[Module 𝕜 G]
[TopologicalSpace G]
[TopologicalAddGroup 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ₙ.
Equations
Instances For
@[simp]
theorem
ContinuousLinearMap.compFormalMultilinearSeries_apply
{𝕜 : Type u}
{E : Type v}
{F : Type w}
{G : Type x}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[AddCommGroup G]
[Module 𝕜 G]
[TopologicalSpace G]
[TopologicalAddGroup G]
[ContinuousConstSMul 𝕜 G]
(f : F →L[𝕜] G)
(p : FormalMultilinearSeries 𝕜 E F)
(n : ℕ)
:
theorem
ContinuousLinearMap.compFormalMultilinearSeries_apply'
{𝕜 : Type u}
{E : Type v}
{F : Type w}
{G : Type x}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
[AddCommGroup G]
[Module 𝕜 G]
[TopologicalSpace G]
[TopologicalAddGroup G]
[ContinuousConstSMul 𝕜 G]
(f : F →L[𝕜] G)
(p : FormalMultilinearSeries 𝕜 E F)
(n : ℕ)
(v : Fin n → E)
:
(ContinuousLinearMap.compFormalMultilinearSeries f p n) v = f ((p n) v)
noncomputable def
ContinuousMultilinearMap.toFormalMultilinearSeries
{𝕜 : Type u}
{F : Type w}
[Ring 𝕜]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{ι : Type u_1}
{E : ι → Type u_2}
[(i : ι) → AddCommGroup (E i)]
[(i : ι) → Module 𝕜 (E i)]
[(i : ι) → TopologicalSpace (E i)]
[∀ (i : ι), TopologicalAddGroup (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 ι).
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
FormalMultilinearSeries.order
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup 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.
Equations
- FormalMultilinearSeries.order p = sInf {n : ℕ | p n ≠ 0}
Instances For
@[simp]
theorem
FormalMultilinearSeries.order_zero
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
:
theorem
FormalMultilinearSeries.ne_zero_of_order_ne_zero
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
(hp : FormalMultilinearSeries.order p ≠ 0)
:
p ≠ 0
theorem
FormalMultilinearSeries.order_eq_find
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
[DecidablePred fun (n : ℕ) => p n ≠ 0]
(hp : ∃ (n : ℕ), p n ≠ 0)
:
theorem
FormalMultilinearSeries.order_eq_find'
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
[DecidablePred fun (n : ℕ) => p n ≠ 0]
(hp : p ≠ 0)
:
FormalMultilinearSeries.order p = Nat.find (_ : ∃ (n : ℕ), p n ≠ 0 n)
theorem
FormalMultilinearSeries.order_eq_zero_iff'
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
:
theorem
FormalMultilinearSeries.order_eq_zero_iff
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
(hp : p ≠ 0)
:
FormalMultilinearSeries.order p = 0 ↔ p 0 ≠ 0
theorem
FormalMultilinearSeries.apply_order_ne_zero
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
(hp : p ≠ 0)
:
p (FormalMultilinearSeries.order p) ≠ 0
theorem
FormalMultilinearSeries.apply_order_ne_zero'
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
(hp : FormalMultilinearSeries.order p ≠ 0)
:
p (FormalMultilinearSeries.order p) ≠ 0
theorem
FormalMultilinearSeries.apply_eq_zero_of_lt_order
{𝕜 : Type u}
{E : Type v}
{F : Type w}
[Ring 𝕜]
{n : ℕ}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
[AddCommGroup F]
[Module 𝕜 F]
[TopologicalSpace F]
[TopologicalAddGroup F]
[ContinuousConstSMul 𝕜 F]
{p : FormalMultilinearSeries 𝕜 E F}
(hp : n < FormalMultilinearSeries.order p)
:
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.
Equations
- FormalMultilinearSeries.coeff p n = (p n) 1
Instances For
theorem
FormalMultilinearSeries.mkPiRing_coeff_eq
{𝕜 : Type u}
{E : Type v}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
(p : FormalMultilinearSeries 𝕜 𝕜 E)
(n : ℕ)
:
ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (FormalMultilinearSeries.coeff p 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 = (Finset.prod Finset.univ fun (i : Fin n) => y i) • FormalMultilinearSeries.coeff p n
theorem
FormalMultilinearSeries.coeff_eq_zero
{𝕜 : Type u}
{E : Type v}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{p : FormalMultilinearSeries 𝕜 𝕜 E}
{n : ℕ}
:
FormalMultilinearSeries.coeff p n = 0 ↔ p n = 0
@[simp]
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 • FormalMultilinearSeries.coeff p n
@[simp]
theorem
FormalMultilinearSeries.norm_apply_eq_norm_coef
{𝕜 : Type u}
{E : Type v}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{p : FormalMultilinearSeries 𝕜 𝕜 E}
{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.
Equations
- FormalMultilinearSeries.fslope p n = (ContinuousMultilinearMap.curryLeft (p (n + 1))) 1
Instances For
@[simp]
theorem
FormalMultilinearSeries.coeff_fslope
{𝕜 : Type u}
{E : Type v}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{p : FormalMultilinearSeries 𝕜 𝕜 E}
{n : ℕ}
:
@[simp]
theorem
FormalMultilinearSeries.coeff_iterate_fslope
{𝕜 : Type u}
{E : Type v}
[NontriviallyNormedField 𝕜]
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{p : FormalMultilinearSeries 𝕜 𝕜 E}
(k : ℕ)
(n : ℕ)
:
def
constFormalMultilinearSeries
(𝕜 : Type u_1)
[NontriviallyNormedField 𝕜]
(E : Type u_2)
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[ContinuousConstSMul 𝕜 E]
[TopologicalAddGroup E]
{F : Type u_3}
[NormedAddCommGroup F]
[TopologicalAddGroup 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.
Equations
- constFormalMultilinearSeries 𝕜 E c x = match x with | 0 => ContinuousMultilinearMap.curry0 𝕜 E c | x => 0
Instances For
@[simp]
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
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).
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
ContinuousLinearMap.fpowerSeries f x 0 = ContinuousMultilinearMap.curry0 𝕜 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)
:
@[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 : ℕ)
:
ContinuousLinearMap.fpowerSeries f x (n + 2) = 0