OAI/Analysis/CircleDomains/Sobolev/LocalSobolevSmoothing.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local positive smoothing with errors relative to the original weak gradient. Compact cutoffs are removed on a neighborhood of the core.

  1. theorem OAI.CircleDomainRigidity.weakPartial_congrOn line 16
  2. theorem OAI.CircleDomainRigidity.weakGrad_eq_on_cutoff_plateau line 26
  3. theorem OAI.CircleDomainRigidity.tendsto_eLpNorm_restrict_zero line 41
  4. theorem OAI.CircleDomainRigidity.exists_local_positive_sobolev_smoothing line 48