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?

theorem SimpleGraph.ConnectedComponent.card_le_card_of_le {V : Type u} [Finite V] {G G' : SimpleGraph V} (h : G ≤ G') : Nat.card G'.ConnectedComponent ≤ Nat.card 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_reducible]

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_reducible]

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

Equations

• G.instFintypeConnectedComponent = { elems := Finset.image Quotient.mk'' Finset.univ, complete := ⋯ }

@[instance_reducible]

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

Equations

• G.instDecidablePreconnected = { decide := decide (∀ a ∈ Finset.univ, (fun (u : V) => ∀ (v : V), G.Reachable u v) a), reflects_decide := ⋯ }

@[instance_reducible]

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_reducible]

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] : {c : G.ConnectedComponent | c.supp ⊆ c'.supp}.disjiUnion (fun (c : G.ConnectedComponent) => c.supp.toFinset) ⋯ = c'.supp.toFinset

@[reducible, inline]

abbrev SimpleGraph.oddComponents {V : Type u} (G : SimpleGraph V) : Set G.ConnectedComponent

The odd components are the connected components of odd cardinality. This definition excludes infinite components.

Equations

• G.oddComponents = {c : G.ConnectedComponent | Odd c.supp.ncard}

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

theorem SimpleGraph.odd_ncard_oddComponents {V : Type u} (G : SimpleGraph V) [Finite V] : Odd G.oddComponents.ncard ↔ Odd (Nat.card V)

theorem SimpleGraph.ncard_oddComponents_mono {V : Type u} (G : SimpleGraph V) [Finite V] {G' : SimpleGraph V} (h : G ≤ G') : G'.oddComponents.ncard ≤ G.oddComponents.ncard