OAI/Analysis/CircleDomains/Sobolev/LocalSobolevNullLevels.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The zero-gradient conclusion on scalar null values is local on any open source domain. Compact cutoffs reduce it to planar coarea; an exhaustion covers the entire domain.

  1. theorem OAI.CircleDomainRigidity.local_sobolev_gradient_zero_on_null_values_compact line 15
  2. theorem OAI.CircleDomainRigidity.local_sobolev_gradient_zero_on_null_values line 55