OAI/Analysis/CircleDomains/Probability/MeasureFamilyCompactLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact ambient family retains any prescribed strict modulus threshold. This is the tightness localization for the Borel-image argument.

  1. lemma OAI.CircleDomainRigidity.exists_compact_modulus_localization line 13