# Faa di Bruno formula #

The Faa di Bruno formula gives the iterated derivative of `g ∘ f` in terms of those of `g` and `f`. It is expressed in terms of partitions `I` of `{0, ..., n-1}`. For such a partition, denote by `k` its number of parts, write the parts as `I₀, ..., Iₖ₋₁` ordered so that `max I₀ < ... < max Iₖ₋₁`, and let `iₘ` be the number of elements of `Iₘ`. Then `D^n (g ∘ f) (x) (v₀, ..., vₙ₋₁) = ∑_{I partition of {0, ..., n-1}} D^k g (f x) (D^{i₀} f (x) (v_{I₀}), ..., D^{iₖ₋₁} f (x) (v_{Iₖ₋₁}))` where by `v_{Iₘ}` we mean the vectors `vᵢ` with indices in `Iₘ`, i.e., the composition of `v` with the increasing embedding of `Fin iₘ` into `Fin n` with range `Iₘ`.

For instance, for `n = 2`, there are 2 partitions of `{0, 1}`, given by `{0}, {1}` and `{0, 1}`, and therefore `D^2(g ∘ f) (x) (v₀, v₁) = D^2 g (f x) (Df (x) v₀, Df (x) v₁) + Dg (f x) (D^2f (x) (v₀, v₁))`.

The formula is straightforward to prove by induction, as differentiating `D^k g (f x) (D^{i₀} f (x) (v_{I₀}), ..., D^{iₖ₋₁} f (x) (v_{Iₖ₋₁}))` gives a sum with `k + 1` terms where one differentiates either `D^k g (f x)`, or one of the `D^{iₘ} f (x)`, amounting to adding to the partition `I` either a new atom `{-1}` to its left, or extending `Iₘ` by adding `-1` to it. In this way, one obtains bijectively all partitions of `{-1, ..., n}`, and the proof can go on (up to relabelling).

The main difficulty is to write things down in a precise language, namely to write `D^k g (f x) (D^{i₀} f (x) (v_{I₀}), ..., D^{iₖ₋₁} f (x) (v_{Iₖ₋₁}))` as a continuous multilinear map of the `vᵢ`. For this, instead of working with partitions of `{0, ..., n-1}` and ordering their parts, we work with partitions in which the ordering is part of the data -- this is equivalent, but much more convenient to implement. We call these `OrderedFinpartition n`.

Note that the implementation of `OrderedFinpartition` is very specific to the Faa di Bruno formula: as testified by the formula above, what matters is really the embedding of the parts in `Fin n`, and moreover the parts have to be ordered by `max I₀ < ... < max Iₖ₋₁` for the formula to hold in the general case where the iterated differential might not be symmetric. The defeqs with respect to `Fin.cons` are also important when doing the induction. For this reason, we do not expect this class to be useful beyond the Faa di Bruno formula, which is why it is in this file instead of a dedicated file in the `Combinatorics` folder.

## Main results #

Given `c : OrderedFinpartition n` and two formal multilinear series `q` and `p`, we define `c.compAlongOrderedFinpartition q p` as an `n`-multilinear map given by the formula above, i.e., `(v₁, ..., vₙ) ↦ qₖ (p_{i₁} (v_{I₁}), ..., p_{iₖ} (v_{Iₖ}))`.

Then, we define `q.taylorComp p` as a formal multilinear series whose `n`-th term is the sum of `c.compAlongOrderedFinpartition q p` over all ordered finpartitions of size `n`.

Finally, we prove in `HasFTaylorSeriesUptoOn.comp` that, if two functions `g` and `f` have Taylor series up to `n` given by `q` and `p`, then `g ∘ f` also has a Taylor series, given by `q.taylorComp p`.

## Implementation #

A first technical difficulty is to implement the extension process of `OrderedFinpartition` corresponding to adding a new atom, or appending an atom to an existing part, and defining the associated increasing parameterizations that show up in the definition of `compAlongOrderedFinpartition`.

Then, one has to show that the ordered finpartitions thus obtained give exactly all ordered finpartitions of order `n+1`. For this, we define the inverse process (shrinking a finpartition of `n+1` by erasing `0`, either as an atom or from the part that contains it), and we show that these processes are inverse to each other, yielding an equivalence between `(c : OrderedFinpartition n) × Option (Fin c.length)` and `OrderedFinpartition (n + 1)`. This equivalence shows up prominently in the inductive proof of Faa di Bruno formula to identify the sums that show up.

