OAI/Analysis/CircleDomains/Modulus/NormalizedComponentQuotient.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalize the component quotient at the source point at infinity. The dust then has no point at infinity, so every marked endpoint admits the physical collars used in the local-exclusion construction.

  1. theorem OAI.CircleDomainRigidity.normalized_component_quotient_of_moore line 14