OAI/Analysis/CircleDomains/Selection/FinitePointAvoidance.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An L² occupation density makes every fixed finite physical-domain point polar for a code law whose terminal point lies outside the domain.

  1. theorem OAI.CircleDomainRigidity.finite_domain_point_avoided line 22