OAI/Analysis/CircleDomains/Sobolev/IndicatorL2Energy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Convert a small weighted mass of a changed set into the exact L2 error contribution used by source priority interpolation.

  1. theorem OAI.CircleDomainRigidity.indicator_L2_norm_lt_of_energy_lt line 12