ContinuumLimits.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.EuclideanFiveColor.ae_frequently_notMem_of_measure_tendsto_zero line 12
Source documentation
Vanishing exceptional measure is enough: almost every point is outside the exceptional sets infinitely often. No summability or nesting is required.
```
lemma ae_frequently_notMem_of_measure_tendsto_zero {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {E : ℕ → Set X}
    (hE : Tendsto (fun n => μ (E n)) atTop (𝓝 0)) :
    ∀ᵐ z ∂μ, ∃ᶠ n in atTop, z ∉ E n := by
…
```

lemma OAI.EuclideanFiveColor.ae_ne_one_of_eventual_bound line 32

Source documentation

Pointwise differentiation plus vanishing exceptional sets gives the measure exclusion used for both the mesh bound and the common continuum exclusions.

lemma ae_ne_one_of_eventual_bound {X : Type*} [MeasurableSpace X]
    {μ : Measure X} {p : ℕ → X → ℝ} {f : X → ℝ} {E : ℕ → Set X} {U : Set X}
    {α : ℝ} (hα : 0 < α)
    (hp : ∀ᵐ z ∂μ, Tendsto (fun n => p n z) atTop (𝓝 (f z)))
    (hE : Tendsto (fun n => μ (E n)) atTop (𝓝 0))
    (hb : ∀ z ∈ U, ∀ᶠ n in atTop, z ∉ E n → p n z ≤ 1-α) :
    ∀ᵐ z ∂μ, z ∈ U → f z ≠ 1 := by
…

lemma OAI.EuclideanFiveColor.colorFn_locallyIntegrable line 51
lemma OAI.EuclideanFiveColor.diskAverage_eq_average_ball line 56
lemma OAI.EuclideanFiveColor.complex_ball_ae_closedBall line 67
lemma OAI.EuclideanFiveColor.diskAverage_ae_tendsto line 72
lemma OAI.EuclideanFiveColor.support_disjoint_open_of_ae line 86
lemma OAI.EuclideanFiveColor.diskAverage_support_exclusion line 98

theorem OAI.EuclideanFiveColor.nonemptyCompacts_preconnected_limit line 117

Source documentation

Connectedness passes to a Vietoris (equivalently compact Hausdorff metric) limit.

theorem nonemptyCompacts_preconnected_limit {X : Type u} [TopologicalSpace X]
    [T2Space X] [NormalSpace X] {ι : Type v} {l : Filter ι} [NeBot l]
    {K : ι → NonemptyCompacts X} {L : NonemptyCompacts X}
    (hlim : Tendsto K l (𝓝 L)) (hc : ∀ᶠn in l,IsPreconnected (K n : Set X)) :
    IsPreconnected (L : Set X) := by
…

lemma OAI.EuclideanFiveColor.nonemptyCompacts_mem_limit line 142
lemma OAI.EuclideanFiveColor.nonemptyCompacts_inter_closed_limit line 154

theorem OAI.EuclideanFiveColor.finite_continuum_subsequence line 163

Source documentation

A finite family of nonempty compact continua in a compact metric space has one common subsequence of connected compact limits.

theorem finite_continuum_subsequence {X : Type u} [MetricSpace X] [CompactSpace X]
    {J : Type v} [Finite J] (K : ℕ → J → NonemptyCompacts X)
    (hc : ∀n j,IsPreconnected (K n j : Set X)) :
    ∃L : J → NonemptyCompacts X, ∃φ : ℕ → ℕ, StrictMono φ ∧
      (∀j,Tendsto (fun n => K (φ n) j) atTop (𝓝 (L j))) ∧
      (∀j,IsPreconnected (L j : Set X)) := by
…

lemma OAI.EuclideanFiveColor.straddle_eventually_of_compact_limit line 184

theorem OAI.EuclideanFiveColor.continuum_limit_support_exclusion line 200

Source documentation

The common-exclusion continuum limit argument. The sole exceptional sets are actual unit neighborhoods of the holes, and their measures tend to zero.

theorem continuum_limit_support_exclusion {k : ℕ} {c : ℂ → Fin k}
    (hc : Measurable c) (hw : WeakColoring k c)
    {K : ℕ → NonemptyCompacts ℂ} {L : NonemptyCompacts ℂ}
    (hlim : Tendsto K atTop (𝓝 L)) (hconn : ∀n,IsPreconnected (K n : Set ℂ))
    {ε : ℕ → ℝ} (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<α) (i : Fin k)
    (hprob : ∀n q,q∈K n → q∉H n → α<diskAverage c (ε n) i q) :
    Disjoint (spatialSupport c i) (Straddle (L : Set ℂ)) := by
…

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

def OAI.EuclideanFiveColor.CommonInterface line 228
Source documentation
One interface excludes both labels from the same straddling set and approaches its center in an actual unit direction.
```
def CommonInterface (c : ℂ → Fin 5) (x : ℂ) (i j : Fin 5) : Prop :=
…
```
lemma OAI.EuclideanFiveColor.CommonInterface.symm line 231
lemma OAI.EuclideanFiveColor.spatialSupport_perm line 235
lemma OAI.EuclideanFiveColor.CommonInterface.perm line 241
lemma OAI.EuclideanFiveColor.commonInterface_of_continuum line 246
lemma OAI.EuclideanFiveColor.no_triangle_commonInterface line 252
lemma OAI.EuclideanFiveColor.no_four_commonInterface line 270
lemma OAI.EuclideanFiveColor.no_five_commonInterface line 290
theorem OAI.EuclideanFiveColor.commonInterface_graph_acyclic line 296
Source documentation
All actual common-exclusion interfaces at a point form a forest. This assembles triangle, four and five cases for arbitrary labels, not just canonical cycles.
```
theorem commonInterface_graph_acyclic {c : ℂ → Fin 5} (hc : Measurable c)
    (hw : WeakColoring 5 c) (x : ℂ) (G : SimpleGraph (Fin 5))
    (hG : ∀i j,G.Adj i j → CommonInterface c x i j) : G.IsAcyclic := by
…
```
Mentions: OAI.EuclideanFiveColor.WeakColoring, OAI.EuclideanFiveColor.CommonInterface

theorem OAI.EuclideanFiveColor.commonInterface_of_compact_sequence line 318

Source documentation

End-to-end limit of actual connected midpoint fibers, retaining both endpoint exclusions on the same limiting continuum.

theorem commonInterface_of_compact_sequence {c : ℂ → Fin 5}
    (hc : Measurable c) (hw : WeakColoring 5 c) {x : ℂ} {ρ : ℝ} (hρ : 0<ρ)
    (K : ℕ → NonemptyCompacts ℂ) (hsub : ∀n,(K n : Set ℂ)⊆Metric.closedBall x ρ)
    (hconn : ∀n,IsPreconnected (K n : Set ℂ))
    (a : ℕ → ℂ) (ha : ∀n,a n∈K n) (halim : Tendsto a atTop (𝓝 x))
    (hout : ∀n,((K n : Set ℂ)∩Metric.sphere x ρ).Nonempty)
    {ε : ℕ → ℝ} (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<α) (i j : Fin 5)
    (hi : ∀n q,q∈K n → q∉H n → α<diskAverage c (ε n) i q)
    (hj : ∀n q,q∈K n → q∉H n → α<diskAverage c (ε n) j q) :
…

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