OAI/Analysis/CircleDomains/Sobolev/RectangleSobolev.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

ACL and an L² bound on the line derivatives produce an actual local Sobolev gradient. All gradient fields here are constructed Borel functions.

  1. theorem OAI.CircleDomainRigidity.rectangle_restrict_Ioo_eq_Icc line 16
  2. theorem OAI.CircleDomainRigidity.exists_rectangle_weak_gradient line 22