Proof of `Factorial estimates for iterated analytic vector fields` (2nd statement)

groundedproofs/Lax825748Proofs/WordMajorant.lean · lax-825748

What this proof establishes

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Use the nonnegative series FI=C∣I∣F_I=C^{|I|} as a coefficient majorant. Its derivatives satisfy ∂iF⪯CF2\partial_i F\preceq C F^2. After pp vector fields the majorant is α(2dαC)pp!F2p+1\alpha(2d\alpha C)^p p! F^{2p+1}; its constant coefficient is the claimed bound.