OAI/Analysis/CircleDomains/Sobolev/MollificationMovingPoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual positive mollifiers converge at moving points whenever those points converge. Only continuity near a compact ball is used.

  1. lemma OAI.CircleDomainRigidity.planarMollification_tendsto_moving line 12