OAI/Analysis/CircleDomains/Probability/CountableDiffuseCodeLaws.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The crossing contradiction for a family of actual positive code laws. Pairwise dust contacts are countable; square occupation and hit bounds make all remaining meetings small on a common member of the countable collar basis.

  1. theorem OAI.CircleDomainRigidity.countable_diffuse_code_laws line 25