OAI/Analysis/CircleDomains/Sobolev/LocalizedRealGradientNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact gradient norm transport on measurable subsets of the physical chart, used when excluding the permitted penalty region.

  1. theorem OAI.CircleDomainRigidity.real_chart_partial_eLpNorm_on line 15
  2. theorem OAI.CircleDomainRigidity.physical_coordinate_partial_eLpNorm_on line 43