OAI/Analysis/CircleDomains/Sobolev/BorelSobolevGradient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Borel L² representatives of the two actual global weak derivatives. Changing these representatives preserves the Sobolev witness.

  1. def OAI.CircleDomainRigidity.scalarGradientRepresentative line 13
  2. theorem OAI.CircleDomainRigidity.scalarGradientRepresentative_ae line 19
  3. def OAI.CircleDomainRigidity.borelSobolevWitness line 24