mollified_continuous
Mollification of a continuous real function G by a normalized ContDiffBump kernel φ produces a continuous output. Researchers relaxing polynomial-degree hypotheses to continuity in the d'Alembert functional equation would cite this result. The proof is a term-mode wrapper that unfolds the convolution definition and applies the general continuity theorem for left convolution against a compactly supported continuous kernel.
claimLet $G : ℝ → ℝ$ be continuous and let $φ$ be a normalized $C^∞$ bump function centered at the origin with compact support. Then the mollification of $G$ by $φ$, given by the convolution $φ ⋆ G$, is continuous.
background
The module GeneralizedDAlembert discharges the polynomial-degree-≤-2 restriction on the route-independence combiner P by invoking the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation. A continuous $H : ℝ → ℝ$ with $H(0)=1$ satisfying $H(x+y)+H(x-y)=2H(x)H(y)$ must be the constant 1, a hyperbolic cosine, or a trigonometric cosine. The mollified definition is the left convolution of G against the normalized bump: $φ.normed ⋆ G$ using the lsmul map and Lebesgue measure. Upstream results supply the bump-function properties (compact support, ContDiff at level 0) and the local-integrability fact for continuous functions.
proof idea
The term proof unfolds mollified to expose the convolution, then applies HasCompactSupport.continuous_convolution_left. It supplies three arguments: the compact support of the normed bump, the fact that ContDiff at level 0 implies continuity of the normed kernel, and the local integrability of the continuous input G.
why it matters in Recognition Science
The result supplies the continuity preservation step needed for the continuous-combiner version of SatisfiesLawsOfLogic, which in turn lets the Aczél–Kannappan trichotomy replace the stricter polynomial hypothesis in the Translation Theorem. It completes Move 3 of the module by showing that mere continuity of the combiner is sufficient for the classification into constant, cosh, or cos solutions. The declaration sits inside the Recognition Science pipeline that derives the d'Alembert equation from the Recognition Composition Law and then classifies its continuous solutions.
scope and limits
- Does not establish differentiability or higher regularity of the mollified output.
- Does not apply when G fails to be continuous or locally integrable.
- Does not prove that the mollified function itself satisfies the d'Alembert equation.
- Does not address convergence rates as the bump support shrinks.
formal statement (Lean)
218theorem mollified_continuous (G : ℝ → ℝ) (hG : Continuous G)
219 (φ : ContDiffBump (0 : ℝ)) : Continuous (mollified G φ) := by
proof body
Term-mode proof.
220 unfold mollified
221 refine HasCompactSupport.continuous_convolution_left
222 (L := ContinuousLinearMap.lsmul ℝ ℝ) ?_ ?_ ?_
223 · exact φ.hasCompactSupport_normed (μ := (volume : MeasureTheory.Measure ℝ))
224 · have h0 : ContDiff ℝ ((0 : ℕ∞) : WithTop ℕ∞)
225 (φ.normed (μ := (volume : MeasureTheory.Measure ℝ))) :=
226 φ.contDiff_normed (μ := (volume : MeasureTheory.Measure ℝ)) (n := 0)
227 -- ContDiff at level 0 is continuity.
228 exact (contDiff_zero.mp (by exact_mod_cast h0))
229 · exact hG.locallyIntegrable (μ := (volume : MeasureTheory.Measure ℝ))
230
231/-- As the bump support shrinks, the mollification converges pointwise to
232the original continuous function. -/