FullApproximation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.EuclideanFiveColor.eventually_forest_of_bridges line 12

Source documentation

Compactness and the angular theorems force all sufficiently fine crossing graphs to be forests. This is about actual compact bridges, not assumed interface data.

theorem eventually_forest_of_bridges {c : ℂ → Fin 5} (hc : Measurable c)
    (hw : WeakColoring 5 c) {x : ℂ} {ρ : ℝ} (hρ : 0<ρ)
    (D : ℕ → SimpleGraph (Fin 5)) {r ε : ℕ → ℝ}
    (hr : Tendsto r atTop (𝓝 0)) (hε : Tendsto ε atTop (𝓝 0)) (hpos : ∀n,0<ε n)
    {H E : ℕ → Set ℂ} (hE : Tendsto (fun n => volume (E n)) atTop (𝓝 0))
    (hnear : ∀n z q,q∈H n → dist z q=1 → z∈E n)
    {α : ℝ} (hα : 0<α)
    (hbridge : ∀n i j,(D n).Adj i j → ∃K : NonemptyCompacts ℂ,
      (K : Set ℂ)⊆Metric.closedBall x ρ ∧ IsPreconnected (K : Set ℂ) ∧
      (∃a∈K,dist a x≤r n) ∧ ((K : Set ℂ)∩Metric.sphere x ρ).Nonempty ∧
      (∀q∈K,q∉H n → α<diskAverage c (ε n) i q) ∧
      (∀q∈K,q∉H n → α<diskAverage c (ε n) j q)) :
…

Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.diskAverage

lemma OAI.EuclideanFiveColor.midpoint_threshold_labels line 52

theorem OAI.EuclideanFiveColor.annulus_maps_eventually_forest line 64

Source documentation

The actual continuous annulus maps eventually permit disk extensions.

