Counting cliques, independent sets, and vertex covers

Lax280166.CountingCliques · concepts/Lax280166/CountingCliques.lean · lax-280166

definition

Loading review…

Natural Language Statement

Definition

On a finite marked graph with $k$ marked vertices, #Clique counts the cliques of exactly $k$ vertices, #Independent Set the independent sets of exactly $k$ vertices, and #Vertex Cover the vertex covers of exactly $k$ vertices. The count is taken at the threshold size: a set larger or smaller than the marked set is not counted.

Concept map

9 concepts; 25 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Tactic.FinCases
2	import Mathlib.Order.PiLex
3	import Mathlib.Data.Prod.Lex
4	import Mathlib.Data.Fintype.EquivFin
5	import Mathlib.ModelTheory.Order
6	import Mathlib.ModelTheory.Semantics
7	import Mathlib.ModelTheory.Complexity
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Fintype.Lattice
10	import Mathlib.Data.Finite.Sigma
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.ModelTheory.Syntax
16	import Mathlib.Algebra.Order.BigOperators.Group.Finset
17	import Mathlib.Data.Fintype.Card
18	import Mathlib.SetTheory.Cardinal.Finite
19	import Mathlib.Data.Fintype.Sort
20	import Mathlib.Order.Hom.Set
21	import Mathlib.Logic.Equiv.Prod
22	import Mathlib.Data.Set.Finite.Lemmas
23	import Lax799700.CliqueFamily
24	import Mathlib.SetTheory.Cardinal.Finite
25	import Lax366625.CountingProblems
26
27	/-!
28	---
29	title: Counting cliques, independent sets, and vertex covers
30	type: definition
31	---
32	On a finite marked graph with $k$ marked vertices, #Clique counts the cliques
33	of exactly $k$ vertices, #Independent Set the independent sets of exactly $k$
34	vertices, and #Vertex Cover the vertex covers of exactly $k$ vertices. The
35	count is taken at the threshold size: a set larger or smaller than the
36	marked set is not counted.
37	-/
38
39	namespace Lax280166.CountingCliques
40
41	open Lax799700.CliqueFamily
42
43	open FirstOrder
44
45	open Language Structure
46
47	section Solutions
48
49	variable (A : Type) [markedGraph.Structure A]
50
51	/-- The set `S` is a clique with exactly as many vertices as the marked set, in
52	a finite marked graph. -/
53	def CliqueOfSize (S : A → Prop) : Prop :=
54	Finite A ∧ (∀ x y, S x → S y → x ≠ y → MGAdj x y) ∧
55	{x \| S x}.ncard = {x : A \| MGMarked x}.ncard
56
57	end Solutions
58
59	open FirstOrder
60
61	open Language Structure
62
63	section Generic
64
65	variable {A B : Type}
66
67	/-- The set `S` is pairwise `Adjp`-related off the diagonal and has exactly as
68	many elements as the `Kp`-marked set. -/
69	def CliqueOfSizeOn (Adjp : A → A → Prop) (Kp : A → Prop) (S : A → Prop) : Prop :=
70	(∀ x y, S x → S y → x ≠ y → Adjp x y) ∧ {x \| S x}.ncard = {x \| Kp x}.ncard
71
72	/-- The set `C` meets every off-diagonal `Adjp`-edge and has exactly as many
73	elements as the `Kp`-marked set. -/
74	def CoverOfSizeOn (Adjp : A → A → Prop) (Kp : A → Prop) (C : A → Prop) : Prop :=
75	(∀ x y, x ≠ y → Adjp x y → C x ∨ C y) ∧ {x \| C x}.ncard = {x \| Kp x}.ncard
76
77	end Generic
78
79	section Problems
80
81	variable (A : Type) [markedGraph.Structure A]
82
83	/-- The set `S` is an independent set with exactly as many vertices as the
84	marked set, in a finite marked graph. -/
85	def IndepOfSize (S : A → Prop) : Prop :=
86	Finite A ∧ CliqueOfSizeOn (fun x y : A => ¬MGAdj x y) (fun x => MGMarked x) S
87
88	/-- The set `C` is a vertex cover with exactly as many vertices as the marked
89	set, in a finite marked graph. -/
90	def CoverOfSize (C : A → Prop) : Prop :=
91	Finite A ∧ CoverOfSizeOn (fun x y : A => MGAdj x y) (fun x => MGMarked x) C
92
93	end Problems
94
95	open Lax366625.CountingProblems
96
97	/-- #Clique, as a counting problem. -/
98	noncomputable def SharpClique : CountingProblem Lax799700.CliqueFamily.markedGraph :=
99	CountingProblem.ofFun fun A _ =>
100	Nat.card {S : A → Prop // CliqueOfSize A S}
101
102	/-- #Independent Set, as a counting problem. -/
103	noncomputable def SharpIndependentSet : CountingProblem Lax799700.CliqueFamily.markedGraph :=
104	CountingProblem.ofFun fun A _ =>
105	Nat.card {S : A → Prop // IndepOfSize A S}
106
107	/-- #Vertex Cover, as a counting problem. -/
108	noncomputable def SharpVertexCover : CountingProblem Lax799700.CliqueFamily.markedGraph :=
109	CountingProblem.ofFun fun A _ =>
110	Nat.card {C : A → Prop // CoverOfSize A C}
111
112	end Lax280166.CountingCliques
113

Builds on

Used by

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Counting cliques, independent sets, and vertex covers

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments