RealEndProtrusion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Protrusion localization for the actual marked components of the real-model limit.

theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.plane_eq_component line 21
Source documentation
Removing infinity preserves these complementary components, which all lie in the finite plane.
```
theorem plane_eq_component {x : ℂ} (hx : x ∈ E.plane) :
    E.plane = connectedComponentIn
      (((↑) : ℂ → Sphere) ⁻¹' (extendAtInfinity L.function '' G)ᶜ) x := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.extendAtInfinity

theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.exists_protrusion_and_anchor line 44

Source documentation

If an assigned marked disk does not fill its component, there is a nontrivial local continuum outside the disk and a nearby genuine target ball serving as the anchor for the barrier/stream alternatives.

theorem exists_protrusion_and_anchor
    (hG : IsOpen G)
    (hr : ∀ x y, π x = π y ↔ x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (hq : q ∈ Gᶜ) {s : S} (hqs : π q = σ s)
    (hne : E.plane ≠ closedBall (L.center s) (L.radius s)) :
    ∃ (x : ℂ) (ρ : ℝ) (Q : Set ℂ) (a : ℂ) (δ : ℝ),
      0 < ρ ∧ x ∈ frontier E.plane ∧
      Disjoint (closedBall x (2 * ρ)) (closedBall (L.center s) (L.radius s)) ∧
      IsCompact Q ∧ IsConnected Q ∧ Q.Nontrivial ∧ x ∈ Q ∧
      Q ⊆ E.plane ∩ ball x ρ ∧ 0 < δ ∧
      closedBall a δ ⊆ (((↑) : ℂ → Sphere) ⁻¹' (extendAtInfinity L.function '' G)) ∩ ball x ρ := by
…

Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.extendAtInfinity