source
structure OrderedFinpartition (n : ℕ) :
Type

A partition of `Fin n` into finitely many nonempty subsets, given by the increasing parameterization of these subsets. We order the subsets by increasing greatest element. This definition is tailored-made for the Faa di Bruno formula, and probably not useful elsewhere, because of the specific parameterization by `Fin n` and the peculiar ordering.

- length : ℕ

  The number of parts in the partition

- partSize : Fin self.length → ℕ

  The size of each part

- partSize_pos (m : Fin self.length) : 0 < self.partSize m
- emb (m : Fin self.length) : Fin (self.partSize m) → Fin n

  The increasing parameterization of each part

- emb_strictMono (m : Fin self.length) : StrictMono (self.emb m)
- parts_strictMono : StrictMono fun (m : Fin self.length) => self.emb m ⟨self.partSize m - 1, ⋯⟩

  The parts are ordered by increasing greatest element.

- disjoint : Set.univ.PairwiseDisjoint fun (m : Fin self.length) => Set.range (self.emb m)

  The parts are disjoint

- cover (x : Fin n) : ∃ (m : Fin self.length), x ∈ Set.range (self.emb m)

  The parts cover everything

Instances For

source
theorem OrderedFinpartition.ext_iff {n : ℕ} {x y : OrderedFinpartition n} :
x = y ↔ x.length = y.length ∧ x.partSize ≍ y.partSize ∧ x.emb ≍ y.emb
source
theorem OrderedFinpartition.ext {n : ℕ} {x y : OrderedFinpartition n} (length : x.length = y.length) (partSize : x.partSize ≍ y.partSize) (emb : x.emb ≍ y.emb) :
x = y
source
instance instDecidableEqOrderedFinpartition {n✝ : ℕ} :
DecidableEq (OrderedFinpartition n✝)
Equations

- instDecidableEqOrderedFinpartition = instDecidableEqOrderedFinpartition.decEq

source
def instDecidableEqOrderedFinpartition.decEq {n✝ : ℕ} (x✝ x✝¹ : OrderedFinpartition n✝) :
Decidable (x✝ = x✝¹)
Equations

- One or more equations did not get rendered due to their size.

Instances For

### Basic API for ordered finpartitions #

source
def OrderedFinpartition.atomic (n : ℕ) :
OrderedFinpartition n

The ordered finpartition of `Fin n` into singletons.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderedFinpartition.atomic_partSize (n : ℕ) :
(atomic n).partSize = fun (x : Fin n) => 1
source
@[simp]
theorem OrderedFinpartition.atomic_length (n : ℕ) :
(atomic n).length = n
source
@[simp]
theorem OrderedFinpartition.atomic_emb (n : ℕ) :
(atomic n).emb = fun (m : Fin n) (x : Fin 1) => m
source
instance OrderedFinpartition.instInhabited {n : ℕ} :
Inhabited (OrderedFinpartition n)
Equations

- OrderedFinpartition.instInhabited = { default := OrderedFinpartition.atomic n }

source
@[simp]
theorem OrderedFinpartition.default_eq {n : ℕ} :
default = atomic n
source
theorem OrderedFinpartition.length_le {n : ℕ} (c : OrderedFinpartition n) :
c.length ≤ n
source
theorem OrderedFinpartition.partSize_le {n : ℕ} (c : OrderedFinpartition n) (m : Fin c.length) :
c.partSize m ≤ n
source
def OrderedFinpartition.embSigma (n : ℕ) :
OrderedFinpartition n → (l : Fin (n + 1)) × (p : Fin ↑l → Fin (n + 1)) × ((i : Fin ↑l) → Fin ↑(p i) → Fin n)

Embedding of ordered finpartitions in a sigma type. The sigma type on the right is quite big, but this is enough to get finiteness of ordered finpartitions.

Equations

- OrderedFinpartition.embSigma n c = ⟨⟨c.length, ⋯⟩, ⟨fun (m : Fin ↑⟨c.length, ⋯⟩) => ⟨c.partSize m, ⋯⟩, fun (j : Fin ↑⟨c.length, ⋯⟩) => c.emb j⟩⟩

