OAI/Analysis/CircleDomains/Sobolev/BoundedWeakIdentification.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

On a measurable region where uniformly bounded functions converge pointwise, their L² weak limit has the same values almost everywhere.

  1. theorem OAI.CircleDomainRigidity.ae_eq_on_of_bounded_weak_pointwise line 13