OAI/Analysis/CircleDomains/Probability/PositiveMassCompactLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

If zero is absent from the image, compact localization can also retain a positive lower mass. The resulting compact family avoids zero.

  1. lemma OAI.CircleDomainRigidity.exists_compact_nonzero_modulus_localization line 14