Code for studying infinite rooted trees

Stream: Is there code for X?

[Abraham Solomon]

Hey all,

I have been trying to define some results for infinite rooted trees, I have some vague ideas of how to do it -- but curious if something already exists.

My goal is to define for an infinite rooted tree $T$ the notion of a cutset $\Pi \subset T$ -- a finite subset of vertices such that every infinite path from the root has a non-empty intersection with $\Pi$.

I can define an infinite graph that's a tree, and currently working to adapt Mathlib.Combinatorics.SimpleGraph.Path to the infinite setting.

A very rough sketch is something like this(assuming the tree has no leaves other than the root):

import Mathlib.Combinatorics.SimpleGraph.Path

variable {V : Type u} (G : SimpleGraph V)

def IsAcyclic : Prop := ∀ ⦃v : V⦄ (c : G.Walk v v), ¬c.IsCycle

inductive Infinite_Walk : V → Type u
  | nil {u : V} : Infinite_Walk u
  | cons {u v: V} (h : G.Adj u v) (p : Infinite_Walk u) : Infinite_Walk v


def IsCutset (T: SimpleGraph V)(S: T.Subgraph)(h₁: T.Connected ∧  IsAcyclic T) (root : V): Prop :=
 ∀ c : Infinite_Walk T root, ∃(k : S.verts), (k ∈ c)

Of course, to check membership is probably hard and requires some interoperability with finite paths. Does anyone know of anything like this?

The cardinality of all (unique) infinite paths is unfortunately often equal to the continuum, so there are complexities arising with that already; not to mention various other issues. But the above is just a rough idea.

[Yaël Dillies]

@Daniel Weber successfully implemented rooted trees as archimedean pred-orders (docs#PredOrder, docs#IsPredArchimedean). Could you reuse this idea?

[Nir Paz]

I'm not too familiar with these notions, is a tree with uncountable height an archimedean pred order? In set theory every ordinal is a tree (although I'm not sure if that's what @Abraham Solomon is going for here).

[Nir Paz]

Actually that's not a simple graph, so doesn't match the definition above

[Abraham Solomon]

Nir Paz said:

I'm not too familiar with these notions, is a tree with uncountable height an archimedean pred order? In set theory every ordinal is a tree (although I'm not sure if that's what Abraham Solomon is going for here).

I think that's the set theory type tree, which is connected to graph theory / rooted trees via Hasse diagrams -- but i want to be able to access the 'nth' level of an infinite walk.

Essentially, from the root, there exist degree(root) infinite paths at first (rays isomorphic to $\mathbb{N}$ with some darts(assume locally finite tree so degrees are all finite)).

Then, every time there is another child (since there are no leaves) this creates more rays inductively.

The easiest notion of cutset(s) for a tree $T$ with root $\rho$ are the level sets $S_{n} := \{ v \in T | |v| = n\}$ -- $|\cdot|$ the graph distance from the root. If a tree $T$ is spherically symmetric ( something like the degree of $v \in T$ depends only on $|v|$) these are often all you need in practice not to lose generality.

Eventually, such notions allow the categorisation of all locally finite trees by their 'exponents', with more information for spherically symmetric trees. For example, for the perfect rooted infinite binary tree -- an exponent known as the branching number is 2; for d-ary trees this is d.

[Abraham Solomon]

Yaël Dillies said:

Daniel Weber successfully implemented rooted trees as archimedean pred-orders (docs#PredOrder, docs#IsPredArchimedean). Could you reuse this idea?

I think this could be similar to what i wanted, thanks!

I think the way it would be defined for me is for two vertices $v,w \in T$, $v \leq w$ if both are on an infinite path together and $|v| \leq |w|$.

[Daniel Weber]

Nir Paz said:

I'm not too familiar with these notions, is a tree with uncountable height an archimedean pred order? In set theory every ordinal is a tree (although I'm not sure if that's what Abraham Solomon is going for here).

No, archimedeaness implies height $\omega$. A set theoretic tree is a partial order where every docs#Set.Iio is a well order, and then you can define the distance with docs#Ordinal.type (perhaps you can even relax the IsWellOrder in docs#Ordinal.typein to make it be the distance directly)

[Daniel Weber]

Abraham Solomon said:

Yaël Dillies said:

Daniel Weber successfully implemented rooted trees as archimedean pred-orders (docs#PredOrder, docs#IsPredArchimedean). Could you reuse this idea?

I think this could be similar to what i wanted, thanks!

I think the way it would be defined for me is for two vertices $v,w \in T$, $v \leq w$ if both are on an infinite path together and $|v| \leq |w|$.

Maybe I misunderstand what you want to do, but can't you directly use docs#RootedTree and then define $\left| \cdot \right|$ as Nat.find (bot_le (a := r)).exists_pred_iterate (this is also part of the definition of docs#IsPredArchimedean.findAtom, so it could be moved out of there)?

[Abraham Solomon]

Daniel Weber said:

Abraham Solomon said:

Yaël Dillies said:

Daniel Weber successfully implemented rooted trees as archimedean pred-orders (docs#PredOrder, docs#IsPredArchimedean). Could you reuse this idea?

I think this could be similar to what i wanted, thanks!

I think the way it would be defined for me is for two vertices $v,w \in T$, $v \leq w$ if both are on an infinite path together and $|v| \leq |w|$.

Maybe I misunderstand what you want to do, but can't you directly use docs#RootedTree and then define $\left| \cdot \right|$ as Nat.find (bot_le (a := r)).exists_pred_iterate (this is also part of the definition of docs#IsPredArchimedean.findAtom, so it could be moved out of there)?

Yea i think that could work, eventually i want to be able to define something like this:

$\inf \{ \lambda > 0 | \inf_{\Pi}\sum_{z \in \Pi}\lambda^{-|z|} = 0\}$.

Where the second infimum is taken over all cutsets of the tree $T$; this is the branching number of the tree $\text{br}(T)$ and for the binary tree is equal to 2(this is one of several exponents that can classify spherically symmetric trees). Almost by definition, it is larger than or equal to one.

With that as the end goal, ill have to be careful as to how the tree works with regards to its 'cutsets'.

The reference for doing this is from:
Russell Lyons and Yuval Peres. Probability on Trees and Networks. Cambridge
Series in Statistical and Probabilistic Mathematics. Cambridge University Press,
2017.

[Daniel Weber]

If I understood correctly, order theoretically a set $\Pi$ is a cutset if for all $x$ there exists $y \in \Pi$ such that $x, y$ are comparable

[Abraham Solomon]

Daniel Weber said:

If I understood correctly, order theoretically a set $\Pi$ is a cutset if for all $x$ there exists $y \in \Pi$ such that $x, y$ are comparable

Yea, and it must also be finite