A normalized mollification of a function bounded by $M$ is bounded by $3M$

Proved

JHolomorphic.norm_normed_convolution_le

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

convolutionmollifiersweak-derivatives

Let $g:\mathbb{C}\to\mathbb{R}$ be continuous with $|g|\le M$ everywhere, let $\rho$ be a bump function centred at $0$ and let $\rho_{\mathrm{n}}=\rho/\int\rho$ . Then $|(\rho_{\mathrm{n}}*g)(z)|\le 3M$ for every $z\in\mathbb{C}$ .

Formalization Note For a bump function $\rho$ centred at $0$ (ContDiffBump (0 : ℂ)), $\rho_{\mathrm{n}}$ is ρ.normed volume, the multiple of $\rho$ with integral $1$ ; $\rho_{\mathrm{n}}*g$ is the convolution ρ.normed volume ⋆[lsmul ℝ ℝ, volume] g with respect to Lebesgue measure on $\mathbb{C}$ .

Preamble

import Definitions.Def_JHolomorphic_Setting
import Mathlib.Analysis.Calculus.ContDiff.Convolution
import Mathlib.Analysis.Calculus.BumpFunction.Convolution
import Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension

Formal statement

namespace JHolomorphic

open MeasureTheory Filter Topology Metric ContinuousLinearMap
open scoped ContDiff Convolution

/-- A mollification of a bounded continuous function is bounded by three times the bound. -/
theorem norm_normed_convolution_le (ρ : ContDiffBump (0 : ℂ)) {g : ℂ → ℝ} (hg : Continuous g)
    {M : ℝ} (hM : ∀ x, ‖g x‖ ≤ M) (z : ℂ) :
    ‖(ρ.normed volume ⋆[lsmul ℝ ℝ, volume] g) z‖ ≤ 3 * M := by
  sorry

end JHolomorphic

Source

Standard (mollification).

View graph

A normalized mollification of a function bounded by MMM is bounded by 3M3M3M

A normalized mollification of a function bounded by $M$ is bounded by $3M$