OAI/Analysis/CircleDomains/Sobolev/CompactSobolevCutoff.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Smooth compact cutoffs turn local planar Sobolev functions into global Sobolev functions, to which positive mollification applies.

  1. theorem OAI.CircleDomainRigidity.memW1p_mul_compact_cutoff line 15
  2. theorem OAI.CircleDomainRigidity.exists_global_compact_cutoff_witness line 27
  3. theorem OAI.CircleDomainRigidity.compact_cutoff_mem_Icc line 49