OAI/Analysis/CircleDomains/Rigidity/MaskedCircleEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Localized energy on the actual coordinate masks

The retained core contains the mask boundaries. Smoothness on the compact tail and original masked L² data suffice for whole-domain integrability and comparison after deleting any measurable part of the core. No extension across a mask boundary is required.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_maskedCircleWedges_off_boundaries line 23
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrableOn_masked_circle_energy_tail line 37
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrableOn_masked_circle_energy line 58
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.localized_masked_circle_energy_lt line 85