OAI/Analysis/CircleDomains/Uniformization/FiniteCompletion.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

The retained core and completed domain of a finite disk construction

The core is the spherical complement of all terminal and filling disks. If the disks cover the preimage of the quotient dust, the core is a compact subset of the original domain. Filling the second family leaves precisely the complement of the terminal interiors. This completed compact set has the open neighborhood consisting of the original domain and the filling interiors. In a finite chart its bounded closed pieces are compact, even though the entire planar exterior is unbounded.

The final statements apply the actual finite patching construction to this open neighborhood and recover local agreement on the retained core.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion line 26
  2. def OAI.CircleDomainRigidity.FiniteTransfer.completionCore line 29
  3. def OAI.CircleDomainRigidity.FiniteTransfer.completedRegion line 32
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.isOpen_sphericalDiskUnion line 35
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.coe_mem_sphericalDiskUnion line 39
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.infty_not_mem_sphericalDiskUnion line 43
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.isCompact_completionCore line 47
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.isCompact_completedRegion line 51
  9. theorem OAI.CircleDomainRigidity.FiniteTransfer.completionCore_subset_domain line 57

    Source documentation

    Covering the actual preimage of the dust removes every point outside the original domain.

    theorem completionCore_subset_domain {I J : Type*}
    (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (G B : Set Sphere) (π : Sphere → Sphere)
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (hcover : π ⁻¹' B ⊆ sphericalDiskUnion T ∪ sphericalDiskUnion F) :
    completionCore T F ⊆ G := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion, OAI.CircleDomainRigidity.FiniteTransfer.completionCore

  10. theorem OAI.CircleDomainRigidity.FiniteTransfer.disjoint_sphericalDiskUnion_of_closures line 67
  11. theorem OAI.CircleDomainRigidity.FiniteTransfer.completedRegion_eq_core_union_fillings line 83

    Source documentation

    Filling the second family leaves exactly the complement of the terminal interiors, including their boundaries.

    theorem completedRegion_eq_core_union_fillings {I J : Type*}
    (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (hTF : ∀ i j, Disjoint (closure (jordanInterior (T i)))
      (closure (jordanInterior (F j)))) :
    completedRegion T = completionCore T F ∪ sphericalDiskUnion F := by
…

    Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.completedRegion, OAI.CircleDomainRigidity.FiniteTransfer.completionCore, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion

  12. theorem OAI.CircleDomainRigidity.FiniteTransfer.filling_closure_subset_completedRegion line 100

    Source documentation

    Every filling closure is disjoint from the terminal interiors.

    theorem filling_closure_subset_completedRegion {I J : Type*}
    (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (hTF : ∀ i j, Disjoint (closure (jordanInterior (T i)))
      (closure (jordanInterior (F j)))) (j : J) :
    ((↑) : ℂ → Sphere) '' closure (jordanInterior (F j)) ⊆ completedRegion T := by
…

    Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.completedRegion

  13. theorem OAI.CircleDomainRigidity.FiniteTransfer.preimage_image_sphericalDiskUnion line 111

    Source documentation

    Terminal boundaries in the original domain force whole quotient fibers to stay on one side, so the union of terminal interiors is saturated.

    theorem preimage_image_sphericalDiskUnion
    {I : Type*} (T : I → ℂ ≃ₜ ℂ) (G : Set Sphere) (π : Sphere → Sphere)
    (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (hboundary : ∀ i z, z ∈ frontier (jordanInterior (T i)) → (z : Sphere) ∈ G) :
    π ⁻¹' (π '' sphericalDiskUnion T) = sphericalDiskUnion T := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion

  14. theorem OAI.CircleDomainRigidity.FiniteTransfer.dust_preimage_covered_of_remainder_cover line 131

    Source documentation

    Filling the quotient dust left after the terminal interiors covers the complete physical dust preimage. Saturation, rather than just fiber representative selection, is what makes this implication valid.

    theorem dust_preimage_covered_of_remainder_cover
    {I J : Type*} (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (G B : Set Sphere) (π : Sphere → Sphere) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (hboundary : ∀ i z, z ∈ frontier (jordanInterior (T i)) → (z : Sphere) ∈ G)
    (hfill : π ⁻¹' (B \ (π '' sphericalDiskUnion T)) ⊆ sphericalDiskUnion F) :
    π ⁻¹' B ⊆ sphericalDiskUnion T ∪ sphericalDiskUnion F := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion

  15. theorem OAI.CircleDomainRigidity.FiniteTransfer.spherical_remainder_cover_of_physical_cover line 148

    Source documentation

    A physical finite-chart filling cover supplies the spherical cover as soon as the quotient remainder omits the infinity fiber.

    theorem spherical_remainder_cover_of_physical_cover
    {I J : Type*} (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (B : Set Sphere) (π : Sphere → Sphere)
    (hinfty : π OnePoint.infty ∉ B \ (π '' sphericalDiskUnion T))
    (hfill : (fun z : ℂ => π (z : Sphere)) ⁻¹' (B \ (π '' sphericalDiskUnion T)) ⊆
      ⋃ j, jordanInterior (F j)) :
    π ⁻¹' (B \ (π '' sphericalDiskUnion T)) ⊆ sphericalDiskUnion F := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion, OAI.CircleDomainRigidity.jordanInterior

  16. theorem OAI.CircleDomainRigidity.FiniteTransfer.completedRegion_subset_extension_domain line 164

    Source documentation

    No disjointness is needed for this useful containment: every point left after deleting the terminals is either physical or inside a filling.

    theorem completedRegion_subset_extension_domain {I J : Type*}
    (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (G B : Set Sphere) (π : Sphere → Sphere)
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (hcover : π ⁻¹' B ⊆ sphericalDiskUnion T ∪ sphericalDiskUnion F) :
    completedRegion T ⊆ G ∪ sphericalDiskUnion F := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion, OAI.CircleDomainRigidity.FiniteTransfer.completedRegion

  17. theorem OAI.CircleDomainRigidity.FiniteTransfer.completion_has_open_extension_domain line 177
  18. theorem OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks.completion_geometry line 192

    Source documentation

    Direct interface for the actual terminal family and a finite filling cover of its quotient remainder. No independent total-dust-cover premise is needed.

    theorem PhysicalTerminalDisks.completion_geometry
    {I J : Type*} {G B : Set Sphere} {π : Sphere → Sphere}
    {p : I → Sphere} {O : I → Set Sphere}
    (D : PhysicalTerminalDisks G π B p O) (F : J → ℂ ≃ₜ ℂ)
    (hG : IsOpen G) (hsurj : Surjective π)
    (hr : ∀ x y, π x = π y ↔
      x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x))
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (hfill : π ⁻¹' (B \ (π '' sphericalDiskUnion D.H)) ⊆ sphericalDiskUnion F) :
    IsCompact (completionCore D.H F) ∧ completionCore D.H F ⊆ G ∧
      IsCompact (completedRegion D.H) ∧ IsOpen (G ∪ sphericalDiskUnion F) ∧
      completedRegion D.H ⊆ G ∪ sphericalDiskUnion F := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.PhysicalTerminalDisks, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion, OAI.CircleDomainRigidity.FiniteTransfer.completionCore, OAI.CircleDomainRigidity.FiniteTransfer.completedRegion

  19. theorem OAI.CircleDomainRigidity.FiniteTransfer.compact_chart_completion_in_extension_domain line 213

    Source documentation

    The bounded finite-chart pieces used for local metric selection are compact and remain in the extension domain.

    theorem compact_chart_completion_in_extension_domain {I J : Type*}
    (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (G B : Set Sphere) (π : Sphere → Sphere)
    (hbad : ∀ x ∈ Gᶜ, π x ∈ B)
    (hcover : π ⁻¹' B ⊆ sphericalDiskUnion T ∪ sphericalDiskUnion F)
    (c : ℂ) (R : ℝ) :
    IsCompact ((((↑) : ℂ → Sphere) ⁻¹' completedRegion T) ∩ closedBall c R) ∧
      (((↑) : ℂ → Sphere) ⁻¹' completedRegion T) ∩ closedBall c R ⊆
        ((↑) : ℂ → Sphere) ⁻¹' (G ∪ sphericalDiskUnion F) := by
…

    Mentions: OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion, OAI.CircleDomainRigidity.FiniteTransfer.completedRegion

  20. theorem OAI.CircleDomainRigidity.FiniteTransfer.contDiffOn_finite_completion_patch line 230

    Source documentation

    Patching the filling interiors gives smooth coordinates on the actual open completed domain, not merely on the old physical domain.

    theorem contDiffOn_finite_completion_patch
    {J : Type*} [Fintype J] (F : J → ℂ ≃ₜ ℂ)
    (hF : Pairwise (Disjoint on fun j => closure (jordanInterior (F j))))
    {G : Set Sphere} (hG : IsOpen G)
    (f : ℂ → ℝ) (hf : ContDiffOn ℝ ∞ f (((↑) : ℂ → Sphere) ⁻¹' G))
    (g : J → ℂ → ℝ) (hg : ∀ j, ContDiffOn ℝ ∞ (g j) (jordanInterior (F j)))
    (hagree : ∀ j z, z ∈ frontier (jordanInterior (F j)) → g j =ᶠ[𝓝 z] f) :
    ContDiffOn ℝ ∞ (patchOpenRegions (fun j => jordanInterior (F j)) g f)
      (((↑) : ℂ → Sphere) ⁻¹' (G ∪ sphericalDiskUnion F)) := by
…

    Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions, OAI.CircleDomainRigidity.FiniteTransfer.sphericalDiskUnion

  21. theorem OAI.CircleDomainRigidity.FiniteTransfer.finite_completion_patch_eq_near_core line 253

    Source documentation

    On the retained core the patched coordinate agrees locally with the old one, including points on any filling boundary.

    theorem finite_completion_patch_eq_near_core
    {I J : Type*} [Fintype J] (T : I → ℂ ≃ₜ ℂ) (F : J → ℂ ≃ₜ ℂ)
    (f : ℂ → ℝ) (g : J → ℂ → ℝ)
    (hagree : ∀ j z, z ∈ frontier (jordanInterior (F j)) → g j =ᶠ[𝓝 z] f) :
    patchOpenRegions (fun j => jordanInterior (F j)) g f =ᶠ[
      𝓝ˢ (((↑) : ℂ → Sphere) ⁻¹' completionCore T F)] f := by
…

    Mentions: OAI.CircleDomainRigidity.jordanInterior, OAI.CircleDomainRigidity.FiniteTransfer.patchOpenRegions, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.FiniteTransfer.completionCore