OAI/Analysis/CircleDomains/Sobolev/PositiveSobolevApproximation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

An explicit positive mollification of a compactly supported planar Sobolev function. The values and weak derivatives converge in L².

  1. def OAI.CircleDomainRigidity.planarMollification line 17
  2. theorem OAI.CircleDomainRigidity.planarMollification_smooth line 21
  3. theorem OAI.CircleDomainRigidity.planarMollification_mem_Icc line 28
  4. theorem OAI.CircleDomainRigidity.planarMollification_hasCompactSupport line 33
  5. theorem OAI.CircleDomainRigidity.tendsto_planarMollifier_radius line 38
  6. theorem OAI.CircleDomainRigidity.planarMollification_tsupport_subset line 43
  7. theorem OAI.CircleDomainRigidity.planarMollification_support_eventually line 60
  8. theorem OAI.CircleDomainRigidity.planarMollification_eventually_eq_on_plateau line 70
  9. theorem OAI.CircleDomainRigidity.planarMollification_derivative_of_weak line 81
  10. theorem OAI.CircleDomainRigidity.planarMollification_derivative line 124
  11. theorem OAI.CircleDomainRigidity.planarMollification_tendsto_L2 line 133
  12. theorem OAI.CircleDomainRigidity.planarMollification_tendsto_gradient_L2 line 141
  13. theorem OAI.CircleDomainRigidity.exists_positive_smooth_compact_approx line 155