OAI/Analysis/CircleDomains/Sobolev/PrioritySupportEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Retain the small energy of the altered support, as required by the third term in the actual saved-barrier estimate.

  1. theorem OAI.CircleDomainRigidity.exists_priority_L2_approximation_with_support line 12