Definitions for the Haeupler–Saha–Srinivasan distributional theorem

Lax965890.HaeuplerSahaSrinivasanDefinitions · concepts/Lax965890/HaeuplerSahaSrinivasanDefinitions.lean · lax-965890

definition

Loading review…

Natural Language Statement

Definition

Fix a finite collection of mutually independent random variables and a finite set of bad events determined by them. The Moser–Tardos algorithm repeatedly resamples a currently true bad event. Besides the bad events, we may observe any other event $B$ determined by the same variables. This file defines the bad-event restriction of the event family, the dependency neighborhood $\Gamma(B)$ , the event that $B$ is true at some stage of the algorithm, and the event that $B$ is true in its final output.

Concept map

2 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

1	import Mathlib
2	import Lax965890.MoserTardosDefinitions
3
4	/-!
5	---
6	title: Definitions for the Haeupler–Saha–Srinivasan distributional theorem
7	type: definition
8	---
9	Fix a finite collection of mutually independent random variables and a finite
10	set of bad events determined by them. The Moser--Tardos algorithm repeatedly
11	resamples a currently true bad event. Besides the bad events, we may observe
12	any other event $B$ determined by the same variables. This file defines the
13	bad-event restriction of the event family, the dependency neighborhood
14	$\Gamma(B)$ , the event that $B$ is true at some stage of the algorithm, and
15	the event that $B$ is true in its final output.
16	-/
17
18	set_option autoImplicit false
19
20	open scoped ENNReal
21
22	namespace Lax965890.HaeuplerSahaSrinivasanDefinitions
23
24	open scoped Classical
25
26	open Lax965890.MoserTardosDefinitions
27
28	variable {Event : Type} [Fintype Event] [DecidableEq Event]
29	variable {Variable : Type} [Fintype Variable] [DecidableEq Variable]
30	variable (Value : Variable → Type) [∀ i, MeasurableSpace (Value i)]
31
32	/-- An event belonging to the finite family on which the algorithm runs. -/
33	abbrev BadEventIndex (badEvents : Finset Event) := {A // A ∈ badEvents}
34
35	/-- The variables determining a bad event. -/
36	def badEventVariables (badEvents : Finset Event)
37	(variablesOf : Event → Finset Variable) :
38	BadEventIndex badEvents → Finset Variable :=
39	fun A ↦ variablesOf A.1
40
41	/-- The local set defining a bad event. -/
42	def badEventSet (badEvents : Finset Event)
43	(variablesOf : Event → Finset Variable)
44	(event : ∀ A, Set (LocalAssignment Value (variablesOf A))) :
45	∀ A, Set (LocalAssignment Value (badEventVariables badEvents variablesOf A)) :=
46	fun A ↦ event A.1
47
48	/--
49	The bad events other than `B` that share at least one determining variable
50	with `B`.
51	-/
52	def dependencyNeighborhood (badEvents : Finset Event)
53	(variablesOf : Event → Finset Variable) (B : Event) :
54	Finset (BadEventIndex badEvents) :=
55	Finset.univ.filter fun A ↦
56	A.1 ≠ B ∧ ¬Disjoint (variablesOf A.1) (variablesOf B)
57
58	/-- The observed event `B` is true in the assignment at stage `n`. -/
59	def eventOccursAt (badEvents : Finset Event)
60	(variablesOf : Event → Finset Variable)
61	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
62	(selectionRule : ResamplingRule Value
63	(badEventVariables badEvents variablesOf)
64	(badEventSet Value badEvents variablesOf event))
65	(table : ResamplingTable Value) (B : Event) (n : Nat) : Prop :=
66	violates Value variablesOf event
67	(currentAssignment Value table
68	(runCounts Value (badEventVariables badEvents variablesOf)
69	(badEventSet Value badEvents variablesOf event) selectionRule table n)) B
70
71	/-- The set of sample tables on which `B` is true at least once. -/
72	def eventEverOccurs (badEvents : Finset Event)
73	(variablesOf : Event → Finset Variable)
74	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
75	(selectionRule : ResamplingRule Value
76	(badEventVariables badEvents variablesOf)
77	(badEventSet Value badEvents variablesOf event))
78	(B : Event) : Set (ResamplingTable Value) :=
79	{table \| ∃ n, eventOccursAt Value badEvents variablesOf event selectionRule table B n}
80
81	/--
82	The first stage at which the algorithm has terminated. On a nonterminating
83	table it is set to zero; under the local-lemma hypotheses that exceptional set
84	has probability zero.
85	-/
86	noncomputable def outputTime (badEvents : Finset Event)
87	(variablesOf : Event → Finset Variable)
88	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
89	(selectionRule : ResamplingRule Value
90	(badEventVariables badEvents variablesOf)
91	(badEventSet Value badEvents variablesOf event))
92	(table : ResamplingTable Value) : Nat :=
93	if h : ∃ n, resamplingLog Value (badEventVariables badEvents variablesOf)
94	(badEventSet Value badEvents variablesOf event) selectionRule table n = none
95	then Nat.find h
96	else 0
97
98	/-- The assignment returned when the resampling algorithm terminates. -/
99	noncomputable def outputAssignment (badEvents : Finset Event)
100	(variablesOf : Event → Finset Variable)
101	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
102	(selectionRule : ResamplingRule Value
103	(badEventVariables badEvents variablesOf)
104	(badEventSet Value badEvents variablesOf event))
105	(table : ResamplingTable Value) : Assignment Value :=
106	currentAssignment Value table
107	(runCounts Value (badEventVariables badEvents variablesOf)
108	(badEventSet Value badEvents variablesOf event) selectionRule table
109	(outputTime Value badEvents variablesOf event selectionRule table))
110
111	/-- The set of sample tables whose output assignment makes `B` true. -/
112	noncomputable def eventOccursInOutput (badEvents : Finset Event)
113	(variablesOf : Event → Finset Variable)
114	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
115	(selectionRule : ResamplingRule Value
116	(badEventVariables badEvents variablesOf)
117	(badEventSet Value badEvents variablesOf event))
118	(B : Event) : Set (ResamplingTable Value) :=
119	{table \| violates Value variablesOf event
120	(outputAssignment Value badEvents variablesOf event selectionRule table) B}
121
122	/-- The probability that `B` is true at least once during the algorithm. -/
123	noncomputable def probabilityEventEverOccurs
124	(distribution : ∀ i, MeasureTheory.Measure (Value i))
125	(badEvents : Finset Event) (variablesOf : Event → Finset Variable)
126	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
127	(selectionRule : ResamplingRule Value
128	(badEventVariables badEvents variablesOf)
129	(badEventSet Value badEvents variablesOf event))
130	(B : Event) : ℝ≥0∞ :=
131	tableMeasure Value distribution
132	(eventEverOccurs Value badEvents variablesOf event selectionRule B)
133
134	/-- The probability that `B` is true in the algorithm's output. -/
135	noncomputable def probabilityEventInOutput
136	(distribution : ∀ i, MeasureTheory.Measure (Value i))
137	(badEvents : Finset Event) (variablesOf : Event → Finset Variable)
138	(event : ∀ A, Set (LocalAssignment Value (variablesOf A)))
139	(selectionRule : ResamplingRule Value
140	(badEventVariables badEvents variablesOf)
141	(badEventSet Value badEvents variablesOf event))
142	(B : Event) : ℝ≥0∞ :=
143	tableMeasure Value distribution
144	(eventOccursInOutput Value badEvents variablesOf event selectionRule B)
145
146	end Lax965890.HaeuplerSahaSrinivasanDefinitions
147