PartitionGraph.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Partition graphs and their extended distances

An edge records equality of one selected label. Distances take values in ℕ∞, so vertices in different connected components have infinite distance. The pivot comparison and finite-walk characterization control the paths between vertices with common labels.

def OAI.MetricEntropyDuality.PartitionGraph.graph line 24
Source documentation
Distinct vertices are adjacent when a selected label agrees.
```
def graph : SimpleGraph X where
…
```
theorem OAI.MetricEntropyDuality.PartitionGraph.adj_iff line 35
def OAI.MetricEntropyDuality.PartitionGraph.distance line 39
Source documentation
The genuine extended shortest-path distance, including infinity.
```
def distance (x y : X) : ℕ∞ := (graph L T).edist x y
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.graph
def OAI.MetricEntropyDuality.PartitionGraph.near line 42
Source documentation
Membership in a closed graph ball of finite natural radius.
```
def near (k : ℕ) (x y : X) : Prop := distance L T x y ≤ (k : ℕ∞)
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.distance
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_self line 44
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_eq_zero_iff line 47
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_comm line 50
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_triangle line 53
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_eq_top_of_not_reachable line 57
theorem OAI.MetricEntropyDuality.PartitionGraph.near_zero_iff line 61
theorem OAI.MetricEntropyDuality.PartitionGraph.near_self line 64
theorem OAI.MetricEntropyDuality.PartitionGraph.near_symm line 67
theorem OAI.MetricEntropyDuality.PartitionGraph.near_mono line 73
theorem OAI.MetricEntropyDuality.PartitionGraph.near_triangle line 77
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_le_one_of_label_eq line 85
Source documentation
A label match gives distance at most one, including coincident vertices.
```
theorem distance_le_one_of_label_eq {i : ι} {x y : X}
    (hi : i ∈ T) (heq : L i x = L i y) : distance L T x y ≤ 1 := by
…
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.distance
theorem OAI.MetricEntropyDuality.PartitionGraph.near_one_of_label_eq line 93
theorem OAI.MetricEntropyDuality.PartitionGraph.exists_walk_of_le line 98
Source documentation
Every finite distance bound is witnessed by an actual walk.
```
theorem exists_walk_of_le {k : ℕ} {x y : X}
    (h : distance L T x y ≤ (k : ℕ∞)) :
    ∃ p : (graph L T).Walk x y, p.length ≤ k := by
…
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.PartitionGraph.graph
theorem OAI.MetricEntropyDuality.PartitionGraph.distance_le_iff_exists_walk line 106
theorem OAI.MetricEntropyDuality.PartitionGraph.near_iff_exists_walk line 114
theorem OAI.MetricEntropyDuality.PartitionGraph.lt_distance_of_forall_walk line 119
Source documentation
To separate vertices beyond radius k, it suffices to rule out short walks.
```
theorem lt_distance_of_forall_walk {k : ℕ} {x y : X}
    (h : ∀ p : (graph L T).Walk x y, k < p.length) :
    (k : ℕ∞) < distance L T x y := by
…
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.graph, OAI.MetricEntropyDuality.PartitionGraph.distance
theorem OAI.MetricEntropyDuality.PartitionGraph.pivot_replacement line 128
Source documentation
Replacing a pivot by a vertex with the same selected label costs one step.
```
theorem pivot_replacement {i : ι} {j : ℕ} {v z z' : X}
    (hi : i ∈ T) (heq : L i z' = L i z) (hvz : near L T j v z) :
    near L T (j + 1) v z' :=
…
```
Mentions: OAI.MetricEntropyDuality.PartitionGraph.near
theorem OAI.MetricEntropyDuality.PartitionGraph.pivot_forward line 133
theorem OAI.MetricEntropyDuality.PartitionGraph.pivot_backward line 139

theorem OAI.MetricEntropyDuality.PartitionGraph.pivot_comparison line 148

Source documentation

The replacement and the forward/backward comparisons for one fixed label.

theorem pivot_comparison {i : ι} {j : ℕ} {v z z' x : X}
    (hi : i ∈ T) (heq : L i z' = L i z) (hvz : near L T j v z) :
    near L T (j + 1) v z' ∧
      (near L T j x v → near L T (2 * j + 1) x z') ∧
      (near L T (2 * j + 1) x z' → near L T (3 * j + 2) x v) :=
…

Mentions: OAI.MetricEntropyDuality.PartitionGraph.near