OAI/Geometry/PlaneColoring/GraphPatches.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EuclideanFiveColor.contractible_patch line 13

   Source documentation

   Patch a map across separated bad fibers. Only the intervening values need lie in a contractible subspace; the map is kept on one closed set and made constant on the other.

   theorem contractible_patch {X : Type u} {Y : Type v} [TopologicalSpace X]
       [TopologicalSpace Y] [NormalSpace X] (D : Set Y) [ContractibleSpace D]
       (f : C(X,Y)) {A B : Set X} (hA : IsClosed A) (hB : IsClosed B) (hd : Disjoint A B)
       (hg : ∀x,x∉A → x∉B → f x∈D) :
       ∃a : D, ∃g : C(X,Y), EqOn g (fun _ => a.val) A ∧ EqOn g f B ∧
         ∀x,g x=f x ∨ g x∈D := by
   …

2. def OAI.EuclideanFiveColor.crossingGraph line 105

   Source documentation

   Edges whose midpoint fibers contain a compact continuum joining the two boundaries.

   def crossingGraph {X : Type u} {V : Type v} [TopologicalSpace X]
       (f : X → V → ℝ) (A B : Set X) : SimpleGraph V where
   …

3. theorem OAI.EuclideanFiveColor.graph_forest_patch line 118

   Source documentation

   If the crossing edges form a forest, the boundary map can be patched to a constant on the inner closed set, unchanged on the outer closed set. This replaces the graph-word and winding detour for the existential interface-cycle producer.

   theorem graph_forest_patch {X : Type u} {V : Type v} [TopologicalSpace X]
       [CompactSpace X] [T2Space X] [Fintype V] [Nonempty V]
       (f : C(X,GraphSpace (⊤ : SimpleGraph V))) {A B : Set X}
       (hA : IsClosed A) (hB : IsClosed B) (hd : Disjoint A B)
       (hforest : (crossingGraph (fun x => (f x).val) A B).IsAcyclic) :
       ∃a : GraphSpace (⊤ : SimpleGraph V), ∃g : C(X,GraphSpace (⊤ : SimpleGraph V)),
         EqOn g (fun _ => a) A ∧ EqOn g f B := by
   …

   Mentions: OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.crossingGraph

4. def OAI.EuclideanFiveColor.planeAnnulus line 168
5. lemma OAI.EuclideanFiveColor.planeAnnulus_compact line 169
6. lemma OAI.EuclideanFiveColor.mem_planeAnnulus line 171
7. def OAI.EuclideanFiveColor.annulusInner line 173
8. def OAI.EuclideanFiveColor.annulusOuter line 174
9. lemma OAI.EuclideanFiveColor.sphere_mem_annulus line 175
10. theorem OAI.EuclideanFiveColor.annulus_forest_extension line 183

    Source documentation

    A forest crossing graph yields an actual extension of the outer boundary over its disk. This uses compact fiber separation and tree contraction, not graph words.

    theorem annulus_forest_extension {V : Type u} [Fintype V] [Nonempty V]
        {x : ℂ} {r R : ℝ} (hrR : r<R)
        (f : C(planeAnnulus x r R,GraphSpace (⊤ : SimpleGraph V)))
        (hforest : (crossingGraph (fun z => (f z).val) (annulusInner x r R) (annulusOuter x r R)).IsAcyclic) :
        ∃g : C(Metric.closedBall x R,GraphSpace (⊤ : SimpleGraph V)),
          ∀z : Metric.sphere x R,g ⟨z.val,Metric.sphere_subset_closedBall z.property⟩=
            f ⟨z.val,sphere_mem_annulus hrR.le z.property⟩ := by
    …

    Mentions: OAI.EuclideanFiveColor.planeAnnulus, OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.crossingGraph, OAI.EuclideanFiveColor.annulusInner, OAI.EuclideanFiveColor.annulusOuter, OAI.EuclideanFiveColor.sphere_mem_annulus

11. lemma OAI.EuclideanFiveColor.finite_centers_separation line 239
12. def OAI.EuclideanFiveColor.centerDisks line 245
13. lemma OAI.EuclideanFiveColor.mem_centerDisks line 246
14. lemma OAI.EuclideanFiveColor.centerDisks_sum line 248
15. lemma OAI.EuclideanFiveColor.centerDisks_disjoint line 251
16. lemma OAI.EuclideanFiveColor.mem_center_holes line 265
17. def OAI.EuclideanFiveColor.activeCenters line 274
18. lemma OAI.EuclideanFiveColor.HoleApprox.annulus_in_domain line 276
19. lemma OAI.EuclideanFiveColor.HoleApprox.outside_centers_in_domain line 296