GraphRealization.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.EuclideanFiveColor.continuum_has_approach line 11
Source documentation
The directional subsequence in the last paragraph of interface-cycle follows from connectedness and an outer contact. Compactness of the continuum is not needed.
```
lemma continuum_has_approach {x y : ℂ} {K : Set ℂ} (hK : IsPreconnected K)
    (hx : x∈K) (hy : y∈K) (hne : y≠x) :
    ∃v : ℂ, ‖v‖=1 ∧ Nonempty (ApproachingContinuum x K v) := by
…
```
Mentions: OAI.EuclideanFiveColor.ApproachingContinuum

lemma OAI.EuclideanFiveColor.compact_component_partition line 55

Source documentation

The compact contact partition used in the manuscript's annular-crossing proof. This reuses Mathlib's Hausdorff component quotient and its profinite separation theorem.

lemma compact_component_partition {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    {I O : Set X} (hI : IsCompact I) (hO : IsCompact O)
    (hno : ∀x∈I, Disjoint (connectedComponent x) O) :
    ∃Z₁ Z₂ : Set X, IsCompact Z₁ ∧ IsCompact Z₂ ∧ Disjoint Z₁ Z₂ ∧
      Z₁∪Z₂=univ ∧ I⊆Z₁ ∧ O⊆Z₂ := by
…

def OAI.EuclideanFiveColor.graphVertex line 87
Source documentation
Standard affine vertices. These are the manuscript's probability-simplex coordinates.
```
def graphVertex {V : Type u} (i : V) : V → ℝ := fun j => if j=i then 1 else 0
```
def OAI.EuclideanFiveColor.graphEdgePoint line 89
Source documentation
Affine parameterization of an edge, including its two vertices.
```
def graphEdgePoint {V : Type u} (i j : V) (t : ℝ) : V → ℝ :=
…
```
def OAI.EuclideanFiveColor.graphRealization line 93
Source documentation
The geometric realization of a simple graph in its probability simplex. The equal-endpoint option includes isolated vertices.
```
def graphRealization {V : Type u} (G : SimpleGraph V) : Set (V → ℝ) :=
…
```
abbrev OAI.EuclideanFiveColor.GraphSpace line 95
lemma OAI.EuclideanFiveColor.graphEdgePoint_apply line 96
lemma OAI.EuclideanFiveColor.graphEdgePoint_zero line 98
lemma OAI.EuclideanFiveColor.graphEdgePoint_one line 100
lemma OAI.EuclideanFiveColor.graphEdgePoint_self line 102
lemma OAI.EuclideanFiveColor.graphEdgePoint_swap line 104
lemma OAI.EuclideanFiveColor.continuous_graphEdgePoint line 107
lemma OAI.EuclideanFiveColor.graphVertex_mem line 110
lemma OAI.EuclideanFiveColor.graphEdgePoint_mem line 112
lemma OAI.EuclideanFiveColor.graphRealization_mono line 115
lemma OAI.EuclideanFiveColor.graphRealization_nonneg line 119
lemma OAI.EuclideanFiveColor.graphRealization_sum line 124
lemma OAI.EuclideanFiveColor.graphRealization_compact line 128
lemma OAI.EuclideanFiveColor.graphRealization_closed line 140
instance OAI.EuclideanFiveColor.graphSpace_compact line 142
lemma OAI.EuclideanFiveColor.graphRealization_singleton line 144
lemma OAI.EuclideanFiveColor.graphRealization_of_two_support line 160
theorem OAI.EuclideanFiveColor.simplex_mem_forest line 194
Source documentation
A simplex vector whose positive labels form a clique in a forest is genuinely in that forest's affine realization, rather than just in the complete graph.
```
theorem simplex_mem_forest {V : Type u} [Fintype V] {G : SimpleGraph V}
    (hG : G.IsAcyclic) {p : V → ℝ} (hn : ∀i,0≤p i) (hs : ∑i,p i=1)
    (hcl : ∀i j,i≠j → 0<p i → 0<p j → G.Adj i j) : p∈graphRealization G := by
…
```
Mentions: OAI.EuclideanFiveColor.graphRealization
def OAI.EuclideanFiveColor.thresholdWeight line 243
Source documentation
The manuscript's thresholded and renormalized disk average (equation 22).
```
def thresholdWeight (c : ℂ → Fin 5) (ε α : ℝ) (q : ℂ) (i : Fin 5) : ℝ :=
…
```
def OAI.EuclideanFiveColor.thresholdTotal line 245
def OAI.EuclideanFiveColor.thresholdMap line 247
lemma OAI.EuclideanFiveColor.thresholdTotal_pos line 249
lemma OAI.EuclideanFiveColor.thresholdMap_nonneg line 257
lemma OAI.EuclideanFiveColor.thresholdMap_sum line 260
lemma OAI.EuclideanFiveColor.thresholdMap_pos line 265
lemma OAI.EuclideanFiveColor.continuous_thresholdMap line 270
lemma OAI.EuclideanFiveColor.thresholdMap_mem_forest line 276
lemma OAI.EuclideanFiveColor.finite_pos_lt line 290
lemma OAI.EuclideanFiveColor.finite_small_scale line 298

theorem OAI.EuclideanFiveColor.forest_chart line 306

Source documentation

A genuine local forest chart; its exception disks have arbitrarily small total radius at sufficiently small averaging scale.

theorem forest_chart {c : ℂ → Fin 5} (hc : Measurable c) {α : ℝ}
    (hα : 0<α) (hα' : α<1/5) (x : ℂ) (hf : (transitionGraph c x).IsAcyclic) :
    ∃s>0,∀η>0,∃δ>0,∀ε,0<ε → ε<δ → ∃C : Finset ℂ,
      (C.card:ℝ)*(α*ε/4)<η ∧ ∀q∈Metric.ball x s,
      q∉⋃z∈C,Metric.ball z (α*ε/4) → thresholdMap c ε α q∈graphRealization (transitionGraph c x) := by
…

Mentions: OAI.EuclideanFiveColor.transitionGraph, OAI.EuclideanFiveColor.thresholdMap, OAI.EuclideanFiveColor.graphRealization

theorem OAI.EuclideanFiveColor.compact_forest_charts line 367

Source documentation

Compact local forest control with one Lebesgue radius, chosen before the hole budget and the disk-average scale. The resulting forest controls the WHOLE nearby ball off the common exception disks, not merely the compact set.

theorem compact_forest_charts {c : ℂ → Fin 5} (hc : Measurable c) {α : ℝ}
    (hα : 0<α) (hα' : α<1/5) (M : Set ℂ) (hM : IsCompact M)
    (hf : ∀x∈M,(transitionGraph c x).IsAcyclic) :
    ∃l>0,∀η>0,∃δ>0,∀ε,0<ε → ε<δ → ∃C : Finset ℂ,
      (C.card:ℝ)*(α*ε/4)<η ∧ ∀a∈M,∃G : SimpleGraph (Fin 5),G.IsAcyclic ∧
      ∀q∈Metric.ball a l,q∉⋃z∈C,Metric.ball z (α*ε/4) → thresholdMap c ε α q∈graphRealization G := by
…

Mentions: OAI.EuclideanFiveColor.transitionGraph, OAI.EuclideanFiveColor.thresholdMap, OAI.EuclideanFiveColor.graphRealization