OAI/Analysis/CircleDomains/Sobolev/SmoothRectangleExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A smooth function on a neighborhood of a closed rectangle has a compactly supported smooth extension agreeing there on an open set.

  1. theorem OAI.CircleDomainRigidity.exists_rectangle_cutoff_one_near line 13
  2. theorem OAI.CircleDomainRigidity.exists_smooth_rectangle_extension line 31