LocalWeightedCollars.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Only the density near the requested collar is used. Extending it by zero removes any unnecessary global planar square-integrability requirement.

theorem OAI.CircleDomainRigidity.exists_weighted_collar_of_local_energy line 15