`BookProof.WeylCauchyRiemann.tendsto_mollify_bump_of_continuous` {h : ℂ → ℂ} (hh : Continuous h) (z : ℂ) : Tendsto (fun n => mollify h ((bumpSeq n).normed volume) z) atTop (nhds (h

Proved

BookProof.WeylCauchyRiemann.tendsto_mollify_bump_of_continuous

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterWeylCauchyRiemann.

BookProof.WeylCauchyRiemann.tendsto_mollify_bump_of_continuous {h : ℂ → ℂ} (hh : Continuous h) (z : ℂ) : Tendsto (fun n => mollify h ((bumpSeq n).normed volume) z) atTop (nhds (h z))

Formalization note: Lean 4 identifier BookProof.WeylCauchyRiemann.tendsto_mollify_bump_of_continuous.

Preamble

-- Generated from ChapterWeylCauchyRiemann.lean — theorem BookProof.WeylCauchyRiemann.tendsto_mollify_bump_of_continuous
import Definitions.Def_ChapterRadialMollifier
import Mathlib
import Definitions.Def_ChapterWeylCauchyRiemann
open BookProof.WeylCauchyRiemann



open MeasureTheory Metric Set Filter Complex BookProof.RadialMollifier
open scoped Convolution Topology ContDiff

noncomputable section

Formal statement

theorem BookProof.WeylCauchyRiemann.tendsto_mollify_bump_of_continuous {h : ℂ → ℂ} (hh : Continuous h) (z : ℂ) :
    Tendsto (fun n => mollify h ((bumpSeq n).normed volume) z) atTop (nhds (h z)) := by sorry

View graph