Instances For

source
theorem OrderedFinpartition.injective_embSigma (n : ℕ) :
Function.Injective (embSigma n)
source
noncomputable instance OrderedFinpartition.instFintype {n : ℕ} :
Fintype (OrderedFinpartition n)
Equations

- OrderedFinpartition.instFintype = Fintype.ofInjective (OrderedFinpartition.embSigma n) ⋯

source
instance OrderedFinpartition.instUniqueZero :
Unique (OrderedFinpartition 0)
Equations

- OrderedFinpartition.instUniqueZero = Unique.mk' (OrderedFinpartition 0)

source
theorem OrderedFinpartition.exists_inverse {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) :
∃ (p : (m : Fin c.length) × Fin (c.partSize m)), c.emb p.fst p.snd = j
source
theorem OrderedFinpartition.emb_injective {n : ℕ} (c : OrderedFinpartition n) :
Function.Injective fun (p : (m : Fin c.length) × Fin (c.partSize m)) => c.emb p.fst p.snd
source
theorem OrderedFinpartition.emb_ne_emb_of_ne {n : ℕ} (c : OrderedFinpartition n) {i j : Fin c.length} {a : Fin (c.partSize i)} {b : Fin (c.partSize j)} (h : i ≠ j) :
c.emb i a ≠ c.emb j b
source
noncomputable def OrderedFinpartition.index {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) :
Fin c.length

Given `j : Fin n`, the index of the part to which it belongs.

Equations

- c.index j = ⋯.choose.fst

Instances For

source
noncomputable def OrderedFinpartition.invEmbedding {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) :
Fin (c.partSize (c.index j))

The inverse of `c.emb` for `c : OrderedFinpartition`. It maps `j : Fin n` to the point in `Fin (c.partSize (c.index j))` which is mapped back to `j` by `c.emb (c.index j)`.

Equations

- c.invEmbedding j = ⋯.choose.snd

Instances For

source
@[simp]
theorem OrderedFinpartition.emb_invEmbedding {n : ℕ} (c : OrderedFinpartition n) (j : Fin n) :
c.emb (c.index j) (c.invEmbedding j) = j
source
noncomputable def OrderedFinpartition.equivSigma {n : ℕ} (c : OrderedFinpartition n) :
(i : Fin c.length) × Fin (c.partSize i) ≃ Fin n

An ordered finpartition gives an equivalence between `Fin n` and the disjoint union of the parts, each of them parameterized by `Fin (c.partSize i)`.

Equations

- c.equivSigma = { toFun := fun (p : (i : Fin c.length) × Fin (c.partSize i)) => c.emb p.fst p.snd, invFun := fun (i : Fin n) => ⟨c.index i, c.invEmbedding i⟩, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
theorem OrderedFinpartition.prod_sigma_eq_prod {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} [CommMonoid α] (v : Fin n → α) :
∏ m : Fin c.length, ∏ r : Fin (c.partSize m), v (c.emb m r) = ∏ i : Fin n, v i
source
theorem OrderedFinpartition.sum_sigma_eq_sum {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} [AddCommMonoid α] (v : Fin n → α) :
∑ m : Fin c.length, ∑ r : Fin (c.partSize m), v (c.emb m r) = ∑ i : Fin n, v i
source
theorem OrderedFinpartition.length_pos {n : ℕ} (c : OrderedFinpartition n) (h : 0 < n) :
0 < c.length
source
theorem OrderedFinpartition.neZero_length {n : ℕ} [NeZero n] (c : OrderedFinpartition n) :
NeZero c.length
source
theorem OrderedFinpartition.neZero_partSize {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) :
NeZero (c.partSize i)
source
instance OrderedFinpartition.instUniqueOne :
Unique (OrderedFinpartition 1)
Equations

- OrderedFinpartition.instUniqueOne = { toInhabited := OrderedFinpartition.instInhabited, uniq := OrderedFinpartition.instUniqueOne._proof_1 }

source
theorem OrderedFinpartition.emb_zero {n : ℕ} (c : OrderedFinpartition n) [NeZero n] :
c.emb (c.index 0) 0 = 0
source
theorem OrderedFinpartition.partSize_eq_one_of_range_emb_eq_singleton {n : ℕ} (c : OrderedFinpartition n) {i : Fin c.length} {j : Fin n} (hc : Set.range (c.emb i) = {j}) :
c.partSize i = 1
source
theorem OrderedFinpartition.one_lt_partSize_index_zero {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) ≠ {0}) :
1 < c.partSize (c.index 0)

