contDiff_top_of_contDiff_nat
plain-language theorem explainer
A real-valued function on the line that meets the ContDiff condition at every finite order is automatically infinitely differentiable. The result is invoked inside the continuous-combiner construction to lift finite-order certificates to the top-level smoothness statement required downstream. The proof is a direct one-line application of Mathlib's contDiff_infty equivalence.
Claim. If $f : ℝ → ℝ$ satisfies ContDiff $ℝ$ $n$ $f$ for every natural number $n$, then ContDiff $ℝ$ $⊤$ $f$, where $⊤$ is the top element of the extended naturals.
background
The module supplies a finite-to-top smoothness helper for the continuous-combiner route inside the generalized d'Alembert construction. Mathlib encodes $C^∞$ smoothness as ContDiff $𝕜$ $⊤$ $f$ and records via contDiff_infty that this is equivalent to the conjunction of all finite-order conditions. The file isolates the promotion step so the main module need not treat it as an axiom.
proof idea
The proof is a one-line wrapper that applies the second projection of contDiff_infty directly to the finite-order hypothesis.
why it matters
The declaration supplies the promotion step required by residual input 1b in continuous_combiner_finite_smoothness_to_top. That parent theorem consumes the resulting top-level smoothness to finish the log-cost argument for the continuous combiner. It therefore closes the finite-to-infinite gap between mollifier certificates and the infinite differentiability needed by the generalized d'Alembert route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.