LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Rooted-tree series and the inverse of u exp(-u)

Statement

Let $T (z) = \sum_{k \geq 1} k^{k - 1} z^{k} / k!$ and $U (z) = T (z) - T (z)^{2} / 2$ . These series converge absolutely for $∣ z ∣ < e^{- 1}$ . On that disk they satisfy $T = z e^{T}$ , $z T^{'} = T / (1 - T)$ , and $z U^{'} = T$ . Consequently $U (z) = \sum_{k \geq 1} k^{k - 2} z^{k} / k!$ . For real $0 \leq z < e^{- 1}$ , $T (z)$ is the unique $u \in [0, 1)$ satisfying $u e^{- u} = z$ .

Facts & Assumptions

Given: Formal series are multiplied by coefficient convolution, and the Lagrange–Bürmann formula applies to the unique formal solution of $w = z ϕ (w)$ over a field containing $Q$ .

[F1]

Lagrange–Bürmann inversion extracts coefficients of a compositional inverse and of functions of it: if $w = z ϕ (w)$ and $ϕ (0) \neq 0$ , then $[z^{n}] H (w) = \frac{1}{n} [u^{n - 1}] H^{'} (u) ϕ (u)^{n}$ for every $n \geq 1$ .

[F2]

Formal differentiation is linear and satisfies product, power, quotient, chain, and coefficient-recovery laws: formal differentiation obeys the product rule and the chain rule for admissible compositions with summable differentiated families; composition with a series of zero constant coefficient is locally finite.

[F3]

A formal power series is a unit exactly when its constant coefficient is a unit: a formal power series with nonzero constant coefficient over a field is invertible.

[F4]

For every real $x$ , $(1 + x / n)^{n} \to \exp x$ : $(1 + 1 / n)^{n} \to e$ .

[F5]

Convergent power series differentiate term by term inside their radius: for real coefficients and real arguments, if a power series and its formal derivative series converge absolutely at every smaller radius, the sum differentiates termwise inside the radius.

Proof

1.1givenF1algebra

Apply [F1] with $ϕ (u) = e^{u}$ and $H (u) = u$ . It gives $[z^{k}] T = \frac{1}{k} [u^{k - 1}] e^{k u} = k^{k - 1} / k!$ , and the defining equation for the compositional inverse gives $T = z e^{T}$ as a formal identity.

2.1step 1.1F2F3algebra

Differentiate $T = z e^{T}$ formally using [F2]. Since $T (0) = 0$ , the series $1 - T$ is a unit by [F3], and rearrangement yields $z T^{'} = T / (1 - T)$ . Therefore $z U^{'} = z T^{'} (1 - T) = T$ , so $[z^{k}] U = [z^{k}] T / k = k^{k - 2} / k!$ .

3.1F4F5step 2.1algebra

For $a_{k} = k^{k - 1} / k!$ , the ratio is $a_{k + 1} / a_{k} = (1 + 1 / k)^{k - 1} \to e$ by [F4]. The coefficients of $U$ are $a_{k} / k$ , so their ratios have the same limit; the derivative-series ratios are $(1 + 1 / k)^{k} \to e$ and $(1 + 1 / k)^{k - 1} \to e$ , respectively. For every $0 < r < e^{- 1}$ , all four series are therefore bounded in their tails on $∣ z ∣ \leq r$ by convergent geometric series. In particular, [F5] gives termwise differentiation for real arguments.

4.1step 1.1step 2.1step 3.1algebra

For either coefficient sequence $(c_{k}) = (a_{k})$ or $(a_{k} / k)$ , fix complex $z$ and real $R$ with $∣ z ∣ < R < e^{- 1}$ . For complex $0 < ∣ h ∣ < R - ∣ z ∣$ , the identity $((z + h)^{k} - z^{k}) / h = \sum_{j = 0}^{k - 1} (z + h)^{k - 1 - j} z^{j}$ bounds the difference-quotient tail after degree $m$ by $\sum_{k > m} k ∣ c_{k} ∣ R^{k - 1}$ , uniformly in $h$ . The derivative-series tail has the same bound, tending to zero by step 3.1. The finite polynomial head differentiates for complex increments, so taking its limit and then letting $m \to \infty$ proves complex termwise differentiation. Products may be regrouped absolutely, and the expansion of $e^{T (z)}$ is absolutely dominated by $\exp (\sum_{k \geq 1} a_{k} ∣ z ∣^{k})$ . Thus the formal identities in steps 1.1 and 2.1 give $T = z e^{T}$ , $(1 - T) z T^{'} = T$ , and $z U^{'} = T$ for the sums. The middle identity rules out $T (z) = 1$ , and hence gives $z T^{'} = T / (1 - T)$ .

5.1step 3.1step 4.1algebra∎

For real $0 \leq z < e^{- 1}$ , the coefficients of $T$ are nonnegative, so $T (z) \geq 0$ . If $T (z) \geq 1$ , continuity and $T (0) = 0$ give $z_{0} \leq z$ with $T (z_{0}) = 1$ , but step 4.1 implies $z_{0} = T (z_{0}) e^{- T (z_{0})} = e^{- 1}$ , a contradiction. Thus $T (z) < 1$ . Since $u \mapsto u e^{- u}$ is strictly increasing on $[0, 1)$ , step 4.1 identifies $T (z)$ with its unique inverse-branch value.

Depends on

Used by

The discrete product-kernel solution has finite-time second-moment blow-up Theorem

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Philippe Laurençot, Weak compactness techniques and coagulation equations, §§1 and 3.3 (standard reference, not scraped)