OAI/Analysis/CircleDomains/Selection/PeriodDomainIntersections.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A compact mask away from the image of infinity has a compact physical inverse image. This converts the two-cut coarea estimate into finite expected domain intersections of a masked period level.

  1. theorem OAI.CircleDomainRigidity.mean_masked_circle_domain_count_finite line 22