GraphicMatroid

Graph, coordinate, and measure constructions for the hard-sphere NBC volume identity.

noncomputable def HsVirial.componentEdgeFinset {V : Type u_1} [Fintype V] {H : SimpleGraph V} (c : H.ConnectedComponent) : Finset (Sym2 ↥c)

The finite edge set of a connected component.

Equations

• HsVirial.componentEdgeFinset c = ⋯.toFinset

@[simp]

theorem HsVirial.mem_componentEdgeFinset {V : Type u_1} [Fintype V] {H : SimpleGraph V} {c : H.ConnectedComponent} {e : Sym2 ↥c} : e ∈ componentEdgeFinset c ↔ e ∈ c.toSimpleGraph.edgeSet

def HsVirial.sym2SubtypeEmbedding {V : Type u_1} {S : Set V} : Sym2 ↑S ↪ Sym2 V

The inclusion of unordered pairs from a vertex subset into the ambient vertex set.

Equations

• HsVirial.sym2SubtypeEmbedding = { toFun := Sym2.map fun (x : ↑S) => ↑x, inj' := ⋯ }

theorem HsVirial.component_edge_map_mem {V : Type u_1} {H : SimpleGraph V} {c : H.ConnectedComponent} {e : Sym2 ↥c} (he : e ∈ c.toSimpleGraph.edgeSet) : sym2SubtypeEmbedding e ∈ H.edgeSet

theorem HsVirial.component_edge_card_bij {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] : (graphEdgeFinset H).card = ∑ c : H.ConnectedComponent, (componentEdgeFinset c).card

theorem HsVirial.component_edge_card_add_one {V : Type u_1} [Fintype V] (H : SimpleGraph V) (hH : H.IsAcyclic) (c : H.ConnectedComponent) : (componentEdgeFinset c).card + 1 = Nat.card ↥c

theorem HsVirial.componentVerts_card {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] : ∑ c : H.ConnectedComponent, Nat.card ↥c = Fintype.card V

theorem HsVirial.forest_edge_formula {V : Type u_1} [Fintype V] [DecidableEq V] (H : SimpleGraph V) [DecidableRel H.Adj] (hH : H.IsAcyclic) : (graphEdgeFinset H).card + Fintype.card H.ConnectedComponent = Fintype.card V

def HsVirial.IsGraphForest {V : Type u_1} (G : SimpleGraph V) (A : Finset (Sym2 V)) : Prop

An edge subset of the graph whose induced graph is acyclic.

Equations

• HsVirial.IsGraphForest G A = (↑A ⊆ G.edgeSet ∧ (SimpleGraph.fromEdgeSet ↑A).IsAcyclic)

def HsVirial.IsGraphCircuit {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (C : Finset (Sym2 V)) : Prop

A nonforest edge subset that becomes a forest after deleting any edge.

Equations

• HsVirial.IsGraphCircuit G C = (C ⊆ HsVirial.graphEdgeFinset G ∧ ¬HsVirial.IsGraphForest G C ∧ ∀ e ∈ C, HsVirial.IsGraphForest G (C.erase e))

theorem HsVirial.edgeSet_fromEdgeSet_of_subset {V : Type u_1} {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : ↑A ⊆ G.edgeSet) : (SimpleGraph.fromEdgeSet ↑A).edgeSet = ↑A

theorem HsVirial.graphEdgeFinset_fromEdgeSet {V : Type u_1} [Fintype V] {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : ↑A ⊆ G.edgeSet) : graphEdgeFinset (SimpleGraph.fromEdgeSet ↑A) = A

theorem HsVirial.graphEdgeFinset_fromEdgeSet_card {V : Type u_1} [Fintype V] {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : ↑A ⊆ G.edgeSet) : (graphEdgeFinset (SimpleGraph.fromEdgeSet ↑A)).card = A.card

theorem HsVirial.IsGraphForest.empty {V : Type u_1} (G : SimpleGraph V) : IsGraphForest G ∅

theorem HsVirial.IsGraphForest.subset {V : Type u_1} {G : SimpleGraph V} {A B : Finset (Sym2 V)} (hB : IsGraphForest G B) (hAB : A ⊆ B) : IsGraphForest G A

theorem HsVirial.IsGraphForest.insert_of_mem_forest {V : Type u_1} [DecidableEq V] {G F : SimpleGraph V} {A : Finset (Sym2 V)} (hA : IsGraphForest G A) (hAF : SimpleGraph.fromEdgeSet ↑A ≤ F) (hF : F.IsAcyclic) (e : Sym2 V) (heF : e ∈ F.edgeSet) (heG : e ∈ G.edgeSet) (heA : e ∉ A) : IsGraphForest G (insert e A)

def HsVirial.connectedComponentEquivOfReachableEq {V : Type u_1} {G H : SimpleGraph V} (h : G.Reachable = H.Reachable) : G.ConnectedComponent ≃ H.ConnectedComponent

Identification of components for graphs with the same reachability relation.

Equations

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

theorem HsVirial.connectedComponent_card_eq_of_reachable_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G H : SimpleGraph V} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G.Reachable = H.Reachable) : Fintype.card G.ConnectedComponent = Fintype.card H.ConnectedComponent

