phi_contDiff_succ
plain-language theorem explainer
The result shows that the integral operator applied to a continuous C^n function yields a C^{n+1} function. Analysts proving regularity theorems for functional equations would cite it in inductive bootstraps. The proof reduces the smoothness claim to the known derivative formula via the standard characterization of higher differentiability classes.
Claim. If $H:ℝ→ℝ$ is continuous and belongs to the class $C^n$, then the antiderivative $Φ(H)$ defined by $Φ(H)(t)=∫_0^t H(s) ds$ belongs to the class $C^{n+1}$.
background
The module proves Aczél's smoothness theorem: continuous solutions H to the d'Alembert equation H(t+u)+H(t-u)=2 H(t) H(u) with H(0)=1 are real analytic. Phi is the antiderivative operator Phi(H)(t)=∫_0^t H(s) ds. The shifted cost H equals J plus one and satisfies the d'Alembert equation under the Recognition Composition Law. The lemma depends on the prior results that Phi is differentiable with derivative exactly H.
proof idea
The tactic proof first casts the target order via suffices, then rewrites via contDiff_succ_iff_deriv. It supplies differentiability of the integral from the dedicated lemma, discards the infinite-order case by contradiction, and substitutes the derivative identity.
why it matters
The lemma supplies the inductive step inside dAlembert_contDiff_nat, which establishes C^n regularity for every n from mere continuity. That theorem completes the bootstrap toward analyticity in the cost algebra, where H arises directly from the J-cost via the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.