OAI/Analysis/CircleDomains/Probability/MeasureFamilyNullUnions.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Countable unions of pointwise zero-modulus families have zero modulus. The admissible density is the square root of the sum of the squared individual densities, so the argument keeps every family member.

  1. lemma OAI.CircleDomainRigidity.measureFamilyModulus_zero_of_countable_cover line 15