OAI/Combinatorics/Ramsey/CycleClique/Construction/LongestPaths.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CycleClique.Construction.IsIndexedPath line 9
2. theorem OAI.CycleClique.Construction.indexedPath_snoc line 13
3. theorem OAI.CycleClique.Construction.exists_longest_path_from line 27

   Source documentation

   Finite cardinality bounds path order, so maximizing it uses only well-ordering of natural numbers.

   theorem exists_longest_path_from {V : Type*} [Fintype V]
       (G : SimpleGraph V) (x : V) :
       ∃ r, ∃ f : Fin (r + 1) → V, IsIndexedPath G f ∧ f 0 = x ∧
         ∀ q (g : Fin (q + 1) → V), IsIndexedPath G g → g 0 = x → q ≤ r := by
   …

   Mentions: OAI.CycleClique.Construction.IsIndexedPath

4. theorem OAI.CycleClique.Construction.longest_path_endpoint_neighbors line 55

   Source documentation

   Every neighbour of the last vertex of a longest fixed-start path lies on that path.

   theorem longest_path_endpoint_neighbors {V : Type*} {G : SimpleGraph V}
       {x : V} {r : ℕ} {f : Fin (r + 1) → V} (hf : IsIndexedPath G f)
       (hstart : f 0 = x)
       (hmax : ∀ q (g : Fin (q + 1) → V), IsIndexedPath G g → g 0 = x → q ≤ r) :
       ∀ v, G.Adj (f (Fin.last r)) v → v ∈ Set.range f := by
   …

   Mentions: OAI.CycleClique.Construction.IsIndexedPath

5. theorem OAI.CycleClique.Construction.longest_path_degree_bound line 68

   Source documentation

   The endpoint neighbourhood alone gives the elementary lower bound on the order of a longest fixed-start path.

   theorem longest_path_degree_bound {V : Type*} [Fintype V] {G : SimpleGraph V}
       {x : V} {r : ℕ} {f : Fin (r + 1) → V} (hf : IsIndexedPath G f)
       (hstart : f 0 = x)
       (hmax : ∀ q (g : Fin (q + 1) → V), IsIndexedPath G g → g 0 = x → q ≤ r) :
       (G.neighborSet (f (Fin.last r))).ncard ≤ r := by
   …

   Mentions: OAI.CycleClique.Construction.IsIndexedPath