theorem HsVirial.finset_subset_graphEdgeFinset_of_fromEdgeSet_le {V : Type u_1} [Fintype V] {G F : SimpleGraph V} {A : Finset (Sym2 V)} (hA : IsGraphForest G A) (hAF : SimpleGraph.fromEdgeSet ↑A ≤ F) : A ⊆ graphEdgeFinset F

theorem HsVirial.graphEdgeFinset_subset_of_le_fromEdgeSet_union {V : Type u_1} [Fintype V] [DecidableEq V] {F : SimpleGraph V} {A B : Finset (Sym2 V)} (hF : F ≤ SimpleGraph.fromEdgeSet ↑(A ∪ B)) : graphEdgeFinset F ⊆ A ∪ B

theorem HsVirial.graphEdgeFinset_card_eq_of_reachable_eq {V : Type u_1} [Fintype V] {F H : SimpleGraph V} (hF : F.IsAcyclic) (hH : H.IsAcyclic) (hreach : F.Reachable = H.Reachable) : (graphEdgeFinset F).card = (graphEdgeFinset H).card

theorem HsVirial.IsGraphForest.augment {V : Type u_1} [DecidableEq V] [Finite V] {G : SimpleGraph V} {I J : Finset (Sym2 V)} (hI : IsGraphForest G I) (hJ : IsGraphForest G J) (hcard : I.card < J.card) : ∃ e ∈ J, e ∉ I ∧ IsGraphForest G (insert e I)

def HsVirial.graphicMatroid {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : Matroid (Sym2 V)

The matroid whose independent edge sets are the forests of the graph.

Equations

• HsVirial.graphicMatroid G = (IndepMatroid.ofFinset G.edgeSet (HsVirial.IsGraphForest G) ⋯ ⋯ ⋯ ⋯).matroid

@[simp]

theorem HsVirial.graphicMatroid_ground {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) : (graphicMatroid G).E = G.edgeSet

theorem HsVirial.graphicMatroid_indep_finset {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {A : Finset (Sym2 V)} : (graphicMatroid G).Indep ↑A ↔ IsGraphForest G A

theorem HsVirial.graphicMatroid_isCircuit_iff_graphCircuit {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {C : Finset (Sym2 V)} : (graphicMatroid G).IsCircuit ↑C ↔ IsGraphCircuit G C

theorem HsVirial.fromEdgeSet_le_of_graphForest {V : Type u_1} {G : SimpleGraph V} {A : Finset (Sym2 V)} (hA : IsGraphForest G A) : SimpleGraph.fromEdgeSet ↑A ≤ G

theorem HsVirial.graphicMatroid_isBase_iff_reachable_eq {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {B : Finset (Sym2 V)} (hB : IsGraphForest G B) : (graphicMatroid G).IsBase ↑B ↔ (SimpleGraph.fromEdgeSet ↑B).Reachable = G.Reachable