#BIS and #PP2DNF

Lax859101.CountingBipartite · concepts/Lax859101/CountingBipartite.lean · lax-859101

definition

Loading review…

Natural Language Statement

Definition

A bipartite graph is given with its bipartition, a mark on the left side, and its edges, read from left to right. #BIS counts the independent sets: the sets of vertices with no edge from a left member to a right member. #PP2DNF counts the models of the partitioned positive 2-DNF formula of the graph, with one variable per vertex and one term $x \wedge y$ per edge from $x$ to $y$ : the sets of vertices containing both ends of some edge.

Concept map

5 concepts; 13 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Data.Set.Card
2	import Mathlib.Algebra.BigOperators.Ring.Finset
3	import Mathlib.Algebra.Order.BigOperators.Group.Finset
4	import Mathlib.Data.Fintype.BigOperators
5	import Mathlib.SetTheory.Cardinal.Finite
6	import Mathlib.Algebra.Group.Action.Defs
7	import Mathlib.Tactic.Ring
8	import Mathlib.ModelTheory.Graph
9	import Mathlib.Order.PiLex
10	import Mathlib.Data.Prod.Lex
11	import Mathlib.Data.Fintype.EquivFin
12	import Mathlib.ModelTheory.Order
13	import Mathlib.ModelTheory.Semantics
14	import Mathlib.ModelTheory.Complexity
15	import Mathlib.Tactic.FinCases
16	import Mathlib.Logic.Equiv.Fin.Basic
17	import Mathlib.Data.Fintype.Lattice
18	import Mathlib.Data.Finite.Sigma
19	import Mathlib.Order.Lattice.Nat
20	import Mathlib.Data.Fintype.Pigeonhole
21	import Mathlib.Dynamics.FixedPoints.Basic
22	import Mathlib.ModelTheory.Syntax
23	import Mathlib.Data.Fintype.Card
24	import Mathlib.Logic.Equiv.Prod
25	import Mathlib.Data.Set.Finite.Lemmas
26	import Mathlib.Data.Fintype.Sort
27	import Mathlib.Order.Hom.Set
28	import Lax366625.CountingProblems
29
30	/-!
31	---
32	title: #BIS and #PP2DNF
33	type: definition
34	---
35	A bipartite graph is given with its bipartition, a mark on the left side,
36	and its edges, read from left to right. #BIS counts the independent sets:
37	the sets of vertices with no edge from a left member to a right member.
38	#PP2DNF counts the models of the partitioned positive 2-DNF formula of the
39	graph, with one variable per vertex and one term $x \wedge y$ per edge from
40	$x$ to $y$ : the sets of vertices containing both ends of some edge.
41	-/
42
43	namespace Lax859101.CountingBipartite
44
45	open FirstOrder
46
47	open FirstOrder.Language
48
49	/-- The relation symbols of the language. -/
50	inductive bipGraphRel : ℕ → Type where
51	/-- `left a`: the vertex `a` is on the left side. -/
52	\| left : bipGraphRel 1
53	/-- `edge a b`: there is an edge between `a` and `b`; read for `a` on the
54	left and `b` on the right. -/
55	\| edge : bipGraphRel 2
56	deriving DecidableEq
57
58	/-- The relational language of bipartite graphs given with their bipartition. -/
59	def bipGraph : FirstOrder.Language :=
60	⟨fun _ => Empty, bipGraphRel⟩
61
62	instance instIsRelationalBipGraph : FirstOrder.Language.IsRelational bipGraph := fun _ =>
63	(inferInstance : IsEmpty Empty)
64
65	/-- `left a`: the vertex `a` is on the left side. -/
66	abbrev bgLeft : bipGraph.Relations 1 :=
67	.left
68
69	/-- `edge a b`: there is an edge between `a` and `b`; read for `a` on the
70	left and `b` on the right. -/
71	abbrev bgEdge : bipGraph.Relations 2 :=
72	.edge
73
74	open FirstOrder
75
76	open Language Structure
77
78	section Shorthands
79
80	variable {A : Type} [bipGraph.Structure A]
81
82	/-- `left a`: the vertex `a` is on the left side. -/
83	def BGLeft {A : Type} [bipGraph.Structure A] (a0 : A) : Prop :=
84	FirstOrder.Language.Structure.RelMap bgLeft ![a0]
85
86	/-- `edge a b`: there is an edge between `a` and `b`; read for `a` on the
87	left and `b` on the right. -/
88	def BGEdge {A : Type} [bipGraph.Structure A] (a0 : A) (a1 : A) : Prop :=
89	FirstOrder.Language.Structure.RelMap bgEdge ![a0, a1]
90
91	end Shorthands
92
93	/-- The set `S` is independent in a bipartite graph: no edge goes from a left
94	member of `S` to a right member of `S`. -/
95	def BipIndep (A : Type) [bipGraph.Structure A] (S : A → Prop) : Prop :=
96	∀ x y : A, S x → S y → BGLeft x → ¬BGLeft y → ¬BGEdge x y
97
98	/-- The set `S` of true variables satisfies the partitioned positive 2-DNF
99	formula of a bipartite graph – one variable per vertex, one term `x ∧ y` per
100	edge from a left vertex `x` to a right vertex `y`: some term has both its
101	variables true. -/
102	def Pp2dnfModel (A : Type) [bipGraph.Structure A] (S : A → Prop) : Prop :=
103	∃ x y : A, S x ∧ S y ∧ BGLeft x ∧ ¬BGLeft y ∧ BGEdge x y
104
105	open Lax366625.CountingProblems
106
107	/-- #BIS, as a counting problem. -/
108	noncomputable def SharpBIS : CountingProblem Lax859101.CountingBipartite.bipGraph :=
109	CountingProblem.ofFun fun A _ =>
110	Nat.card {S : A → Prop // BipIndep A S}
111
112	/-- #PP2DNF, as a counting problem. -/
113	noncomputable def SharpPP2DNF : CountingProblem Lax859101.CountingBipartite.bipGraph :=
114	CountingProblem.ofFun fun A _ =>
115	Nat.card {S : A → Prop // Pp2dnfModel A S}
116
117	end Lax859101.CountingBipartite
118

Builds on

Lax366625.CountingProblems

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

#BIS and #PP2DNF

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments