The finite-dimensional multivariate Faà di Bruno formula

Mathlib's OrderedFinpartition representation is the coordinate-free form of the multivariate formula: its parts group the input derivative directions that enter each derivative of the inner map. The paper-form sum is defined separately below; identifying its terms with fibers of the ordered-partition sum remains a separate combinatorial theorem.

theorem AVenhance.FaaDiBruno.multivariateFaaDiBruno {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] {h : F → G} {g : E → F} {x : E} {n : ℕ} (hh : ContDiffAt ℝ (↑n) h (g x)) (hg : ContDiffAt ℝ (↑n) g x) : iteratedFDeriv ℝ n (h ∘ g) x = ∑ c : OrderedFinpartition n, (ftaylorSeries ℝ h (g x)).compAlongOrderedFinpartition (ftaylorSeries ℝ g x) c

The n-th derivative of a composition, expanded over ordered set partitions of its n coordinate directions. This is Mathlib's Faà di Bruno formula, stated for arbitrary real normed spaces so it specializes to Vec d → Vec d and Vec d → ℝ.

@[reducible, inline]

abbrev AVenhance.FaaDiBruno.PaperMultiIndex (d : ℕ) : Type

A paper multi-index is a coordinatewise multiplicity vector.

Equations

• AVenhance.FaaDiBruno.PaperMultiIndex d = (Fin d → ℕ)

def AVenhance.FaaDiBruno.paperMultiIndexSize {d : ℕ} (α : PaperMultiIndex d) : ℕ

The order of a paper multi-index.

Equations

• AVenhance.FaaDiBruno.paperMultiIndexSize α = ∑ i : Fin d, α i

theorem AVenhance.FaaDiBruno.paperMultiIndex_coord_le_size {d : ℕ} (α : PaperMultiIndex d) (i : Fin d) : α i ≤ paperMultiIndexSize α

def AVenhance.FaaDiBruno.PaperMultiIndexUpTo (d n : ℕ) : Type

The finite range of nonzero multi-indices of order at most n.

Equations

• AVenhance.FaaDiBruno.PaperMultiIndexUpTo d n = { α : AVenhance.FaaDiBruno.PaperMultiIndex d // 1 ≤ AVenhance.FaaDiBruno.paperMultiIndexSize α ∧ AVenhance.FaaDiBruno.paperMultiIndexSize α ≤ n }

theorem AVenhance.FaaDiBruno.PaperMultiIndexUpTo.finite {d n : ℕ} : Finite (PaperMultiIndexUpTo d n)

instance AVenhance.FaaDiBruno.PaperMultiIndexUpTo.instFinite {d n : ℕ} : Finite (PaperMultiIndexUpTo d n)

@[instance_reducible]

noncomputable instance AVenhance.FaaDiBruno.PaperMultiIndexUpTo.instFintype {d n : ℕ} : Fintype (PaperMultiIndexUpTo d n)

Equations

• AVenhance.FaaDiBruno.PaperMultiIndexUpTo.instFintype = Fintype.ofFinite (AVenhance.FaaDiBruno.PaperMultiIndexUpTo d n)

def AVenhance.FaaDiBruno.paperMultiIndexLT {d : ℕ} (α β : PaperMultiIndex d) : Prop

Graded lexicographic order used for the strictly ordered derivative multi-indices in the paper's partition data.

Equations

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

structure AVenhance.FaaDiBruno.PaperPartitionData (d s : ℕ) (β α : PaperMultiIndex d) : Type

The finite multi-index and multiplicity data called p_s(β, α) in Appendix B.1. The ell entries are distinct and strictly increasing in graded lexicographic order.

• k : Fin s → PaperMultiIndex d

  Multi-index multiplicities in a Faà di Bruno partition.

• ell : Fin s → PaperMultiIndex d

  Distinct derivative multi-indices ordered by graded lexicographic order.

• k_nonzero (j : Fin s) : 0 < paperMultiIndexSize (self.k j)
• ell_nonzero (j : Fin s) : 0 < paperMultiIndexSize (self.ell j)
• ell_strictlyOrdered (i j : Fin s) : i < j → paperMultiIndexLT (self.ell i) (self.ell j)
• k_sum (i : Fin d) : ∑ j : Fin s, self.k j i = α i
• beta_sum (i : Fin d) : ∑ j : Fin s, paperMultiIndexSize (self.k j) * self.ell j i = β i

theorem AVenhance.FaaDiBruno.PaperPartitionData.ext {d s : ℕ} {β α : PaperMultiIndex d} {x y : PaperPartitionData d s β α} (k : x.k = y.k) (ell : x.ell = y.ell) : x = y

theorem AVenhance.FaaDiBruno.PaperPartitionData.ext_iff {d s : ℕ} {β α : PaperMultiIndex d} {x y : PaperPartitionData d s β α} : x = y ↔ x.k = y.k ∧ x.ell = y.ell

def AVenhance.FaaDiBruno.paperPartitions {d s : ℕ} (β α : PaperMultiIndex d) : Type

The paper's p_s(β, α), with the dimension generalized according to the correction.

Equations

• AVenhance.FaaDiBruno.paperPartitions β α = AVenhance.FaaDiBruno.PaperPartitionData d s β α

theorem AVenhance.FaaDiBruno.PaperPartitionData.k_le_alpha {d s : ℕ} {β α : PaperMultiIndex d} (P : paperPartitions β α) (j : Fin s) (i : Fin d) : P.k j i ≤ α i

theorem AVenhance.FaaDiBruno.PaperPartitionData.ell_le_beta {d s : ℕ} {β α : PaperMultiIndex d} (P : paperPartitions β α) (j : Fin s) (i : Fin d) : P.ell j i ≤ β i

theorem AVenhance.FaaDiBruno.PaperPartitionData.finite {d s : ℕ} {β α : PaperMultiIndex d} : Finite (paperPartitions β α)

instance AVenhance.FaaDiBruno.PaperPartitionData.instFinite {d s : ℕ} {β α : PaperMultiIndex d} : Finite (paperPartitions β α)

@[instance_reducible]

noncomputable instance AVenhance.FaaDiBruno.PaperPartitionData.instFintype {d s : ℕ} {β α : PaperMultiIndex d} : Fintype (paperPartitions β α)

Equations

• AVenhance.FaaDiBruno.PaperPartitionData.instFintype = Fintype.ofFinite (AVenhance.FaaDiBruno.paperPartitions β α)