OAI/Analysis/CircleDomains/Sobolev/CountableEnergyNeighborhoods.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Countably many source points admit shrinking prescribed neighborhoods whose union has arbitrarily small mass for an atomless finite energy measure.

  1. theorem OAI.CircleDomainRigidity.exists_shrinking_energy_balls line 13