ComplexLocalScalarWitness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A local complex scalar with square-integrable value and differential has the explicit physical Sobolev witness on its open source region.