If the left-most part is not `{0}`, then the part containing `0` has at least two elements: either because it's the left-most part, and then it's not just `0` by assumption, or because it's not the left-most part and then, by increasingness of maximal elements in parts, it contains a positive element.

### Extending and shrinking ordered finpartitions #

We show how an ordered finpartition can be extended to the left, either by adding a new atomic part (in `extendLeft`) or adding the new element to an existing part (in `extendMiddle`). Conversely, one can shrink a finpartition by deleting the element to the left, with a different behavior if it was an atomic part (in `eraseLeft`, in which case the number of parts decreases by one) or if it belonged to a non-atomic part (in `eraseMiddle`, in which case the number of parts stays the same).

These operations are inverse to each other, giving rise to an equivalence between `((c : OrderedFinpartition n) × Option (Fin c.length))` and `OrderedFinpartition (n + 1)` called `OrderedFinPartition.extendEquiv`.

source
def OrderedFinpartition.extendLeft {n : ℕ} (c : OrderedFinpartition n) :
OrderedFinpartition (n + 1)

Extend an ordered partition of `n` entries, by adding a new singleton part to the left.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderedFinpartition.extendLeft_partSize {n : ℕ} (c : OrderedFinpartition n) :
c.extendLeft.partSize = Fin.cons 1 c.partSize
source
@[simp]
theorem OrderedFinpartition.extendLeft_length {n : ℕ} (c : OrderedFinpartition n) :
c.extendLeft.length = c.length + 1
source
@[simp]
theorem OrderedFinpartition.range_extendLeft_zero {n : ℕ} (c : OrderedFinpartition n) :
Set.range (c.extendLeft.emb 0) = {0}
source
def OrderedFinpartition.extendMiddle {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length) :
OrderedFinpartition (n + 1)

Extend an ordered partition of `n` entries, by adding to the `i`-th part a new point to the left.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderedFinpartition.extendMiddle_length {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length) :
(c.extendMiddle k).length = c.length
source
@[simp]
theorem OrderedFinpartition.extendMiddle_partSize {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length) :
(c.extendMiddle k).partSize = Function.update c.partSize k (c.partSize k + 1)
source
theorem OrderedFinpartition.index_extendMiddle_zero {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) :
(c.extendMiddle i).index 0 = i
source
theorem OrderedFinpartition.range_emb_extendMiddle_ne_singleton_zero {n : ℕ} (c : OrderedFinpartition n) (i j : Fin c.length) :
Set.range ((c.extendMiddle i).emb j) ≠ {0}
source
def OrderedFinpartition.extend {n : ℕ} (c : OrderedFinpartition n) (i : Option (Fin c.length)) :
OrderedFinpartition (n + 1)

Extend an ordered partition of `n` entries, by adding singleton to the left or appending it to one of the existing part.

Equations

- c.extend none = c.extendLeft
- c.extend (some i_2) = c.extendMiddle i_2

Instances For

source
@[simp]
theorem OrderedFinpartition.extend_none {n : ℕ} (c : OrderedFinpartition n) :
c.extend none = c.extendLeft
source
@[simp]
theorem OrderedFinpartition.extend_some {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) :
c.extend (some i) = c.extendMiddle i
source
def OrderedFinpartition.eraseLeft {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) = {0}) :
OrderedFinpartition n

Given an ordered finpartition of `n+1`, with a leftmost atom equal to `{0}`, remove this atom to form an ordered finpartition of `n`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def OrderedFinpartition.eraseMiddle {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) ≠ {0}) :
OrderedFinpartition n

Given an ordered finpartition of `n+1`, with a leftmost atom different from `{0}`, remove `{0}` from the atom that contains it, to form an ordered finpartition of `n`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def OrderedFinpartition.extendEquiv (n : ℕ) :
(c : OrderedFinpartition n) × Option (Fin c.length) ≃ OrderedFinpartition (n + 1)

