OAI/Analysis/CircleDomains/Probability/MeasureFamilyExceptional.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Fuglede's elementary exceptional-family estimate: an L² reference density has infinite integral only along a family of zero pointwise modulus.

  1. lemma OAI.CircleDomainRigidity.measureFamilyModulus_zero_of_infinite_integral line 15