OAI/Analysis/CircleDomains/Sobolev/WeightedSobolevErrors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative error estimates for multiplying local Sobolev approximations by smooth partition functions.

  1. theorem OAI.CircleDomainRigidity.aestronglyMeasurable_mul_of_support line 15
  2. theorem OAI.CircleDomainRigidity.eLpNorm_mul_le_of_support line 28
  3. theorem OAI.CircleDomainRigidity.tendsto_eLpNorm_mul_zero_of_support line 46
  4. theorem OAI.CircleDomainRigidity.tendsto_partition_derivative_error line 62
  5. theorem OAI.CircleDomainRigidity.aestronglyMeasurable_partition_derivative_error line 96