OccupationNeighborhood.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The square occupation density has arbitrarily small mass in quotient neighborhoods of a dust point, because its entire fibre lies off the domain.

theorem OAI.CircleDomainRigidity.exists_open_small_occupation_energy line 22