Counting walks of a given length

Main definitions

• walkLengthTwoEquivCommonNeighbors: bijective correspondence between walks of length two from u to v and common neighbours of u and v. Note that u and v may be the same.
• finsetWalkLength: the Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

TODO: should this be extended further?

Walks of a given length

theorem SimpleGraph.set_walk_self_length_zero_eq {V : Type u} (G : SimpleGraph V) (u : V) : {p : G.Walk u u | p.length = 0} = {Walk.nil}

theorem SimpleGraph.set_walk_length_zero_eq_of_ne {V : Type u} (G : SimpleGraph V) {u v : V} (h : u ≠ v) : {p : G.Walk u v | p.length = 0} = ∅

theorem SimpleGraph.set_walk_length_succ_eq {V : Type u} (G : SimpleGraph V) (u v : V) (n : ℕ) : {p : G.Walk u v | p.length = n.succ} = ⋃ (w : V), ⋃ (h : G.Adj u w), Walk.cons h '' {p' : G.Walk w v | p'.length = n}

def SimpleGraph.walkLengthTwoEquivCommonNeighbors {V : Type u} (G : SimpleGraph V) (u v : V) : { p : G.Walk u v // p.length = 2 } ≃ ↑(G.commonNeighbors u v)

Walks of length two from u to v correspond bijectively to common neighbours of u and v. Note that u and v may be the same.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe {V : Type u} (G : SimpleGraph V) (u v : V) (p : { p : G.Walk u v // p.length = 2 }) : ↑((G.walkLengthTwoEquivCommonNeighbors u v) p) = (↑p).snd

@[simp]

theorem SimpleGraph.walkLengthTwoEquivCommonNeighbors_symm_apply_coe {V : Type u} (G : SimpleGraph V) (u v : V) (w : ↑(G.commonNeighbors u v)) : ↑((G.walkLengthTwoEquivCommonNeighbors u v).symm w) = (Adj.toWalk ⋯).concat ⋯

def SimpleGraph.finsetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : Finset (G.Walk u v)

The Finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a Fintype instance, and it can also be useful as a recursive description of this set when V is finite.

See SimpleGraph.coe_finsetWalkLength_eq for the relationship between this Finset and the set of length-n walks.

Equations

• One or more equations did not get rendered due to their size.
• G.finsetWalkLength 0 u v = if h : u = v then ⋯ ▸ {SimpleGraph.Walk.nil} else ∅

theorem SimpleGraph.coe_finsetWalkLength_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : ↑(G.finsetWalkLength n u v) = {p : G.Walk u v | p.length = n}

theorem SimpleGraph.mem_finsetWalkLength_iff {V : Type u} {G : SimpleGraph V} [DecidableEq V] [G.LocallyFinite] {n : ℕ} {u v : V} {p : G.Walk u v} : p ∈ G.finsetWalkLength n u v ↔ p.length = n

def SimpleGraph.finsetWalkLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : Finset (G.Walk u v)

The Finset of walks from u to v with length less than n. See finsetWalkLength for context. In particular, we use this definition for SimpleGraph.Path.instFintype.

Equations

• G.finsetWalkLengthLT n u v = (Finset.range n).disjiUnion (fun (l : ℕ) => G.finsetWalkLength l u v) ⋯

theorem SimpleGraph.coe_finsetWalkLengthLT_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : ↑(G.finsetWalkLengthLT n u v) = {p : G.Walk u v | p.length < n}

theorem SimpleGraph.mem_finsetWalkLengthLT_iff {V : Type u} {G : SimpleGraph V} [DecidableEq V] [G.LocallyFinite] {n : ℕ} {u v : V} {p : G.Walk u v} : p ∈ G.finsetWalkLengthLT n u v ↔ p.length < n

instance SimpleGraph.fintypeSetWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.length = n}

Equations

• G.fintypeSetWalkLength u v n = Fintype.ofFinset (G.finsetWalkLength n u v) ⋯

instance SimpleGraph.fintypeSubtypeWalkLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.length = n }

Equations

• G.fintypeSubtypeWalkLength u v n = G.fintypeSetWalkLength u v n

theorem SimpleGraph.set_walk_length_toFinset_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (n : ℕ) (u v : V) : {p : G.Walk u v | p.length = n}.toFinset = G.finsetWalkLength n u v

theorem SimpleGraph.card_set_walk_length_eq {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype.card ↑{p : G.Walk u v | p.length = n} = (G.finsetWalkLength n u v).card

instance SimpleGraph.fintypeSetWalkLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.length < n}

Equations

• G.fintypeSetWalkLengthLT u v n = Fintype.ofFinset (G.finsetWalkLengthLT n u v) ⋯

instance SimpleGraph.fintypeSubtypeWalkLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.length < n }

Equations

• G.fintypeSubtypeWalkLengthLT u v n = G.fintypeSetWalkLengthLT u v n

