OAI/Analysis/CircleDomains/Sobolev/PositiveMollification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Normalized smooth mollifiers preserve actual interval bounds and constant plateaus. These are pointwise bounds on the input neighborhood.

  1. theorem OAI.CircleDomainRigidity.normed_convolution_mem_Icc line 19
  2. theorem OAI.CircleDomainRigidity.normed_convolution_eq_of_constant line 36