The panarboreal lower bound

If a graph on n vertices contains a copy of every tree on n vertices, it has at least ½ Σ_{k=1}^{n} ⌈(n − 1)/k⌉ ≥ ½ (n − 1) Hₙ edges (Chung–Graham; the easy half of Theorem of the Day's panarboreal formula s(n) ~ c n log n). For each k a caterpillar with a spine of k vertices has k vertices of degree ≥ ⌈(n − 1)/k⌉, so G has k such vertices too, and summing the sorted degrees gives the bound. Whether c = 1/2 is open.

Main results

• Panarboreal.exists_caterpillar: for 1 ≤ k ≤ n there is a tree on n vertices with k vertices of degree ≥ ⌈(n−1)/k⌉
• Panarboreal.sum_le_sum_degrees: if for each k at least k vertices have degree ≥ d_k, Σ_v deg v ≥ Σ_k d_k (no monotonicity needed)
• Panarboreal.sum_ceil_le_two_mul_card_edges: tree-universal graphs: Σ_k ⌈(n−1)/k⌉ ≤ 2|E|

References

• R. Whitty, Theorem of the Day, «The Panarboreal Formula» (CombinatorialTheory/Panarboreal).
• F. R. K. Chung, R. L. Graham, Universal graphs for trees, 1979 (cota inferior ½ n log n; superior (5/log 4) n log n).

def Panarboreal.pg {n : ℕ} (q : Fin n → Fin n) (hq : ∀ (v : Fin n), 0 < ↑v → ↑(q v) < ↑v) : SimpleGraph (Fin n)

Graph on Fin n in which every vertex v ≠ 0 is joined to its parent q v.

Equations

• Panarboreal.pg q hq = { Adj := fun (u v : Fin n) => 0 < ↑v ∧ u = q v ∨ 0 < ↑u ∧ v = q u, symm := ⋯, loopless := ⋯ }

theorem Panarboreal.pg_connected {n : ℕ} (hn : 0 < n) (q : Fin n → Fin n) (hq : ∀ (v : Fin n), 0 < ↑v → ↑(q v) < ↑v) : (pg q hq).Connected

theorem Panarboreal.pg_edgeFinset {n : ℕ} (hn : 0 < n) (q : Fin n → Fin n) (hq : ∀ (v : Fin n), 0 < ↑v → ↑(q v) < ↑v) [DecidableRel (pg q hq).Adj] : (pg q hq).edgeFinset = Finset.image (fun (v : Fin n) => s(q v, v)) (Finset.univ.erase ⟨0, hn⟩)

theorem Panarboreal.pg_isTree {n : ℕ} (hn : 0 < n) (q : Fin n → Fin n) (hq : ∀ (v : Fin n), 0 < ↑v → ↑(q v) < ↑v) : (pg q hq).IsTree

def Panarboreal.lp (k r : ℕ) : ℕ

Spine vertex that receives the leaves of residue r (residues 0, 1 go to the two ends).

Equations

• Panarboreal.lp k r = if r = 0 then 0 else if r = 1 then k - 1 else r - 1

def Panarboreal.par (k j : ℕ) : ℕ

Parent of j in the caterpillar with spine 0 – 1 – ⋯ – (k-1).

Equations

• Panarboreal.par k j = if j < k then j - 1 else Panarboreal.lp k ((j - k) % k)

theorem Panarboreal.par_lt {k : ℕ} (hk : 1 ≤ k) {j : ℕ} (hj : 0 < j) : par k j < j

theorem Panarboreal.par_le {k : ℕ} (hk : 1 ≤ k) (j : ℕ) : par k j ≤ j

def Panarboreal.catGraph (n k : ℕ) (hk : 1 ≤ k) : SimpleGraph (Fin n)

The caterpillar on Fin n with a spine of k vertices.

Equations

• Panarboreal.catGraph n k hk = Panarboreal.pg (fun (v : Fin n) => ⟨Panarboreal.par k ↑v, ⋯⟩) ⋯

theorem Panarboreal.catGraph_isTree {n k : ℕ} (hk : 1 ≤ k) (hn : 0 < n) : (catGraph n k hk).IsTree

theorem Panarboreal.card_filter_mod_ge {k : ℕ} (hk : 0 < k) (L r : ℕ) (hr : r < k) : L ≤ k * {t ∈ Finset.range L | t % k = r}.card + r

theorem Panarboreal.catGraph_adj {n k : ℕ} (hk : 1 ≤ k) (u v : Fin n) : (catGraph n k hk).Adj u v ↔ 0 < ↑v ∧ ↑u = par k ↑v ∨ 0 < ↑u ∧ ↑v = par k ↑u

theorem Panarboreal.cat_deg {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) [DecidableRel (catGraph n k hk).Adj] (w : Fin n) (hw : ↑w < k) (r : ℕ) (hr : r < k) (hrw : lp k r = ↑w) : {t ∈ Finset.range (n - k) | t % k = r}.card + {u ∈ Finset.range k | u + 1 = ↑w ∨ ↑w + 1 = u}.card ≤ (catGraph n k hk).degree w

theorem Panarboreal.spine_card_ge_one {k : ℕ} (hk2 : 2 ≤ k) {w : ℕ} (hw : w < k) : 1 ≤ {u ∈ Finset.range k | u + 1 = w ∨ w + 1 = u}.card

theorem Panarboreal.spine_card_ge_two {k w : ℕ} (hw0 : 0 < w) (hw : w + 1 < k) : 2 ≤ {u ∈ Finset.range k | u + 1 = w ∨ w + 1 = u}.card

theorem Panarboreal.exists_caterpillar {n k : ℕ} (hk : 1 ≤ k) (hkn : k ≤ n) : ∃ (T : SimpleGraph (Fin n)), T.IsTree ∧ ∃ (S : Finset (Fin n)), S.card = k ∧ ∀ v ∈ S, (n - 1 + k - 1) / k ≤ Nat.card ↑(T.neighborSet v)

theorem Panarboreal.eq_sum_ite (a B : ℕ) (h : a ≤ B) : a = ∑ t ∈ Finset.range B, if t < a then 1 else 0

theorem Panarboreal.sum_le_sum_degrees {V : Type u_1} [Fintype V] (n : ℕ) (f : V → ℕ) (d : ℕ → ℕ) (h : ∀ k ∈ Finset.Icc 1 n, ∃ (S : Finset V), k ≤ S.card ∧ ∀ v ∈ S, d k ≤ f v) : ∑ k ∈ Finset.Icc 1 n, d k ≤ ∑ v : V, f v

Layer-cake ordering lemma. If for every k ∈ [1, n] at least k vertices have f v ≥ d k, then ∑ d k ≤ ∑ f v (the monotonicity of d is not needed).

theorem Panarboreal.sum_ceil_le_two_mul_card_edges (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj] (hG : ∀ (T : SimpleGraph (Fin n)), T.IsTree → ∃ (e : Fin n ↪ Fin n), ∀ (u v : Fin n), T.Adj u v → G.Adj (e u) (e v)) : ∑ k ∈ Finset.Icc 1 n, (n - 1 + k - 1) / k ≤ 2 * G.edgeFinset.card

The panarboreal lower bound (Chung–Graham 1979; the easy half of Theorem of the Day's «panarboreal formula»). If a graph G on n vertices contains a copy of every tree on n vertices (an injective, adjacency-preserving map), then 2 |E(G)| ≥ Σ_{k=1}^{n} ⌈(n − 1)/k⌉ (⌈a/k⌉ = (a + k − 1)/k in ℕ). Hence s(n) ≥ ½ (n − 1) Hₙ ~ ½ n log n. Whether s(n) ~ ½ n log n (the constant c ∈ [1/2, 5/log 4]) is OPEN.