theorem annulus_maps_eventually_forest {c : ℂ → Fin 5} (hc : Measurable c)
    (hw : WeakColoring 5 c) {x : ℂ} {R : ℝ} (hR : 0<R) {r ε : ℕ → ℝ}
    (hr : Tendsto r atTop (𝓝 0)) (hε : Tendsto ε atTop (𝓝 0)) (hpos : ∀n,0<ε n)
    {H E : ℕ → Set ℂ} (hE : Tendsto (fun n => volume (E n)) atTop (𝓝 0))
    (hnear : ∀n z q,q∈H n → dist z q=1 → z∈E n)
    {α : ℝ} (hα : 0<α) (hα' : α<1/5)
    (f : ∀n,C(planeAnnulus x (r n) R,GraphSpace (⊤ : SimpleGraph (Fin 5))))
    (hf : ∀n z,z.val∉H n → (f n z).val=thresholdMap c (ε n) α z.val) :
    ∀ᶠ n in atTop,(crossingGraph (fun z => (f n z).val)
      (annulusInner x (r n) R) (annulusOuter x (r n) R)).IsAcyclic := by
…

Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.planeAnnulus, OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.thresholdMap, OAI.EuclideanFiveColor.crossingGraph, OAI.EuclideanFiveColor.annulusInner, OAI.EuclideanFiveColor.annulusOuter

theorem OAI.EuclideanFiveColor.finite_disk_paste line 107

Source documentation

Actual finite disk pasting from a closed outside domain. Disks may cross the boundary of the ambient compact region.

theorem finite_disk_paste {Y : Type u} [TopologicalSpace Y] (Q : Set ℂ)
    (S : Finset MarkedDisk)
    (hdis : (S : Set MarkedDisk).Pairwise (fun a b => Disjoint a.closedBall b.closedBall))
    (f : C(↥(Q \ diskHoles S),Y))
    (g : ∀d : S,C(d.val.closedBall,Y))
    (hb : ∀d : S,∀z : Metric.sphere d.val.center d.val.radius,∀hzQ : z.val∈Q,
      ∀hzS : z.val∉diskHoles S,
      g d ⟨z.val,Metric.sphere_subset_closedBall z.property⟩=f ⟨z.val,hzQ,hzS⟩) :
    ∃F : C(Q,Y),∀z : Q,∀hz : z.val∉diskHoles S,F z=f ⟨z.val,z.property,hz⟩ := by
…

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

def OAI.EuclideanFiveColor.HoleApprox.annulusMap line 167

theorem OAI.EuclideanFiveColor.HoleApprox.fill_cores line 175

Source documentation

Fill all the actual core holes simultaneously when their surrounding crossing graphs are forests, retaining the threshold map outside the original and outer disks.

theorem fill_cores {c : ℂ → Fin 5} {α t R : ℝ} {L : Finset ℂ}
    (a : HoleApprox c α L t) (hR : R<1) (htR : 2*t<R)
    (hsep : ∀x∈L,∀y∈L,x≠y → 2*R<dist x y)
    (hforest : ∀x (hx : x∈activeCenters L),
      (crossingGraph (fun z => (a.annulusMap hR htR hsep hx z).val)
        (annulusInner x (2*t) R) (annulusOuter x (2*t) R)).IsAcyclic) :
    ∃F : C(Metric.closedBall (0:ℂ) 5,GraphSpace (⊤ : SimpleGraph (Fin 5))),
      ∀z : Metric.closedBall (0:ℂ) 5,z.val∉diskHoles a.disks →
        z.val∉diskHoles (centerDisks (activeCenters L) R) →
        (F z).val=thresholdMap c a.ε α z.val := by
…

Mentions: OAI.EuclideanFiveColor.HoleApprox, OAI.EuclideanFiveColor.activeCenters, OAI.EuclideanFiveColor.crossingGraph, OAI.EuclideanFiveColor.annulusInner, OAI.EuclideanFiveColor.annulusOuter, OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.diskHoles, OAI.EuclideanFiveColor.centerDisks, OAI.EuclideanFiveColor.thresholdMap

theorem OAI.EuclideanFiveColor.HoleApprox.eventually_fill_cores line 206

Source documentation

The common-exclusion limit contradiction applies to the constructed maps, so all these actual core fillings exist eventually at any fixed separated outer scale.

theorem eventually_fill_cores {c : ℂ → Fin 5} (hc : Measurable c) (hw : WeakColoring 5 c)
    {α R : ℝ} (hα : 0<α) (hα' : α<1/5) {L : Finset ℂ} {t : ℕ → ℝ}
    (a : ∀n,HoleApprox c α L (t n)) (ht : Tendsto t atTop (𝓝 0))
    (hR0 : 0<R) (hR : R<1) (htR : ∀n,2*t n<R)
    (hsep : ∀x∈L,∀y∈L,x≠y → 2*R<dist x y) :
    ∀ᶠ n in atTop,∃F : C(Metric.closedBall (0:ℂ) 5,GraphSpace (⊤ : SimpleGraph (Fin 5))),
      ∀z : Metric.closedBall (0:ℂ) 5,z.val∉diskHoles (a n).disks →
        z.val∉diskHoles (centerDisks (activeCenters L) R) →
        (F z).val=thresholdMap c (a n).ε α z.val := by
…

Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.HoleApprox, OAI.EuclideanFiveColor.GraphSpace, OAI.EuclideanFiveColor.diskHoles, OAI.EuclideanFiveColor.centerDisks, OAI.EuclideanFiveColor.activeCenters, OAI.EuclideanFiveColor.thresholdMap

lemma OAI.EuclideanFiveColor.diskHoles_union line 236
lemma OAI.EuclideanFiveColor.disk_radius_sum_union_le line 240
structure OAI.EuclideanFiveColor.FullApprox line 255
Source documentation
A global graph approximation, with actual small exceptional disks. All fields will be constructed, not postulated as coloring hypotheses.
```
structure FullApprox (c : ℂ → Fin 5) (α t : ℝ) where
…
```
theorem OAI.EuclideanFiveColor.fullApprox_exists_of_finite_core line 268
Source documentation
The whole producer, using actual annular crossing fibers and all angular contradictions: global graph approximants exist at arbitrarily small exception scales.
```
theorem fullApprox_exists_of_finite_core {c : ℂ → Fin 5} (hc : Measurable c)
    (hw : WeakColoring 5 c) {α : ℝ} (hα : 0<α) (hα' : α<1/5)
    (L : Finset ℂ) (hL : ∀x∈Metric.closedBall (0:ℂ) 8,¬(transitionGraph c x).IsAcyclic → x∈L)
    {t : ℝ} (ht : 0<t) : Nonempty (FullApprox c α t) := by
…
```
Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.transitionGraph, OAI.EuclideanFiveColor.FullApprox
theorem OAI.EuclideanFiveColor.fullApprox_exists line 330
Source documentation
The finite core used above is obtained from the proved actual transition core local-finiteness theorem; no regularity of the original coloring is added.
```
theorem fullApprox_exists {c : ℂ → Fin 5} (hc : Measurable c)
    (hw : WeakColoring 5 c) {α : ℝ} (hα : 0<α) (hα' : α<1/5) {t : ℝ} (ht : 0<t) :
    Nonempty (FullApprox c α t) := by
…
```
Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.FullApprox