Ordered-finpartition resummations

The factorial weights in the composition estimate have a closed form when summed over Mathlib's ordered finpartitions. This is the coefficient-level form of the 10469 resummation needed by Proposition 10528.

def AVenhance.FaaDiBruno.orderedPartitionFactorialProduct {n : ℕ} (c : OrderedFinpartition n) : ℕ

Product of the factorials of the part sizes of an ordered finpartition.

Equations

• AVenhance.FaaDiBruno.orderedPartitionFactorialProduct c = ∏ i : Fin c.length, (c.partSize i).factorial

noncomputable def AVenhance.FaaDiBruno.orderedPartitionWeightPolynomial (n : ℕ) : Polynomial ℝ

The weighted ordered-finpartition polynomial. The weight of a partition with s parts of sizes r₁,…,rₛ is X^s s! ∏ rᵢ!.

Equations

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

theorem AVenhance.FaaDiBruno.Resummation.orderedPartition_partSize_sum {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, c.partSize i = n

theorem AVenhance.FaaDiBruno.Resummation.orderedPartition_partSize_add_one_sum {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, (c.partSize i + 1) = n + c.length

theorem AVenhance.FaaDiBruno.Resummation.factorialProduct_extendLeft {n : ℕ} (c : OrderedFinpartition n) : orderedPartitionFactorialProduct c.extendLeft = orderedPartitionFactorialProduct c

theorem AVenhance.FaaDiBruno.Resummation.factorialProduct_extendMiddle {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : orderedPartitionFactorialProduct (c.extendMiddle i) = (c.partSize i + 1) * orderedPartitionFactorialProduct c

theorem AVenhance.FaaDiBruno.Resummation.x_mul_derivative_x_pow_C (s : ℕ) (a : ℝ) : Polynomial.X * Polynomial.derivative (Polynomial.X ^ s * Polynomial.C a) = Polynomial.X ^ s * Polynomial.C (↑s * a)

theorem AVenhance.FaaDiBruno.Resummation.x_derivative_orderedPartitionWeightPolynomial (n : ℕ) : Polynomial.X * Polynomial.derivative (orderedPartitionWeightPolynomial n) = ∑ c : OrderedFinpartition n, Polynomial.X ^ c.length * Polynomial.C (↑c.length * ↑(c.length.factorial * orderedPartitionFactorialProduct c))

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionSomeWeightSum {n : ℕ} (c : OrderedFinpartition n) : ∑ i : Fin c.length, Polynomial.X ^ c.length * Polynomial.C ↑(c.length.factorial * (c.partSize i + 1) * orderedPartitionFactorialProduct c) = Polynomial.X ^ c.length * Polynomial.C ↑(c.length.factorial * (n + c.length) * orderedPartitionFactorialProduct c)

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionWeightPolynomial_succ_expansion (n : ℕ) : orderedPartitionWeightPolynomial (n + 1) = ∑ c : OrderedFinpartition n, (Polynomial.X ^ (c.length + 1) * Polynomial.C ↑((c.length + 1).factorial * orderedPartitionFactorialProduct c) + ∑ i : Fin c.length, Polynomial.X ^ c.length * Polynomial.C ↑(c.length.factorial * (c.partSize i + 1) * orderedPartitionFactorialProduct c))

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionWeightPolynomial_succ (n : ℕ) : orderedPartitionWeightPolynomial (n + 1) = (Polynomial.C ↑n + Polynomial.X) * orderedPartitionWeightPolynomial n + (Polynomial.X + 1) * (Polynomial.X * Polynomial.derivative (orderedPartitionWeightPolynomial n))

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionWeightPolynomial_zero : orderedPartitionWeightPolynomial 0 = 1

theorem AVenhance.FaaDiBruno.Resummation.derivative_weight_shape (n : ℕ) : Polynomial.derivative (Polynomial.C ↑(n + 1).factorial * Polynomial.X * (1 + Polynomial.X) ^ n) = Polynomial.C ↑(n + 1).factorial * ((1 + Polynomial.X) ^ n + Polynomial.X * Polynomial.C ↑n * (1 + Polynomial.X) ^ (n - 1))

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionWeightPolynomial_closed_succ (n : ℕ) : orderedPartitionWeightPolynomial (n + 1) = Polynomial.C ↑(n + 1).factorial * Polynomial.X * (1 + Polynomial.X) ^ n

theorem AVenhance.FaaDiBruno.orderedFinpartitionFactorialResummation10469 {n : ℕ} (hn : 0 < n) (R : ℝ) : ∑ c : OrderedFinpartition n, R ^ c.length * ↑c.length.factorial * ↑(orderedPartitionFactorialProduct c) = ↑n.factorial * R * (1 + R) ^ (n - 1)

The factorial-weighted ordered-finpartition form of the 10469 resummation. This is the all-order coefficient sum used in Composition estimate 10528; substituting R := d * C_g * R_h gives the paper's d R (1 + d R)^(n-1) n! factor.

noncomputable def AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockWeight (r : ℕ) : ℝ

One block's signed-binomial factorial weight in the 10421 resummation.

Equations

• AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockWeight r = ↑r.factorial * Ring.choose (1 / 2) r

noncomputable def AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockProduct {n : ℕ} (c : OrderedFinpartition n) : ℝ

Product of the 10421 block weights over an ordered finpartition.

Equations

• AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockProduct c = ∏ i : Fin c.length, AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockWeight (c.partSize i)

noncomputable def AVenhance.FaaDiBruno.orderedPartitionHalfBinomialWeight {n : ℕ} (c : OrderedFinpartition n) : ℝ

The signed 10421 weight of one ordered finpartition.

Equations

• AVenhance.FaaDiBruno.orderedPartitionHalfBinomialWeight c = (-1) ^ c.length * ↑c.length.factorial * AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockProduct c

noncomputable def AVenhance.FaaDiBruno.orderedPartitionHalfBinomialSum (n : ℕ) : ℝ

The sum of the signed 10421 weights over ordered finpartitions.

Equations

• AVenhance.FaaDiBruno.orderedPartitionHalfBinomialSum n = ∑ c : OrderedFinpartition n, AVenhance.FaaDiBruno.orderedPartitionHalfBinomialWeight c

theorem AVenhance.FaaDiBruno.orderedPartitionHalfBinomialBlockWeight_succ (r : ℕ) : orderedPartitionHalfBinomialBlockWeight (r + 1) = (1 / 2 - ↑r) * orderedPartitionHalfBinomialBlockWeight r

The signed half-binomial factorial weights obey their first-order recurrence. This is the coefficient identity used in the flow Dn induction.

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionHalfBinomialBlockProduct_extendLeft {n : ℕ} (c : OrderedFinpartition n) : orderedPartitionHalfBinomialBlockProduct c.extendLeft = 1 / 2 * orderedPartitionHalfBinomialBlockProduct c

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionHalfBinomialBlockProduct_extendMiddle {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : orderedPartitionHalfBinomialBlockProduct (c.extendMiddle i) = (1 / 2 - ↑(c.partSize i)) * orderedPartitionHalfBinomialBlockProduct c

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionHalfBinomialWeight_extendLeft {n : ℕ} (c : OrderedFinpartition n) : orderedPartitionHalfBinomialWeight c.extendLeft = -(↑(c.length + 1) / 2) * orderedPartitionHalfBinomialWeight c

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionHalfBinomialWeight_extendMiddle {n : ℕ} (c : OrderedFinpartition n) (i : Fin c.length) : orderedPartitionHalfBinomialWeight (c.extendMiddle i) = (1 / 2 - ↑(c.partSize i)) * orderedPartitionHalfBinomialWeight c

theorem AVenhance.FaaDiBruno.Resummation.orderedPartitionHalfBinomialSum_succ (n : ℕ) : orderedPartitionHalfBinomialSum (n + 1) = -(↑n + 1 / 2) * orderedPartitionHalfBinomialSum n

theorem AVenhance.FaaDiBruno.orderedFinpartitionResummation10421 (n : ℕ) : orderedPartitionHalfBinomialSum n = 2 * ↑(n + 1).factorial * Ring.choose (1 / 2) (n + 1)

The all-order 10421 signed-binomial resummation in ordered-finpartition form.