Extending the ordered partitions of `Fin n` bijects with the ordered partitions of `Fin (n+1)`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderedFinpartition.extendEquiv_apply (n : ℕ) (c : (c : OrderedFinpartition n) × Option (Fin c.length)) :
(extendEquiv n) c = c.fst.extend c.snd

### Applying ordered finpartitions to multilinear maps #

source
def OrderedFinpartition.applyOrderedFinpartition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) :
(Fin n → E) → Fin c.length → F

Given a formal multilinear series `p`, an ordered partition `c` of `n` and the index `i` of a block of `c`, we may define a function on `Fin n → E` by picking the variables in the `i`-th block of `n`, and applying the corresponding coefficient of `p` to these variables. This function is called `p.applyOrderedFinpartition c v i` for `v : Fin n → E` and `i : Fin c.k`.

Equations

- c.applyOrderedFinpartition p v m = (p m) (v ∘ c.emb m)

Instances For

source
theorem OrderedFinpartition.applyOrderedFinpartition_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (v : Fin n → E) :
c.applyOrderedFinpartition p v = fun (m : Fin c.length) => (p m) (v ∘ c.emb m)
source
theorem OrderedFinpartition.norm_applyOrderedFinpartition_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (v : Fin n → E) (m : Fin c.length) :
‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i : Fin (c.partSize m), ‖v (c.emb m i)‖
source
theorem OrderedFinpartition.applyOrderedFinpartition_update_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (j : Fin n) (v : Fin n → E) (z : E) :
c.applyOrderedFinpartition p (Function.update v j z) = Function.update (c.applyOrderedFinpartition p v) (c.index j) ((p (c.index j)) (Function.update (v ∘ c.emb (c.index j)) (c.invEmbedding j) z))

Technical lemma stating how `c.applyOrderedFinpartition` commutes with updating variables. This will be the key point to show that functions constructed from `applyOrderedFinpartition` retain multilinearity.

source
theorem OrderedFinpartition.applyOrderedFinpartition_update_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (c : OrderedFinpartition n) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (m : Fin c.length) (v : Fin n → E) (q : ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize m)) => E) F) :
c.applyOrderedFinpartition (Function.update p m q) v = Function.update (c.applyOrderedFinpartition p v) m (q (v ∘ c.emb m))
source
def OrderedFinpartition.compAlongOrderedFinpartition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) :
ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G

Given a an ordered finite partition `c` of `n`, a continuous multilinear map `f` in `c.length` variables, and for each `m` a continuous multilinear map `p m` in `c.partSize m` variables, one can form a continuous multilinear map in `n` variables by applying `p m` to each part of the partition, and then applying `f` to the resulting vector. It is called `c.compAlongOrderedFinpartition f p`.

Equations

- c.compAlongOrderedFinpartition f p = { toMultilinearMap := MultilinearMap.mk' (fun (v : Fin n → E) => f (c.applyOrderedFinpartition p v)) ⋯ ⋯, cont := ⋯ }

Instances For

source
@[simp]
theorem OrderedFinpartition.compAlongOrderFinpartition_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (v : Fin n → E) :
(c.compAlongOrderedFinpartition f p) v = f (c.applyOrderedFinpartition p v)
source
theorem OrderedFinpartition.norm_compAlongOrderedFinpartition_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) :
‖c.compAlongOrderedFinpartition f p‖ ≤ ‖f‖ * ∏ i : Fin c.length, ‖p i‖
source
def OrderedFinpartition.compAlongOrderedFinpartitionₗ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) :
ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G →ₗ[𝕜] MultilinearMap 𝕜 (fun (i : Fin c.length) => ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G)

Bundled version of `compAlongOrderedFinpartition`, depending linearly on `f` and multilinearly on `p`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderedFinpartition.compAlongOrderedFinpartitionₗ_apply_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) :
(c.compAlongOrderedFinpartitionₗ f) p = c.compAlongOrderedFinpartition f p
source
noncomputable def OrderedFinpartition.compAlongOrderedFinpartitionL (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [NormedAddCommGroup E] [NormedSpace 𝕜 E] (F : Type u_3) [NormedAddCommGroup F] [NormedSpace 𝕜 F] (G : Type u_4) [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) :
ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) (ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G)

Bundled version of `compAlongOrderedFinpartition`, depending continuously linearly on `f` and continuously multilinearly on `p`.

Equations

- OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c = MultilinearMap.mkContinuousLinear c.compAlongOrderedFinpartitionₗ 1 ⋯

