OAI/Analysis/CircleDomains/Sobolev/PotentialRectangleACL.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual barrier pullback is absolutely continuous on almost every horizontal and vertical segment in each compact physical chart rectangle.

  1. def OAI.CircleDomainRigidity.closedComplexRectangle line 20
  2. theorem OAI.CircleDomainRigidity.isCompact_closedComplexRectangle line 23
  3. theorem OAI.CircleDomainRigidity.mk_mem_closedComplexRectangle line 27
  4. theorem OAI.CircleDomainRigidity.potential_rectangle_ACL line 35