CoreGeometry.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Keeping the selected physical core away from all terminal disks

A closed planar core extends across infinity to a compact spherical core. Its quotient image is disjoint from the quotient dust. Thus the terminal and filling neighborhoods can be chosen away from the entire retained core. Compact planar tail pieces suffice for the metric step.

def OAI.CircleDomainRigidity.FiniteTransfer.sphericalCore line 22
theorem OAI.CircleDomainRigidity.FiniteTransfer.coe_mem_sphericalCore line 25
theorem OAI.CircleDomainRigidity.FiniteTransfer.infty_mem_sphericalCore line 29
theorem OAI.CircleDomainRigidity.FiniteTransfer.isCompact_sphericalCore line 33
theorem OAI.CircleDomainRigidity.FiniteTransfer.sphericalCore_subset_domain line 39

theorem OAI.CircleDomainRigidity.FiniteTransfer.quotient_core_disjoint_dust line 50

Source documentation

The quotient image of any retained physical core misses every collapsed complementary component.

theorem quotient_core_disjoint_dust
    {G C : Set Sphere} (π : Sphere → Sphere) (hCG : C ⊆ G)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) :
    Disjoint (π '' C) (π '' Gᶜ) := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.FiniteTransfer.quotient_core_safe_open line 63

Source documentation

The complement of the compact quotient image is an open neighborhood of all dust points, whose full physical preimage avoids the core.

theorem quotient_core_safe_open
    {G C : Set Sphere} (π : Sphere → Sphere) (hπ : Continuous π)
    (hC : IsCompact C) (hCG : C ⊆ G)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) :
    IsOpen (π '' C)ᶜ ∧ π '' Gᶜ ⊆ (π '' C)ᶜ ∧
      Disjoint (π ⁻¹' (π '' C)ᶜ) C := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks.closure_disjoint_core line 76
Source documentation
Actual terminal disks in the prescribed quotient neighborhoods avoid the retained core, including their boundaries.
```
theorem PhysicalTerminalDisks.closure_disjoint_core
    {I : Type*} {G B C : Set Sphere} {π : Sphere → Sphere}
    {p : I → Sphere} {O : I → Set Sphere} (D : PhysicalTerminalDisks G π B p O)
    (hO : ∀ i, O i ⊆ (π '' C)ᶜ) (i : I) :
    Disjoint (((↑) : ℂ → Sphere) '' closure (jordanInterior (D.H i))) C := by
…
```
Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks, OAI.CircleDomainRigidity.jordanInterior
theorem OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks.core_subset_completedRegion line 85

theorem OAI.CircleDomainRigidity.FiniteTransfer.quotient_dust_eq_compl_image line 96

Source documentation

The two standard descriptions of quotient dust agree for the actual component-collapse map.

theorem quotient_dust_eq_compl_image
    {G : Set Sphere} (π : Sphere → Sphere) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) :
    π '' Gᶜ = (π '' G)ᶜ := by
…

Mentions: OAI.CircleDomainRigidity.Sphere

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_physical_terminals_avoiding_core line 115

Source documentation

Construct the actual terminal disks in arbitrary prescribed neighborhoods and automatically keep their closed caps off the retained core. Including infinity in the core also excludes the infinity fiber without an additional assumption on the selected indices.

theorem exists_physical_terminals_avoiding_core
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    {I : Type*} [Fintype I] {G C : Set Sphere} (hG : IsOpen G)
    (π : Sphere → Sphere) (hπ : Continuous π) (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (hTD : IsTotallyDisconnected (π '' Gᶜ)) (hC : IsCompact C) (hCG : C ⊆ G)
    (hinfty : OnePoint.infty ∈ C) (p : I → Sphere) (hp : Injective p)
    (hpB : ∀ i, p i ∈ π '' Gᶜ) (O : I → Set Sphere) (hO : ∀ i, O i ∈ 𝓝 (p i)) :
    ∃ D : PhysicalTerminalDisks G π (π '' Gᶜ) p O,
      ∀ i, Disjoint (((↑) : ℂ → Sphere) '' closure (jordanInterior (D.H i))) C := by
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks, OAI.CircleDomainRigidity.jordanInterior

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_compact_tail_piece line 143
Source documentation
For a core containing a neighborhood of infinity the entire tail integral can be computed on one compact part of the finite chart.
```
theorem exists_compact_tail_piece
    {Q K : Set (ℝ × ℝ)} (hQ : IsClosed Q) (hK : IsCompact (closure Kᶜ)) :
    ∃ R : ℝ, 0 < R ∧ IsCompact (Q ∩ closedBall 0 R) ∧
      Q \ K = (Q ∩ closedBall 0 R) \ K := by
…
```