Catalog/Sparsity/Admissibility/Contract.lean

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3
4	open Classical
5
6	namespace Catalog.Sparsity.Admissibility
7
8	noncomputable section
9
10	variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V]
11
12	/-- An admissible family of paths at vertex `v`: an indexed collection of
13	paths from `v` to distinct vertices below `v` in the ordering, each of
14	length at most `r`, pairwise vertex-disjoint except at their shared
15	starting point `v`. (Def 2.2) -/
16	structure IsAdmFamily (G : SimpleGraph V) (r : ℕ) (v : V)
17	{ι : Type*} (paths : ι → (u : V) × G.Walk v u) : Prop where
18	target_lt : ∀ i, (paths i).1 < v
19	isPath : ∀ i, (paths i).2.IsPath
20	length_le : ∀ i, (paths i).2.length ≤ r
21	disjoint : ∀ i j, i ≠ j →
22	∀ w, w ∈ (paths i).2.support → w ∈ (paths j).2.support → w = v
23
24	/-- The r-admissibility of a vertex `v`: one plus the maximum size of an
25	admissible family of paths at `v`. (Def 2.2) -/
26	def admVertex (G : SimpleGraph V) (r : ℕ) (v : V) : ℕ :=
27	1 + Finset.sup (Finset.range (Fintype.card V)) (fun k =>
28	if ∃ (paths : Fin k → (u : V) × G.Walk v u), IsAdmFamily G r v paths
29	then k else 0)
30
31	/-- The r-admissibility of `G` (per ordering): the maximum over all vertices
32	of per-vertex r-admissibility. (Def 2.3) -/
33	def adm (G : SimpleGraph V) (r : ℕ) : ℕ :=
34	Finset.sup Finset.univ (fun v => admVertex G r v)
35
36	end
37
38	end Catalog.Sparsity.Admissibility
39