OAI/Analysis/CircleDomains/Sobolev/LocalizedPartitionEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Localizing the global smoothing error keeps the original density on the complement of a penalty region.

  1. theorem OAI.CircleDomainRigidity.partition_smooth_gradient_energy_on line 14