OAI/Analysis/CircleDomains/Sobolev/CompactMollifierSampling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform sampling control on compact sets, including exact preservation of constant regions and smooth cutoffs equal to one near a compact set.

  1. theorem OAI.CircleDomainRigidity.planarMollifier_samples_eventually line 16
  2. theorem OAI.CircleDomainRigidity.planarMollification_mem_Icc_on_compact_eventually line 28
  3. theorem OAI.CircleDomainRigidity.planarMollification_eq_on_compact_eventually line 37
  4. theorem OAI.CircleDomainRigidity.exists_smooth_compact_cutoff_one_near line 46