mollified
plain-language theorem explainer
Mollified constructs the convolution of a real function G with a normalized ContDiffBump kernel φ on the line. Analysts working on continuous d'Alembert equations cite the construction to produce regularized approximants that support smoothness bootstraps. The definition is a direct left convolution of the normed bump with G under the lsmul map and Lebesgue measure.
Claim. Let $G : ℝ → ℝ$ and let $φ$ be a normalized $C^∞$ bump function with compact support. The mollified function is the left convolution $φ^{normed} ⋆ G$, taken with respect to Lebesgue measure on $ℝ$ via the scalar multiplication map.
background
The GeneralizedDAlembert module replaces the polynomial-degree-≤2 restriction on the route-independence combiner with mere continuity. It invokes the Aczél–Kannappan classification: a continuous $H : ℝ → ℝ$ satisfying $H(x+y) + H(x-y) = 2H(x)H(y)$ with $H(0)=1$ must be the constant 1, a hyperbolic cosine, or a trigonometric cosine. Mollification supplies the smoothing step that turns a continuous combiner into a smooth one while preserving the equation in the limit.
proof idea
The definition is a one-line wrapper that applies the convolution operator from Mathlib.Analysis.Convolution to the normed bump φ and the input G, using ContinuousLinearMap.lsmul and the volume measure.
why it matters
Mollified supports mollified_continuous and mollified_pointwise_tendsto, which feed log_aczel_data_of_laws. That theorem extracts LogAczelData from any continuous SatisfiesLawsOfLogicContinuous instance, allowing the smoothness bootstrap to proceed from continuity alone. It relaxes the polynomial hypothesis of the Translation Theorem to continuity, aligning with the Aczél–Kannappan classification inside the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.