OAI/Analysis/CircleDomains/Sobolev/LocallySobolevACL.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coordinate absolute continuity for continuous local W1,2 functions, obtained from compact cutoffs without assumptions at infinity.

  1. lemma OAI.CircleDomainRigidity.compact_core_sobolev_coordinate_ACL line 12
  2. lemma OAI.CircleDomainRigidity.locally_sobolev_coordinate_absolutelyContinuous line 37