OAI/Analysis/CircleDomains/Sobolev/LocallySobolevPartials.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Classical coordinate partials for the precise continuous representative of a genuinely local W1,2 function. No global integrability is assumed.

  1. def OAI.CircleDomainRigidity.scalarBallWeakWitness line 13
  2. lemma OAI.CircleDomainRigidity.locally_sobolev_coordinate_ae_hasDerivAt line 22