Catalog/Sparsity/Admissibility/Full.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`. (Def 2.2) -/
13	structure IsAdmFamily (G : SimpleGraph V) (r : ℕ) (v : V)
14	{ι : Type*} (paths : ι → (u : V) × G.Walk v u) : Prop where
15	target_lt : ∀ i, (paths i).1 < v
16	isPath : ∀ i, (paths i).2.IsPath
17	length_le : ∀ i, (paths i).2.length ≤ r
18	disjoint : ∀ i j, i ≠ j →
19	∀ w, w ∈ (paths i).2.support → w ∈ (paths j).2.support → w = v
20
21	/-- The r-admissibility of a vertex `v`. (Def 2.2) -/
22	def admVertex (G : SimpleGraph V) (r : ℕ) (v : V) : ℕ :=
23	1 + Finset.sup (Finset.range (Fintype.card V)) (fun k =>
24	if ∃ (paths : Fin k → (u : V) × G.Walk v u), IsAdmFamily G r v paths
25	then k else 0)
26
27	/-- The r-admissibility of `G` (per ordering). (Def 2.3) -/
28	def adm (G : SimpleGraph V) (r : ℕ) : ℕ :=
29	Finset.sup Finset.univ (fun v => admVertex G r v)
30
31	end
32
33	end Catalog.Sparsity.Admissibility
34