OAI/Analysis/CircleDomains/Sobolev/BoundedWeakRange.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Weak L² limits of functions valued in the unit interval still lie in that interval almost everywhere. The proof tests measurable sets.

  1. theorem OAI.CircleDomainRigidity.ae_mem_unitInterval_of_weak_limit line 13