OAI/Analysis/CircleDomains/Sobolev/CircleEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Localized energy for periodic differentials

Agreement of circle maps near the retained core implies agreement of their intrinsic differentials. Original L² energy controls the entire unbounded core; smoothness on a compact tail controls the remainder.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleGradient_congr_of_eventuallyEq line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.fieldEnergy_spherical line 34
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_fieldEnergy_spherical_of_memLp line 41
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrableOn_fieldEnergy_with_cofinite_core line 52
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.localized_circle_energy_lt line 72