mollified_continuous

formal source

 215
 216/-- The normalized bump has compact support and is continuous; convolving
 217with a continuous function leaves a continuous function. -/
 218theorem mollified_continuous (G : ℝ → ℝ) (hG : Continuous G)
 219    (φ : ContDiffBump (0 : ℝ)) : Continuous (mollified G φ) := by
 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. -/
 233theorem mollified_pointwise_tendsto {ι : Type*}
 234    (G : ℝ → ℝ) (hG : Continuous G)
 235    {φ : ι → ContDiffBump (0 : ℝ)} {l : Filter ι}
 236    (hφ : Filter.Tendsto (fun i => (φ i).rOut) l (nhds 0)) (x₀ : ℝ) :
 237    Filter.Tendsto (fun i => mollified G (φ i) x₀) l (nhds (G x₀)) := by
 238  unfold mollified
 239  exact ContDiffBump.convolution_tendsto_right_of_continuous hφ hG x₀
 240
 241/-- Helper predicate naming the residual analytic content for Piece 1.
 242
 243`MollifierCkRoute` says: there is a parametrized family of `ContDiffBump`
 244kernels with shrinking support. This is *infrastructure only* — the
 245analytic blocker is uniform compact-set derivative bounds on
 246`mollified G (φ n)`, not the existence of the bump family. -/
 247def MollifierCkRoute : Prop :=
 248  ∃ (φ : ℕ → ContDiffBump (0 : ℝ)),