OAI/Geometry/PlaneColoring/HoleApproximation.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanFiveColor.MarkedDisk.radius_le_sum line 10
2. lemma OAI.EuclideanFiveColor.MarkedDisk.noncoreCost_nonneg line 12
3. lemma OAI.EuclideanFiveColor.MarkedDisk.noncore_radius_le_sum line 15
4. lemma OAI.EuclideanFiveColor.MarkedDisk.sphere_avoids_holes line 19
5. lemma OAI.EuclideanFiveColor.MarkedDisk.closedBall_near_core line 31
6. lemma OAI.EuclideanFiveColor.MarkedDisk.sphere_norm_bound line 37
7. def OAI.EuclideanFiveColor.MarkedDisk.initialDisks line 57
8. lemma OAI.EuclideanFiveColor.MarkedDisk.mem_initialDisks line 59
9. lemma OAI.EuclideanFiveColor.MarkedDisk.initialDisks_valid line 62
10. lemma OAI.EuclideanFiveColor.MarkedDisk.initialDisks_sum line 68
11. lemma OAI.EuclideanFiveColor.MarkedDisk.initial_core_cover line 85
12. lemma OAI.EuclideanFiveColor.MarkedDisk.initial_marked_cover line 88
13. lemma OAI.EuclideanFiveColor.MarkedDisk.holes_subset_of_cover line 91
14. theorem OAI.EuclideanFiveColor.small_hole_map line 115

    Source documentation

    Actual small-hole maps on a fixed disk, with arbitrarily small total radii. The core witnesses lie in the finite actual cyclic core; all other holes have been filled by genuine tree extensions.

    theorem small_hole_map {c : ℂ → Fin 5} (hc : Measurable c) {α : ℝ}
        (hα : 0<α) (hα' : α<1/5) (L : Finset ℂ)
        (hL : ∀x∈Metric.closedBall (0:ℂ) 8,¬(transitionGraph c x).IsAcyclic → x∈L)
        {t : ℝ} (ht : 0<t) (ht' : t<1/2) :
        ∃e>0,∀ε,0<ε → ε<e → ∃S : Finset MarkedDisk,
          (∀d∈S,d.Valid (L : Set ℂ)) ∧
          (S : Set MarkedDisk).Pairwise (fun a b => Disjoint a.closedBall b.closedBall) ∧
          (∑d∈S,d.radius)<t ∧
          ∃g : C(↥(Metric.closedBall (0:ℂ) 7 \ coreHoles S),GraphSpace (⊤ : SimpleGraph (Fin 5))),
            ∀z : ↥(Metric.closedBall (0:ℂ) 7 \ coreHoles S),z.val∉diskHoles S →
              (g z).val=thresholdMap c ε α z.val := by
    …

    Mentions: OAI.EuclideanFiveColor.transitionGraph, OAI.EuclideanFiveColor.MarkedDisk, OAI.EuclideanFiveColor.coreHoles, OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.diskHoles, OAI.EuclideanFiveColor.thresholdMap

15. def OAI.EuclideanFiveColor.diskAnnulus line 211

    Source documentation

    Exception annuli for exact unit distances from the small closed disks.

    def diskAnnulus (d : MarkedDisk) : Set ℂ :=
    …

    Mentions: OAI.EuclideanFiveColor.MarkedDisk

16. def OAI.EuclideanFiveColor.holeAnnuli line 213
17. lemma OAI.EuclideanFiveColor.diskAnnulus_measurable line 214
18. lemma OAI.EuclideanFiveColor.unit_from_disk_mem_annulus line 216
19. lemma OAI.EuclideanFiveColor.volume_diskAnnulus line 226
20. lemma OAI.EuclideanFiveColor.volume_holeAnnuli_le line 240
21. lemma OAI.EuclideanFiveColor.unit_from_hole_mem_annuli line 252
22. lemma OAI.EuclideanFiveColor.holeAnnuli_tendsto_zero line 256
23. structure OAI.EuclideanFiveColor.HoleApprox line 280

    Source documentation

    Data actually constructed by the small-hole lemma.

    structure HoleApprox (c : ℂ → Fin 5) (α : ℝ) (L : Finset ℂ) (t : ℝ) where
    …

24. lemma OAI.EuclideanFiveColor.holeApprox_exists line 291
25. lemma OAI.EuclideanFiveColor.HoleApprox.cores_near line 303
26. lemma OAI.EuclideanFiveColor.HoleApprox.ε_tendsto line 311
27. lemma OAI.EuclideanFiveColor.HoleApprox.sum_tendsto line 315
28. lemma OAI.EuclideanFiveColor.HoleApprox.annuli_tendsto line 320