OAI/Geometry/PlaneColoring/Mesh.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.EuclideanFiveColor.connected_escape_holes line 12

   Source documentation

   A point of a connected set with a distant partner can be moved to the boundary of its (unique) small hole. Pairwise disjoint closed disks make the new point lie outside every open hole. No path regularity is required.

   lemma connected_escape_holes {S : Finset MarkedDisk} {t : ℝ}
       (hS : ∀d∈S,0≤d.radius)
       (hdis : (S : Set MarkedDisk).Pairwise (fun a b => Disjoint a.closedBall b.closedBall))
       (hsum : (∑d∈S,d.radius)<t) {K : Set ℂ} (hK : IsPreconnected K)
       {a b : ℂ} (ha : a∈K) (hb : b∈K) (hab : 2*t<dist a b) :
       ∃a'∈K,a'∉diskHoles S ∧ dist a a'≤2*t := by
   …

   Mentions: OAI.EuclideanFiveColor.MarkedDisk, OAI.EuclideanFiveColor.diskHoles

2. lemma OAI.EuclideanFiveColor.support_of_positive_diskAverage_limit line 39

   Source documentation

   Positive averages on shrinking disks force every limit center into the actual measure support of that color.

   lemma support_of_positive_diskAverage_limit {k : ℕ} {c : ℂ → Fin k} (hc : Measurable c)
       {ε : ℕ → ℝ} (hε : Tendsto ε atTop (𝓝 0)) {a : ℕ → ℂ} {x : ℂ}
       (ha : Tendsto a atTop (𝓝 x)) (i : Fin k)
       (hp : ∀n,0<diskAverage c (ε n) i (a n)) : x∈spatialSupport c i := by
   …

   Mentions: OAI.EuclideanFiveColor.diskAverage, OAI.EuclideanFiveColor.spatialSupport

3. lemma OAI.EuclideanFiveColor.FullApprox.ε_tendsto line 73
4. lemma OAI.EuclideanFiveColor.FullApprox.annuli_tendsto line 77
5. lemma OAI.EuclideanFiveColor.FullApprox.positive_average line 83
6. theorem OAI.EuclideanFiveColor.FullApprox.no_large_positive_sequence line 92

   Source documentation

   A continuous graph approximant cannot have positive-coordinate connected sets of macroscopic diameter at every shrinking scale. This is the manuscript mesh argument, with connectedness replacing the stronger path assumption.

   theorem no_large_positive_sequence {c : ℂ → Fin 5} (hc : Measurable c) (hw : WeakColoring 5 c)
       {α : ℝ} (hα : 0<α) (hα' : α<1/5) {t : ℕ → ℝ}
       (F : ∀n,FullApprox c α (t n)) (htlim : Tendsto t atTop (𝓝 0))
       (htsmall : ∀n,t n≤1/16) (i : Fin 5)
       (hbad : ∀n,∃K : Set ℂ, IsPreconnected K ∧ K⊆Metric.closedBall (0:ℂ) 5 ∧
         (∀z : Metric.closedBall (0:ℂ) 5,z.val∈K → 0<((F n).map z).val i) ∧
         ∃x∈K,∃y∈K,2<dist x y) : False := by
   …

   Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.FullApprox