Instances For

source
@[simp]
theorem OrderedFinpartition.compAlongOrderedFinpartitionL_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) (f : ContinuousMultilinearMap 𝕜 (fun (i : Fin c.length) => F) G) (p : (i : Fin c.length) → ContinuousMultilinearMap 𝕜 (fun (i : Fin (c.partSize i)) => E) F) :
((compAlongOrderedFinpartitionL 𝕜 E F G c) f) p = c.compAlongOrderedFinpartition f p
source
theorem OrderedFinpartition.norm_compAlongOrderedFinpartitionL_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (c : OrderedFinpartition n) :
‖compAlongOrderedFinpartitionL 𝕜 E F G c‖ ≤ 1

### The Faa di Bruno formula #

source
def FormalMultilinearSeries.compAlongOrderedFinpartition {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition n) :
ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) G

Given two formal multilinear series `q` and `p` and a composition `c` of `n`, one may form a continuous multilinear map in `n` variables by applying the right coefficient of `p` to each block of the composition, and then applying `q c.length` to the resulting vector. It is called `q.compAlongComposition p c`.

Equations

- q.compAlongOrderedFinpartition p c = c.compAlongOrderedFinpartition (q c.length) fun (m : Fin c.length) => p (c.partSize m)

Instances For

source
@[simp]
theorem FormalMultilinearSeries.compAlongOrderedFinpartition_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition n) (v : Fin n → E) :
(q.compAlongOrderedFinpartition p c) v = (q c.length) (c.applyOrderedFinpartition (fun (m : Fin c.length) => p (c.partSize m)) v)
source
noncomputable def FormalMultilinearSeries.taylorComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G) (p : FormalMultilinearSeries 𝕜 E F) :
FormalMultilinearSeries 𝕜 E G

Taylor formal composition of two formal multilinear series. The `n`-th coefficient in the composition is defined to be the sum of `q.compAlongOrderedFinpartition p c` over all ordered partitions of `n`. In other words, this term (as a multilinear function applied to `v₀, ..., vₙ₋₁`) is `∑'_{k} ∑'_{I₀ ⊔ ... ⊔ Iₖ₋₁ = {0, ..., n-1}} qₖ (p_{i₀} (...), ..., p_{iₖ₋₁} (...))`, where `iₘ` is the size of `Iₘ` and one puts all variables of `Iₘ` as arguments to `p_{iₘ}`, in increasing order. The sets `I₀, ..., Iₖ₋₁` are ordered so that `max I₀ < max I₁ < ... < max Iₖ₋₁`.

This definition is chosen so that the `n`-th derivative of `g ∘ f` is the Taylor composition of the iterated derivatives of `g` and of `f`.

Not to be confused with another notion of composition for formal multilinear series, called just `FormalMultilinearSeries.comp`, appearing in the composition of analytic functions.

Equations

- q.taylorComp p n = ∑ c : OrderedFinpartition n, q.compAlongOrderedFinpartition p c

Instances For

source
theorem analyticOn_taylorComp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {t : Set F} {q : F → FormalMultilinearSeries 𝕜 F G} {p : E → FormalMultilinearSeries 𝕜 E F} (hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun (x : F) => q x n) t) (hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun (x : E) => p x n) s) {f : E → F} (hf : AnalyticOn 𝕜 f s) (h : Set.MapsTo f s t) (n : ℕ) :
AnalyticOn 𝕜 (fun (x : E) => (q (f x)).taylorComp (p x) n) s
source
theorem HasFTaylorSeriesUpToOn.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {t : Set F} {q : F → FormalMultilinearSeries 𝕜 F G} {p : E → FormalMultilinearSeries 𝕜 E F} {n : WithTop ℕ∞} {g : F → G} {f : E → F} (hg : HasFTaylorSeriesUpToOn n g q t) (hf : HasFTaylorSeriesUpToOn n f p s) (h : Set.MapsTo f s t) :
HasFTaylorSeriesUpToOn n (g ∘ f) (fun (x : E) => (q (f x)).taylorComp (p x)) s

Faa di Bruno formula: If two functions `g` and `f` have Taylor series up to `n` given by `q` and `p`, then `g ∘ f` also has a Taylor series, given by `q.taylorComp p`.