OAI/Analysis/CircleDomains/Selection/OuterContours.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CircleDomainRigidity.jordanInterior line 19
2. theorem OAI.CircleDomainRigidity.jordanInterior_isOpen line 21
3. theorem OAI.CircleDomainRigidity.closure_jordanInterior line 24
4. theorem OAI.CircleDomainRigidity.isCompact_closure_jordanInterior line 28
5. theorem OAI.CircleDomainRigidity.interior_closure_jordanInterior line 33
6. theorem OAI.CircleDomainRigidity.frontier_jordanInterior line 38
7. theorem OAI.CircleDomainRigidity.isConnected_jordanInterior line 42
8. theorem OAI.CircleDomainRigidity.planar_unit_sphere_connected line 45
9. theorem OAI.CircleDomainRigidity.isConnected_frontier_jordanInterior line 48
10. theorem OAI.CircleDomainRigidity.planar_unit_exterior_connected line 53
11. theorem OAI.CircleDomainRigidity.isConnected_exterior_jordanInterior line 75
12. theorem OAI.CircleDomainRigidity.subset_inside_or_exterior line 80
13. theorem OAI.CircleDomainRigidity.exterior_not_bounded line 94
14. theorem OAI.CircleDomainRigidity.closed_fill_subset_of_frontier_subset line 100
15. theorem OAI.CircleDomainRigidity.closed_jordanInterior_subset_of_frontier_subset line 124

    Source documentation

    A Jordan contour contained in the interior of another Jordan disk has its entire closed fill in that interior.

    theorem closed_jordanInterior_subset_of_frontier_subset (H K : ℂ ≃ₜ ℂ)
        (hfront : frontier (jordanInterior H) ⊆ jordanInterior K) :
        closure (jordanInterior H) ⊆ jordanInterior K :=
    …

    Mentions: OAI.CircleDomainRigidity.jordanInterior

16. theorem OAI.CircleDomainRigidity.disjoint_or_nested_closed_fills line 132
17. theorem OAI.CircleDomainRigidity.disjoint_or_nested_jordanInteriors line 169

    Source documentation

    Disjoint Jordan contours have disjoint closed fills or one closed fill lies strictly inside the other disk.

    theorem disjoint_or_nested_jordanInteriors (H K : ℂ ≃ₜ ℂ)
        (hdisj : Disjoint (frontier (jordanInterior H)) (frontier (jordanInterior K))) :
        Disjoint (closure (jordanInterior H)) (closure (jordanInterior K)) ∨
          closure (jordanInterior H) ⊆ jordanInterior K ∨
          closure (jordanInterior K) ⊆ jordanInterior H :=
    …

    Mentions: OAI.CircleDomainRigidity.jordanInterior

18. theorem OAI.CircleDomainRigidity.exists_outer_jordanInteriors line 183

    Source documentation

    Select the outer members of a finite family of disjoint Jordan contours. Their closed disks are pairwise disjoint and cover all the original filled disks. Since this is a subfamily, any prescribed contour properties persist.

    theorem exists_outer_jordanInteriors {ι : Type*} [Finite ι]
        (H : ι → ℂ ≃ₜ ℂ)
        (hdisj : Pairwise (fun i j => Disjoint (frontier (jordanInterior (H i)))
          (frontier (jordanInterior (H j))))) :
        ∃ s : Set ι, s.Finite ∧
          s.Pairwise (fun i j => Disjoint (closure (jordanInterior (H i)))
            (closure (jordanInterior (H j)))) ∧
          (∀ i, ∃ j ∈ s, closure (jordanInterior (H i)) ⊆ closure (jordanInterior (H j))) ∧
          (⋃ i ∈ s, closure (jordanInterior (H i))) = ⋃ i, closure (jordanInterior (H i)) := by
    …

    Mentions: OAI.CircleDomainRigidity.jordanInterior

19. theorem OAI.CircleDomainRigidity.exists_outer_jordanInteriors_in_container line 227

    Source documentation

    The selected outer disks stay inside a Jordan container whenever every original boundary curve lies inside it. This is the containment step used when smoothing dust neighborhoods.

    theorem exists_outer_jordanInteriors_in_container {ι : Type*} [Finite ι]
        (H : ι → ℂ ≃ₜ ℂ) (K : ℂ ≃ₜ ℂ)
        (hdisj : Pairwise (fun i j => Disjoint (frontier (jordanInterior (H i)))
          (frontier (jordanInterior (H j)))))
        (hinside : ∀ i, frontier (jordanInterior (H i)) ⊆ jordanInterior K) :
        ∃ s : Set ι, s.Finite ∧
          s.Pairwise (fun i j => Disjoint (closure (jordanInterior (H i)))
            (closure (jordanInterior (H j)))) ∧
          (∀ i, ∃ j ∈ s, closure (jordanInterior (H i)) ⊆ closure (jordanInterior (H j))) ∧
          ∀ i ∈ s, closure (jordanInterior (H i)) ⊆ jordanInterior K := by
    …

    Mentions: OAI.CircleDomainRigidity.jordanInterior

20. theorem OAI.CircleDomainRigidity.frontier_jordanInterior_eq_circle_range line 241
21. theorem OAI.CircleDomainRigidity.exists_outer_circle_fills_in_container line 255

    Source documentation

    Actual disjoint closed fills for an outer subfamily of finitely many embedded circles in a Jordan container. The circle maps are retained, so smoothness and avoidance properties of those maps require no reconstruction.

    theorem exists_outer_circle_fills_in_container {ι : Type*} [Finite ι]
        (hschoenflies : PlanarSchoenflies) (γ : ι → Circle → ℂ)
        (hγ : ∀ i, Continuous (γ i)) (hinj : ∀ i, Injective (γ i))
        (hdisj : Pairwise (fun i j => Disjoint (range (γ i)) (range (γ j))))
        (K : ℂ ≃ₜ ℂ) (hinside : ∀ i, range (γ i) ⊆ jordanInterior K) :
        ∃ (H : ι → ℂ ≃ₜ ℂ) (s : Set ι), s.Finite ∧
          (∀ i, frontier (jordanInterior (H i)) = range (γ i)) ∧
          s.Pairwise (fun i j => Disjoint (closure (jordanInterior (H i)))
            (closure (jordanInterior (H j)))) ∧
          (∀ i, ∃ j ∈ s, closure (jordanInterior (H i)) ⊆ closure (jordanInterior (H j))) ∧
          ∀ i ∈ s, closure (jordanInterior (H i)) ⊆ jordanInterior K := by
    …

    Mentions: OAI.CircleDomainRigidity.PlanarSchoenflies, OAI.CircleDomainRigidity.jordanInterior