instance SimpleGraph.fintypeSetPathLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.IsPath ∧ p.length = n}

Equations

• G.fintypeSetPathLength u v n = Fintype.ofFinset (Finset.filter (fun (w : G.Walk u v) => w.IsPath) (G.finsetWalkLength n u v)) ⋯

instance SimpleGraph.fintypeSubtypePathLength {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.IsPath ∧ p.length = n }

Equations

• G.fintypeSubtypePathLength u v n = G.fintypeSetPathLength u v n

instance SimpleGraph.fintypeSetPathLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype ↑{p : G.Walk u v | p.IsPath ∧ p.length < n}

Equations

• G.fintypeSetPathLengthLT u v n = Fintype.ofFinset (Finset.filter (fun (w : G.Walk u v) => w.IsPath) (G.finsetWalkLengthLT n u v)) ⋯

instance SimpleGraph.fintypeSubtypePathLengthLT {V : Type u} (G : SimpleGraph V) [DecidableEq V] [G.LocallyFinite] (u v : V) (n : ℕ) : Fintype { p : G.Walk u v // p.IsPath ∧ p.length < n }

Equations

• G.fintypeSubtypePathLengthLT u v n = G.fintypeSetPathLengthLT u v n

instance SimpleGraph.instFiniteConnectedComponent {V : Type u} (G : SimpleGraph V) [Finite V] : Finite G.ConnectedComponent

theorem SimpleGraph.reachable_iff_exists_finsetWalkLength_nonempty {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] (u v : V) : G.Reachable u v ↔ ∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n) u v).Nonempty

instance SimpleGraph.instDecidableRelReachable {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : DecidableRel G.Reachable

Equations

• G.instDecidableRelReachable u v = decidable_of_iff' (∃ (n : Fin (Fintype.card V)), (G.finsetWalkLength (↑n) u v).Nonempty) ⋯

instance SimpleGraph.instFintypeConnectedComponent {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Fintype G.ConnectedComponent

Equations

• G.instFintypeConnectedComponent = Quotient.fintype G.reachableSetoid

instance SimpleGraph.instDecidablePreconnected {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Decidable G.Preconnected

Equations

• G.instDecidablePreconnected = inferInstanceAs (Decidable (∀ (u v : V), G.Reachable u v))

instance SimpleGraph.instDecidableConnected {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] : Decidable G.Connected

Equations

• G.instDecidableConnected = decidable_of_iff (G.Preconnected ∧ Finset.univ.Nonempty) ⋯

instance SimpleGraph.Path.instFintype {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {u v : V} : Fintype (G.Path u v)

Equations

• One or more equations did not get rendered due to their size.

instance SimpleGraph.instDecidableMemSupp {V : Type u} (G : SimpleGraph V) [DecidableEq V] [Fintype V] [DecidableRel G.Adj] (c : G.ConnectedComponent) (v : V) : Decidable (v ∈ c.supp)

Equations

• G.instDecidableMemSupp c v = SimpleGraph.ConnectedComponent.recOn c (fun (w : V) => decidable_of_iff (G.Reachable v w) ⋯) ⋯

theorem SimpleGraph.disjiUnion_supp_toFinset_eq_supp_toFinset {V : Type u} {G : SimpleGraph V} [DecidableEq V] [Fintype V] [DecidableRel G.Adj] {G' : SimpleGraph V} (h : G ≤ G') (c' : G'.ConnectedComponent) [Fintype ↑c'.supp] [DecidablePred fun (c : G.ConnectedComponent) => c.supp ⊆ c'.supp] : (Finset.filter (fun (c : G.ConnectedComponent) => c.supp ⊆ c'.supp) Finset.univ).disjiUnion (fun (c : G.ConnectedComponent) => c.supp.toFinset) ⋯ = c'.supp.toFinset

theorem SimpleGraph.ConnectedComponent.odd_card_supp_iff_odd_subcomponents {V : Type u} (G : SimpleGraph V) [Finite V] {G' : SimpleGraph V} (h : G ≤ G') (c' : G'.ConnectedComponent) : Odd c'.supp.ncard ↔ Odd {c : G.ConnectedComponent | c.supp ⊆ c'.supp ∧ Odd c.supp.ncard}.ncard

theorem SimpleGraph.odd_card_iff_odd_components {V : Type u} (G : SimpleGraph V) [Finite V] : Odd (Nat.card V) ↔ Odd {c : G.ConnectedComponent | Odd c.supp.ncard}.ncard

theorem SimpleGraph.ncard_odd_components_mono {V : Type u} (G : SimpleGraph V) [Finite V] {G' : SimpleGraph V} (h : G ≤ G') : {c : G'.ConnectedComponent | Odd c.supp.ncard}.ncard ≤ {c : G.ConnectedComponent | Odd c.supp.ncard}.ncard