OAI/Analysis/CircleDomains/Sobolev/L2DominatingSubsequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Strong L² convergence admits a cofinal subsequence with one L² pointwise majorant. This will pass smooth line payments to a continuous Sobolev limit without assuming an ACL representative theorem.

  1. theorem OAI.CircleDomainRigidity.exists_L2_dominating_subsequence line 13