OAI/Analysis/CircleDomains/Sobolev/LocalMollificationCongruence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local almost-everywhere equality is preserved by mollification where the actual averaging ball stays inside the equality region.

  1. theorem OAI.CircleDomainRigidity.planarMollification_congr_on_ball line 12
  2. theorem OAI.CircleDomainRigidity.planarMollification_congr_on_compact_eventually line 35
  3. theorem OAI.CircleDomainRigidity.planarMollification_neg line 42