OAI/Geometry/PlaneColoring/DiskExtension.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.EuclideanFiveColor.MarkedDisk line 9
2. def OAI.EuclideanFiveColor.MarkedDisk.ball line 14
3. def OAI.EuclideanFiveColor.MarkedDisk.closedBall line 15
4. def OAI.EuclideanFiveColor.MarkedDisk.noncoreCost line 16
5. def OAI.EuclideanFiveColor.MarkedDisk.Valid line 17
6. lemma OAI.EuclideanFiveColor.MarkedDisk.merge line 20
7. lemma OAI.EuclideanFiveColor.MarkedDisk.erased_pair_sum line 71
8. lemma OAI.EuclideanFiveColor.MarkedDisk.merge_sum_bound line 77
9. theorem OAI.EuclideanFiveColor.MarkedDisk.separate line 90

   Source documentation

   Finite disk merging with separate total and non-core radius budgets. Strict containment at merges, and the retained core witness, are both included.

   theorem separate (S : Finset MarkedDisk) {L : Set ℂ} (hS : ∀d∈S,d.Valid L)
       {η : ℝ} (hη : 0<η) : ∃T : Finset MarkedDisk,
         (∀d∈T,d.Valid L) ∧ (T : Set MarkedDisk).Pairwise (fun a b => Disjoint a.closedBall b.closedBall) ∧
         (∀d∈S,∃e∈T,d.ball⊆e.ball ∧ (d.core=true → e.core=true)) ∧
         (∑d∈T,d.radius)<(∑d∈S,d.radius)+η ∧
         (∑d∈T,d.noncoreCost)<(∑d∈S,d.noncoreCost)+η := by
   …

   Mentions: OAI.EuclideanFiveColor.MarkedDisk

10. lemma OAI.EuclideanFiveColor.cone_dist line 164
11. def OAI.EuclideanFiveColor.diskCone line 168
12. lemma OAI.EuclideanFiveColor.diskCone_surjective line 176
13. lemma OAI.EuclideanFiveColor.diskCone_fiber line 199
14. theorem OAI.EuclideanFiveColor.contractible_disk_extension line 224

    Source documentation

    A contraction genuinely extends arbitrary continuous sphere data across a disk.

    theorem contractible_disk_extension {Y : Type u} [TopologicalSpace Y] [ContractibleSpace Y]
        (c : ℂ) {r : ℝ} (hr : 0<r) (f : C(Metric.sphere c r,Y)) :
        ∃g : C(Metric.closedBall c r,Y), ∀z : Metric.sphere c r,
          g ⟨z.val,Metric.sphere_subset_closedBall z.property⟩=f z := by
    …

15. def OAI.EuclideanFiveColor.graphLeafMove line 258

    Source documentation

    Linear transfer of a leaf coordinate along its unique incident edge.

    def graphLeafMove {V : Type u} (v w : V) (t : ℝ) (p : V → ℝ) : V → ℝ :=
    …

16. lemma OAI.EuclideanFiveColor.continuous_graphLeafMove line 260
17. lemma OAI.EuclideanFiveColor.graphLeafMove_zero line 266
18. lemma OAI.EuclideanFiveColor.graphLeafMove_of_zero line 268
19. lemma OAI.EuclideanFiveColor.graphLeafMove_edge line 270
20. lemma OAI.EuclideanFiveColor.graphLeafMove_vertex line 278
21. lemma OAI.EuclideanFiveColor.graphLeafMove_mem line 281
22. lemma OAI.EuclideanFiveColor.graphLeafMove_one_at line 308
23. def OAI.EuclideanFiveColor.graphDrop line 312
24. def OAI.EuclideanFiveColor.graphLift line 314
25. lemma OAI.EuclideanFiveColor.continuous_graphDrop line 316
26. lemma OAI.EuclideanFiveColor.continuous_graphLift line 318
27. lemma OAI.EuclideanFiveColor.graphLift_drop line 324
28. lemma OAI.EuclideanFiveColor.graphDrop_lift line 330
29. lemma OAI.EuclideanFiveColor.graphDrop_vertex line 333
30. lemma OAI.EuclideanFiveColor.graphDrop_edge line 336
31. lemma OAI.EuclideanFiveColor.graphLift_vertex line 339
32. lemma OAI.EuclideanFiveColor.graphLift_edge line 345
33. lemma OAI.EuclideanFiveColor.graphLift_mem line 351
34. lemma OAI.EuclideanFiveColor.graphDrop_mem line 356
35. def OAI.EuclideanFiveColor.graphLeafRetraction line 388
36. def OAI.EuclideanFiveColor.graphLeafInclusion line 397
37. def OAI.EuclideanFiveColor.graphLeafHomotopy line 402
38. lemma OAI.EuclideanFiveColor.graphTree_contractible_aux line 416
39. theorem OAI.EuclideanFiveColor.graphTree_contractible line 457

    Source documentation

    Genuine contraction of the geometric probability-simplex realization of a finite tree.

    theorem graphTree_contractible {V : Type u} [Fintype V] {G : SimpleGraph V} (hG : G.IsTree) :
        ContractibleSpace (GraphSpace G) := graphTree_contractible_aux _ V G rfl hG
    …

    Mentions: OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.graphTree_contractible_aux

