OAI/Analysis/CircleDomains/Reflection/CompactReflectionCoefficient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The reflection-invariant extension remains compactly supported: every non-base tile lies inside one of the original finitely many disks.

  1. lemma OAI.CircleDomainRigidity.exists_compact_reflection_coefficient line 14