GeometricCompletion.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Geometric completion for the selected reciprocal grid

The terminal remainder and its safe neighborhood are constructed from the actual terminal disks. The descending filling theorem then covers all remaining dust, with disjoint caps away from the retained core. Every filling boundary meets at most one coordinate grid.

theorem OAI.CircleDomainRigidity.FiniteTransfer.exists_geometric_completion_for_grid line 26

Source documentation

Geometric assembly for the actual collision terminal set. The free point conditions are precisely the trace and compatibility conclusions of the preceding level-set construction.

theorem exists_geometric_completion_for_grid
    (hsard : SmoothPlanarSard) (hschoenflies : PlanarSchoenflies)
    (G : Set Sphere) (π : Sphere → Sphere) (hπ : Continuous π)
    (hclosed : IsClosedMap π) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    {B C : Set Sphere} (hB : IsClosed B) (hBdef : B = π '' Gᶜ)
    (hTD : IsTotallyDisconnected B) (hC : IsCompact C) (hCG : C ⊆ G)
    (hinfty : OnePoint.infty ∈ C)
    {n N : ℕ} {S : Type*} (U : Set Sphere) (f : Fin n → Sphere → ℝ)
    (M : Fin n → ℝ) (hbounded : ∀ i x, x ∈ U → |f i x| ≤ M i)
    (σ : S → Sphere) (hσB : ∀ s, σ s ∈ B)
…

Mentions: OAI.CircleDomainRigidity.SmoothPlanarSard, OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.Sphere