ProtrusionGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Initial geometric localization of a marked component protruding beyond its round disk.

theorem OAI.CircleDomainRigidity.exists_frontier_point_outside_closedBall line 17
Source documentation
A compact planar set extending beyond a round disk has a boundary point beyond that disk. No boundary regularity is required.
```
theorem exists_frontier_point_outside_closedBall
    {K : Set ℂ} (hK : IsCompact K) {c : ℂ} {r : ℝ} (hr : 0 ≤ r)
    (hnot : ¬ K ⊆ closedBall c r) :
    ∃ x ∈ frontier K, r < dist x c := by
…
```
theorem OAI.CircleDomainRigidity.frontier_complement_component_subset_closure line 48
Source documentation
Every boundary point of a complementary component can be approached from the planar domain.
```
theorem frontier_complement_component_subset_closure
    {U : Set ℂ} (hU : IsOpen U) {q : ℂ} (hq : q ∈ Uᶜ) :
    frontier (connectedComponentIn Uᶜ q) ⊆ closure U := by
…
```

theorem OAI.CircleDomainRigidity.exists_domain_ball_near_component_frontier line 69

Source documentation

A genuine closed domain ball can be placed arbitrarily near a boundary point of a complementary component.

theorem exists_domain_ball_near_component_frontier
    {U : Set ℂ} (hU : IsOpen U) {q : ℂ} (hq : q ∈ Uᶜ)
    {x : ℂ} (hx : x ∈ frontier (connectedComponentIn Uᶜ q))
    {ρ : ℝ} (hρ : 0 < ρ) :
    ∃ (a : ℂ) (s : ℝ), 0 < s ∧ closedBall a s ⊆ U ∩ ball x ρ := by
…

theorem OAI.CircleDomainRigidity.exists_local_protrusion line 82

Source documentation

A protruding continuum has a small nontrivial subcontinuum separated from its marked round disk, with a fixed pair of nested neighborhoods.

theorem exists_local_protrusion
    {K : Set ℂ} (hK : IsCompact K) (hconn : IsConnected K)
    {c : ℂ} {r : ℝ} (hr : 0 ≤ r) (hDK : closedBall c r ⊆ K)
    (hne : K ≠ closedBall c r) :
    ∃ (x : ℂ) (ρ : ℝ) (Q : Set ℂ),
      0 < ρ ∧ x ∈ frontier K ∧
      Disjoint (closedBall x (2 * ρ)) (closedBall c r) ∧
      IsCompact Q ∧ IsConnected Q ∧ Q.Nontrivial ∧ x ∈ Q ∧
      Q ⊆ K ∩ ball x ρ := by
…