OAI/Analysis/CircleDomains/Sobolev/SobolevNullLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coarea forces the actual weak gradient to vanish on the preimage of any null set of scalar values. In particular, every fixed level has zero gradient almost everywhere; no regularity of the level is assumed.

  1. theorem OAI.CircleDomainRigidity.sobolev_gradient_zero_on_null_values line 13
  2. theorem OAI.CircleDomainRigidity.sobolev_gradient_zero_on_level line 43