Prove2Me

Normalized bump convolutions on C\mathbb{C} converge in LpL^p, 1≤p<∞1\le p<\infty

Proved
JHolomorphic.tendsto_eLpNorm_normed_convolution_sub

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

convolutionlebesgue-spaces

Let EE be a real Banach space, 1≤p<∞1\le p<\infty, and f∈Lp(C;E)f\in L^p(\mathbb{C};E). Let (φn)(\varphi_n) be a sequence of smooth bump functions centred at 00 whose outer radii tend to 00, and write φ~n\tilde\varphi_n for the normalization of φn\varphi_n (integral 11). Then

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

This is the standard LpL^p approximation by mollification on the plane, for vector-valued maps.

Formalization Note The bumps are φ : ℕ → ContDiffBump (0 : ℂ) with Tendsto (fun n => (φ n).rOut) atTop (𝓝 0); the convolution is (φ n).normed volume ⋆[lsmul ℝ ℝ, volume] f, the hypothesis is MemLp f p volume with 1 ≤ p and p ≠ ⊤, and the norm is eLpNorm _ p volume, so the statement is a limit in ℝ≥0∞.

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 `1 ≤ p < ∞`, `f ∈ L^p(ℂ; E)` and normalized bumps `φ n` whose outer radii tend to `0`,
the convolutions `φ n ⋆ f` converge to `f` in `L^p(ℂ)`. -/
theorem tendsto_eLpNorm_normed_convolution_sub {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [CompleteSpace E] {p : ℝ≥0∞} (hp : 1 ≤ p) (hpt : p ≠ ⊤)
    (φ : ℕ → ContDiffBump (0 : ℂ)) (hφ : Tendsto (fun n => (φ n).rOut) atTop (𝓝 0))
    {f : ℂ → E} (hf : MemLp f p volume) :
    Tendsto (fun n => eLpNorm ((φ n).normed volume ⋆[lsmul ℝ ℝ, volume] f - f) p volume)
      atTop (𝓝 0) := by
  sorry

end JHolomorphic
Source
Standard; cf. L. C. Evans, Partial Differential Equations, Appendix C.5, Theorem 7; H. Brezis, Functional Analysis, Sobolev Spaces and PDE, Theorem 4.22

View graph