ComponentBarriers.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

From analytic barriers to circle-domain component control

The complementary components are the components of the sphere's closed complement. Components admitting vanishing absolutely continuous barriers are points. If all remaining components are round disks, the domain is a circle domain.

def OAI.CircleDomainRigidity.planarPart line 21
Source documentation
The finite-coordinate part of a sphere set.
```
def planarPart (K : Set Sphere) : Set ℂ := (fun z : ℂ => (z : Sphere)) ⁻¹' K
```
Mentions: OAI.CircleDomainRigidity.Sphere
theorem OAI.CircleDomainRigidity.image_planarPart line 23
theorem OAI.CircleDomainRigidity.planarPart_isCompact_isConnected line 31
Source documentation
A compact connected sphere set missing infinity is a compact connected plane set in the standard chart.
```
theorem planarPart_isCompact_isConnected {K : Set Sphere}
    (hcompact : IsCompact K) (hconn : IsConnected K) (hinfty : ∞ ∉ K) :
    IsCompact (planarPart K) ∧ IsConnected (planarPart K) := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.planarPart
theorem OAI.CircleDomainRigidity.IsComplementaryComponent.isCompact_isConnected line 47
Source documentation
A genuine complementary component is compact and connected.
```
theorem IsComplementaryComponent.isCompact_isConnected {G K : Set Sphere}
    (hK : IsComplementaryComponent G K) (hG : IsOpen G) :
    IsCompact K ∧ IsConnected K := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsComplementaryComponent

theorem OAI.CircleDomainRigidity.IsComplementaryComponent.eq_singleton_of_barriers line 58

Source documentation

Vanishing projection barriers force an actual complementary component to be a singleton, including components with no interior.

theorem IsComplementaryComponent.eq_singleton_of_barriers
    {G K : Set Sphere} (hK : IsComplementaryComponent G K)
    (hG : IsOpen G) (hinfty : ∞ ∈ G)
    (hre : HasVanishingRectangleBarriers
      (sInf (Complex.re '' planarPart K)) (sSup (Complex.re '' planarPart K)))
    (him : HasVanishingRectangleBarriers
      (sInf (Complex.im '' planarPart K)) (sSup (Complex.im '' planarPart K))) :
    ∃ p : Sphere, K = {p} := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsComplementaryComponent, OAI.CircleDomainRigidity.HasVanishingRectangleBarriers, OAI.CircleDomainRigidity.planarPart

theorem OAI.CircleDomainRigidity.isCircleDomain_of_component_barriers line 82
Source documentation
The final component-recognition implication with explicit analytic barrier data. This remains a reduction: barrier existence and round filling have not been assumed to be published results.
```
theorem isCircleDomain_of_component_barriers
    {G : Set Sphere} (hG : IsOpen G) (hconn : IsConnected G) (hinfty : ∞ ∈ G)
    (hcontrol : ∀ K, IsComplementaryComponent G K →
      IsRoundClosedDisk K ∨
        (HasVanishingRectangleBarriers
          (sInf (Complex.re '' planarPart K)) (sSup (Complex.re '' planarPart K)) ∧
         HasVanishingRectangleBarriers
          (sInf (Complex.im '' planarPart K)) (sSup (Complex.im '' planarPart K)))) :
    IsCircleDomain G := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.IsComplementaryComponent, OAI.CircleDomainRigidity.IsRoundClosedDisk, OAI.CircleDomainRigidity.HasVanishingRectangleBarriers, OAI.CircleDomainRigidity.planarPart, OAI.CircleDomainRigidity.IsCircleDomain