40. theorem OAI.EuclideanFiveColor.forest_disk_extension line 469

    Source documentation

    Forest-valued boundary data extend through an actual spanning tree inside the complete graph. Isolated labels and empty edge sets are retained.

    theorem forest_disk_extension {V : Type u} [Fintype V] [Nonempty V]
        (c : ℂ) {r : ℝ} (hr : 0<r) (f : C(Metric.sphere c r,V → ℝ))
        {G : SimpleGraph V} (hG : G.IsAcyclic) (hf : ∀z,f z∈graphRealization G) :
        ∃g : C(Metric.closedBall c r,GraphSpace (⊤ : SimpleGraph V)), ∀z : Metric.sphere c r,
          (g ⟨z.val,Metric.sphere_subset_closedBall z.property⟩).val=f z := by
    …

    Mentions: OAI.EuclideanFiveColor.graphRealization, OAI.EuclideanFiveColor.GraphSpace

41. def OAI.EuclideanFiveColor.closedCoverMap line 493

    Source documentation

    Finite closed-cover pasting, with the actual glued continuous map.

    def closedCoverMap {X : Type u} {Y : Type v} {ι : Type w}
        [TopologicalSpace X] [TopologicalSpace Y] [Finite ι]
        (S : ι → Set X) (hS : ∀i,IsClosed (S i)) (hc : ⋃i,S i=univ)
        (f : ∀i,C(S i,Y))
        (hf : ∀i j x (hi : x∈S i) (hj : x∈S j), f i ⟨x,hi⟩=f j ⟨x,hj⟩) : C(X,Y) where
    …

42. lemma OAI.EuclideanFiveColor.closedCoverMap_apply line 502
43. def OAI.EuclideanFiveColor.diskHoles line 518
44. def OAI.EuclideanFiveColor.coreHoles line 519
45. lemma OAI.EuclideanFiveColor.diskHoles_open line 520
46. lemma OAI.EuclideanFiveColor.coreHoles_open line 522
47. lemma OAI.EuclideanFiveColor.mem_diskHoles line 524
48. lemma OAI.EuclideanFiveColor.mem_coreHoles line 526
49. theorem OAI.EuclideanFiveColor.fill_noncore_disks line 532

    Source documentation

    Finite closed pasting fills precisely the non-core holes, with actual continuous tree extensions on their disks and no change outside the original open holes.

    theorem fill_noncore_disks {V : Type u} [Fintype V] [Nonempty V]
        (Q : Set ℂ) (S : Finset MarkedDisk) (hr : ∀d∈S,0<d.radius)
        (hdis : (S : Set MarkedDisk).Pairwise (fun a b => Disjoint a.closedBall b.closedBall))
        (f : C(ℂ,V → ℝ))
        (hg : ∀z∈Q,z∉diskHoles S → f z∈graphRealization (⊤ : SimpleGraph V))
        (hb : ∀d∈S,d.core=false → (d.closedBall∩Q).Nonempty →
          ∃G : SimpleGraph V,G.IsAcyclic ∧ ∀z∈Metric.sphere d.center d.radius,f z∈graphRealization G) :
        ∃g : C(↥(Q \ coreHoles S),GraphSpace (⊤ : SimpleGraph V)),
          ∀z : ↥(Q \ coreHoles S),z.val∉diskHoles S → (g z).val=f z.val := by
    …

    Mentions: OAI.EuclideanFiveColor.MarkedDisk, OAI.EuclideanFiveColor.diskHoles, OAI.EuclideanFiveColor.graphRealization, OAI.EuclideanFiveColor.coreHoles, OAI.EuclideanFiveColor.GraphSpace