mollified_pointwise_tendsto
plain-language theorem explainer
The result shows that mollification of a continuous real function G by a net of ContDiffBump kernels whose outer radii tend to zero along a filter converges pointwise to G at every point. Analysts working on regularization steps inside continuous solutions of the d'Alembert equation would cite the statement when passing from continuous to smooth approximants. The argument is a one-line wrapper that unfolds the mollified definition and invokes the standard Mathlib convolution convergence lemma.
Claim. Let $G:ℝ→ℝ$ be continuous. Let $φ:ι→C^∞_c(ℝ)$ be a family of normalized bump functions whose outer radii tend to zero along the filter $l$. Then the mollified approximations satisfy $(G⋆φ_i)(x_0)→G(x_0)$ as $i→l$.
background
The GeneralizedDAlembert module replaces the polynomial-degree restriction on the route-independence combiner with mere continuity, relying on the Aczél–Kannappan trichotomy for continuous solutions of the d'Alembert equation. The mollified operation is the left convolution of G with the normalized ContDiffBump kernel; the upstream definition records that the normalized bump has compact support and that convolution with a continuous function remains continuous. The local theoretical setting is Move 3 of the module: discharge the polynomial regularity hypothesis so that the continuous-combiner version of SatisfiesLawsOfLogic becomes available downstream.
proof idea
The proof is a one-line wrapper. It unfolds the definition of mollified to expose the convolution and then applies the Mathlib lemma ContDiffBump.convolution_tendsto_right_of_continuous to the given filter condition on the outer radii together with the continuity hypothesis on G.
why it matters
This lemma supplies the pointwise convergence step required to pass from continuous log-cost Aczel data to smooth approximants in the smoothness bootstrap. It is invoked by the downstream theorem log_aczel_data_of_laws, which turns the continuous-combiner Law of Logic into a continuous log-coordinate Aczel equation. Within the Recognition framework it closes the gap between the polynomial Translation Theorem and the weaker continuous-combiner version, letting the Aczél–Kannappan classification discharge the degree bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.