ComponentControl.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Recognition of the limiting circle domain

Complementary-component coverage, collapse of unmarked components, and filling of marked components together identify the limiting image as a circle domain.

def OAI.CircleDomainRigidity.IsComplementaryComponent line 17
Source documentation
An actual connected component of the closed complement.
```
def IsComplementaryComponent (G K : Set Sphere) : Prop :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere
theorem OAI.CircleDomainRigidity.IsComplementaryComponent.nonempty line 21
Source documentation
Complementary components are nonempty.
```
theorem IsComplementaryComponent.nonempty {G K : Set Sphere}
    (h : IsComplementaryComponent G K) : K.Nonempty := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsComplementaryComponent
theorem OAI.CircleDomainRigidity.isCircleDomain_of_component_control line 29
Source documentation
The final component argument requires coverage, unmarked collapse, and marked filling separately. In particular, merely finding round disks inside marked components is insufficient.
```
theorem isCircleDomain_of_component_control
    {G : Set Sphere} (hopen : IsOpen G) (hconn : IsConnected G)
    {B : Type*} (component : B → Set Sphere) (marked : Set B)
    (coverage : ∀ K, IsComplementaryComponent G K → ∃ b, K = component b)
    (collapse : ∀ b, b ∉ marked → ∃ p, component b = {p})
    (filling : ∀ b, b ∈ marked → IsRoundClosedDisk (component b)) :
    IsCircleDomain G := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsComplementaryComponent, OAI.CircleDomainRigidity.IsRoundClosedDisk, OAI.CircleDomainRigidity.IsCircleDomain
theorem OAI.CircleDomainRigidity.eq_zero_of_arbitrarily_small_bound line 47
Source documentation
Vanishing barrier estimates force every nonnegative projected length to vanish. This is the real-number limit step of the unmarked-collapse argument (§6, thm:unmarked-collapse).
```
theorem eq_zero_of_arbitrarily_small_bound {length C : ℝ}
    (hlength : 0 ≤ length) (hC : 0 ≤ C)
    (hbound : ∀ ε : ℝ, 0 < ε → length ≤ C * ε) : length = 0 := by
…
```

theorem OAI.CircleDomainRigidity.singleton_of_arbitrarily_small_dist line 63

Source documentation

A metric version of the collapse step: vanishing pairwise distances give a singleton, provided the component is nonempty.

theorem singleton_of_arbitrarily_small_dist {X : Type*} [MetricSpace X]
    {K : Set X} (hne : K.Nonempty) {C : ℝ} (hC : 0 ≤ C)
    (hbound : ∀ x ∈ K, ∀ y ∈ K, ∀ ε : ℝ, 0 < ε → dist x y ≤ C * ε) :
    ∃ x, K = {x} := by
…