OAI/Analysis/CircleDomains/Sobolev/SmoothScalarWeakLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded smooth scalar energies give an actual Sobolev limit, retaining the common subsequence and every L2 derivative pairing.

  1. structure OAI.CircleDomainRigidity.ScalarSmoothWeakLimit line 13
  2. lemma OAI.CircleDomainRigidity.exists_scalarSmoothWeakLimit line 22