OAI/Analysis/CircleDomains/Sobolev/PartitionGradientEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Turn the constructed gradient error and a common local density bound into a global finite-energy estimate for the actual smooth function.

  1. theorem OAI.CircleDomainRigidity.partition_smooth_gradient_energy line 13