Prove2Me

Normalized bump convolutions of a continuous compactly supported map on C\mathbb{C} converge in LpL^p

Proved
JHolomorphic.tendsto_eLpNorm_normed_convolution_sub_of_continuous

by Mazecto · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

convolutionlebesgue-spaces

Let EE be a real Banach space, let g:C→Eg:\mathbb{C}\to E be continuous with compact support, and let (φn)(\varphi_n) be a sequence of smooth bump functions centred at 00 whose outer radii tend to 00. Writing φ~n\tilde\varphi_n for the normalization of φn\varphi_n (integral 11), we have for every exponent p∈[0,∞]p\in[0,\infty]

∥φ~n⋆g−g∥Lp(C)⟶0(n→∞).\|\tilde\varphi_n\star g-g\|_{L^p(\mathbb{C})}\longrightarrow 0\qquad(n\to\infty).

This is the basic approximation statement for continuous compactly supported maps, used to pass from them to general LpL^p maps.

Formalization Note The bumps are φ : ℕ → ContDiffBump (0 : ℂ) with Tendsto (fun n => (φ n).rOut) atTop (𝓝 0); the convolution is (φ n).normed volume ⋆[lsmul ℝ ℝ, volume] g and the norm is eLpNorm _ p volume, an extended nonnegative real, so the statement is a limit in ℝ≥0∞. No restriction on p is needed.

Preamble
import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Calculus.BumpFunction.Convolution
import Mathlib.Analysis.Calculus.BumpFunction.InnerProduct
Formal statement
namespace JHolomorphic

open MeasureTheory Filter Topology ContinuousLinearMap
open scoped Convolution ENNReal

/-- For a continuous compactly supported `g : ℂ → E` and normalized bumps `φ n` whose outer radii
tend to `0`, the convolutions `φ n ⋆ g` converge to `g` in `L^p(ℂ)`, for every exponent `p`. -/
theorem tendsto_eLpNorm_normed_convolution_sub_of_continuous {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] {p : ℝ≥0∞} (φ : ℕ → ContDiffBump (0 : ℂ))
    (hφ : Tendsto (fun n => (φ n).rOut) atTop (𝓝 0)) {g : ℂ → E} (hg : Continuous g)
    (hgc : HasCompactSupport g) :
    Tendsto (fun n => eLpNorm ((φ n).normed volume ⋆[lsmul ℝ ℝ, volume] g - g) p volume)
      atTop (𝓝 0) := by
  sorry

end JHolomorphic
Source
Standard; cf. L. C. Evans, Partial Differential Equations, Appendix C.5, Theorem 7

View graph