OAI/Analysis/CircleDomains/Sobolev/HilbertWeakSubsequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The bounded Hilbert-space subsequence used for the scalar fillings and their two L² differential components. It follows from the library's sequential Banach–Alaoglu theorem and the Riesz representation isometry.

  1. theorem OAI.CircleDomainRigidity.exists_hilbert_weak_subsequence line 14