A factorial-square bound for the partitions in Faà di Bruno's formula

The estimate is uniform in the order. Extending a partition either creates a singleton or increases one old part, so the factorial-square weight grows by at most (n + 1)^2 * (x + 2). This avoids replacing every derivative in the composition formula by the largest derivative bound.

theorem EulerGevreyComposition.sum_partSize {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, c.partSize i = n

theorem EulerGevreyComposition.sum_partSize_real {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, ↑(c.partSize i) = ↑n

theorem EulerGevreyComposition.sum_partSize_succ_sq_le {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, (↑(c.partSize i) + 1) ^ 2 ≤ 2 * (↑n + 1) ^ 2

def EulerGevreyComposition.factorialProduct {n : ℕ} (c : OrderedFinpartition n) : ℝ

Factorial product, given by ∏ i, ((c.partSize i).factorial : ℝ).

Equations

• EulerGevreyComposition.factorialProduct c = ∏ i : Fin c.length, ↑(c.partSize i).factorial

def EulerGevreyComposition.partitionWeight {n : ℕ} (x : ℝ) (c : OrderedFinpartition n) : ℝ

Partition weight, given by x^c.length * ((c.length.factorial : ℝ) * factorialProduct c)^2.

Equations

• EulerGevreyComposition.partitionWeight x c = x ^ c.length * (↑c.length.factorial * EulerGevreyComposition.factorialProduct c) ^ 2

noncomputable def EulerGevreyComposition.partitionSum (n : ℕ) (x : ℝ) : ℝ

Partition sum, given by ∑ c : OrderedFinpartition n, partitionWeight x c.

Equations

• EulerGevreyComposition.partitionSum n x = ∑ c : OrderedFinpartition n, EulerGevreyComposition.partitionWeight x c

theorem EulerGevreyComposition.partitionWeight_nonneg {n : ℕ} (x : ℝ) (hx : 0 ≤ x) (c : OrderedFinpartition n) : 0 ≤ partitionWeight x c

theorem EulerGevreyComposition.factorialProduct_extendLeft {n : ℕ} (c : OrderedFinpartition n) : factorialProduct c.extendLeft = factorialProduct c

theorem EulerGevreyComposition.factorialProduct_extendMiddle {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : factorialProduct (c.extendMiddle i) = (↑(c.partSize i) + 1) * factorialProduct c

theorem EulerGevreyComposition.partitionWeight_extendLeft {n : ℕ} (x : ℝ) (c : OrderedFinpartition n) : partitionWeight x c.extendLeft = x * (↑c.length + 1) ^ 2 * partitionWeight x c

theorem EulerGevreyComposition.partitionWeight_extendMiddle {n : ℕ} (x : ℝ) (c : OrderedFinpartition n) (i : Fin c.length) : partitionWeight x (c.extendMiddle i) = (↑(c.partSize i) + 1) ^ 2 * partitionWeight x c

theorem EulerGevreyComposition.partitionSum_succ (n : ℕ) (x : ℝ) : partitionSum (n + 1) x = ∑ c : OrderedFinpartition n, (x * (↑c.length + 1) ^ 2 + ∑ i : Fin c.length, (↑(c.partSize i) + 1) ^ 2) * partitionWeight x c

theorem EulerGevreyComposition.partitionSum_succ_le (n : ℕ) (x : ℝ) (hx : 0 ≤ x) : partitionSum (n + 1) x ≤ (↑n + 1) ^ 2 * (x + 2) * partitionSum n x

theorem EulerGevreyComposition.partitionSum_le (n : ℕ) (x : ℝ) (hx : 0 ≤ x) : partitionSum n x ≤ (x + 2) ^ n * ↑n.factorial ^ 2

The entire factorial-square Faà di Bruno partition sum has one fixed exponential radius, independent of the differentiation order.