OAI/Analysis/CircleDomains/Sobolev/EnergyLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Localizing the finite-transfer energy estimate

Exact agreement of a coordinate and metric on the retained core, together with small nonnegative total energy outside it, gives the manuscript's localized estimate after any measurable part of that core is removed.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.localized_energy_lt line 17