Weighted possible worlds and the probability of a query

Lax794877.WeightedWorlds · concepts/Lax794877/WeightedWorlds.lean · lax-794877

definition

Loading review…

Natural Language Statement

Definition

A weighted instance gives every uncertain fact two weights, written in binary along a linear order of the positions: a weight of presence $a$ and a weight of absence $c$ , the fact being present with probability $a/(a+c)$ independently of the others. The weight of a world is the product, over the uncertain facts, of the weight each takes in it. Counting weighted possible worlds is the counting problem whose value is the sum of the weights of the worlds in which a sentence $\varphi$ holds, counted as the number of witnesses that pick, for each uncertain fact, a number below its weight; it is $0$ on an instance whose positions are not linearly ordered. The probability of $\varphi$ is the probability of the event that it holds, under the product distribution of the facts.

Concept map

12 concepts; 8 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Group.Finset.Basic
2	import Mathlib.Algebra.BigOperators.Pi
3	import Mathlib.Algebra.BigOperators.Ring.Finset
4	import Mathlib.Algebra.BigOperators.Field
5	import Mathlib.Algebra.Order.BigOperators.Group.Finset
6	import Mathlib.Algebra.Order.BigOperators.Ring.Finset
7	import Mathlib.Algebra.Order.Ring.Rat
8	import Mathlib.Algebra.Order.Field.Basic
9	import Mathlib.Data.Fintype.Pi
10	import Mathlib.Tactic.Linarith
11	import Mathlib.Tactic.FieldSimp
12	import Mathlib.Tactic.Ring
13	import Mathlib.Algebra.BigOperators.Finprod
14	import Mathlib.SetTheory.Cardinal.Finite
15	import Mathlib.Data.Set.Finite.Lemmas
16	import Mathlib.Data.Fintype.EquivFin
17	import Mathlib.Data.Set.Card
18	import Mathlib.Logic.Equiv.Prod
19	import Mathlib.Data.Fintype.BigOperators
20	import Mathlib.Algebra.Group.Action.Defs
21	import Mathlib.Tactic.FinCases
22	import Mathlib.Order.PiLex
23	import Mathlib.Data.Prod.Lex
24	import Mathlib.ModelTheory.Order
25	import Mathlib.ModelTheory.Semantics
26	import Mathlib.ModelTheory.Complexity
27	import Mathlib.Logic.Equiv.Fin.Basic
28	import Mathlib.Data.Fintype.Lattice
29	import Mathlib.Data.Finite.Sigma
30	import Mathlib.Order.Lattice.Nat
31	import Mathlib.Data.Fintype.Pigeonhole
32	import Mathlib.Dynamics.FixedPoints.Basic
33	import Mathlib.ModelTheory.Syntax
34	import Mathlib.Data.Fintype.Card
35	import Lax794877.PossibleWorlds
36	import Lax799700.Common
37	import Lax904597.SecondOrder
38	import Lax366625.CountingProblems
39	import Lax904597.Machines
40
41	/-!
42	---
43	title: Weighted possible worlds and the probability of a query
44	type: definition
45	---
46	A weighted instance gives every uncertain fact two weights, written in
47	binary along a linear order of the positions: a weight of presence $a$ and a
48	weight of absence $c$ , the fact being present with probability $a/(a+c)$
49	independently of the others. The weight of a world is the product, over the
50	uncertain facts, of the weight each takes in it. Counting weighted possible
51	worlds is the counting problem whose value is the sum of the weights of the
52	worlds in which a sentence $\varphi$ holds, counted as the number of
53	witnesses that pick, for each uncertain fact, a number below its weight; it
54	is $0$ on an instance whose positions are not linearly ordered. The
55	probability of $\varphi$ is the probability of the event that it holds,
56	under the product distribution of the facts.
57	-/
58
59	namespace Lax794877.WeightedWorlds
60
61	open Lax794877.PossibleWorlds Lax799700.Common Lax904597.SecondOrder
62
63	variable {X : Type} [Fintype X] [DecidableEq X]
64
65	/-- A probability assignment to a finite set `X` of Boolean variables: each
66	variable is assigned a rational probability in `[0, 1]`. -/
67	structure ProbAssignment (X : Type) where
68	/-- The probability assigned to each variable. -/
69	prob : X → ℚ
70	/-- Probabilities are non-negative. -/
71	prob_nonneg : ∀ x, 0 ≤ prob x
72	/-- Probabilities are at most `1`. -/
73	prob_le_one : ∀ x, prob x ≤ 1
74
75	namespace ProbAssignment
76
77	variable (P : ProbAssignment X)
78
79	/-- Probability of a single valuation `v : X → Bool`, under the independence
80	assumption: `Pr(v) = ∏_{v(x)=⊤} Pr(x) · ∏_{v(x)=⊥} (1 - Pr(x))`. -/
81	def valProb (v : X → Bool) : ℚ :=
82	∏ x, if v x then P.prob x else 1 - P.prob x
83
84	/-- Probability of an event, a Boolean function of the valuation:
85	`Pr(f) = ∑_{v ⊨ f} Pr(v)`. -/
86	def funcProb (f : (X → Bool) → Bool) : ℚ :=
87	∑ v : X → Bool, if f v then P.valProb v else 0
88
89	end ProbAssignment
90
91	section Weights
92
93	variable (a c : X → ℕ)
94
95	/-- The probability assignment of a family of weights: the variable `x` is
96	true with probability `a x / (a x + c x)`. -/
97	def ProbAssignment.ofWeights (h : ∀ x, 0 < a x + c x) : ProbAssignment X where
98	prob x := (a x : ℚ) / ((a x : ℚ) + c x)
99	prob_nonneg x := div_nonneg (Nat.cast_nonneg _) (add_nonneg (Nat.cast_nonneg _)
100	(Nat.cast_nonneg _))
101	prob_le_one x := by
102	have hpos : (0 : ℚ) < (a x : ℚ) + c x := by exact_mod_cast h x
103	rw [div_le_one hpos]
104	have : (0 : ℚ) ≤ c x := Nat.cast_nonneg _
105	linarith
106
107	end Weights
108
109	open FirstOrder
110
111	open Language Structure
112
113	/-- The relation symbols of a weighted instance over the schema `L`: for each
114	symbol of the schema, the certain facts, the uncertain facts, and the bits of
115	the two weights of each fact; and one order, on the bit positions. -/
116	inductive WeightedRel (L : Language.{0, 0}) : ℕ → Type
117	/-- The certain facts. -/
118	\| cert {n : ℕ} (R : L.Relations n) : WeightedRel L n
119	/-- The uncertain facts. -/
120	\| unc {n : ℕ} (R : L.Relations n) : WeightedRel L n
121	/-- `pres R (x̄, i)`: the bit of position `i` of the weight of the fact `R(x̄)`
122	being present. -/
123	\| pres {n : ℕ} (R : L.Relations n) : WeightedRel L (n + 1)
124	/-- `abs R (x̄, i)`: the bit of position `i` of the weight of the fact `R(x̄)`
125	being absent. -/
126	\| abs {n : ℕ} (R : L.Relations n) : WeightedRel L (n + 1)
127	/-- The order of the bit positions. -/
128	\| le : WeightedRel L 2
129
130	/-- The vocabulary of weighted instances over the schema `L`. -/
131	def weightedLang (L : Language.{0, 0}) : Language.{0, 0} :=
132	⟨fun _ => Empty, WeightedRel L⟩
133
134	instance (L : Language.{0, 0}) : (weightedLang L).IsRelational :=
135	fun _ => inferInstanceAs (IsEmpty Empty)
136
137	variable {L : Language.{0, 0}} [Finite (Σ n, L.Relations n)]
138
139	/-- The block guessing a weighted world: a world, and for each fact a number,
140	as the set of its bits. -/
141	def weightBlock (L : Language.{0, 0}) [Finite (Σ n, L.Relations n)] : SOBlock where
142	ι := (Σ n, L.Relations n) ⊕ (Σ n, L.Relations n)
143	arity := Sum.elim (fun p => p.1) fun p => p.1 + 1
144
145	section Kernel
146
147	variable {A : Type} [(weightedLang L).Structure A]
148
149	/-- The world of an assignment of the block. -/
150	def worldOf (σ : (weightBlock L).Assignment A) : (worldBlock L).Assignment A :=
151	fun p x => σ (Sum.inl p) x
152
153	/-- The number an assignment of the block attaches to a fact, as its set of
154	bits. -/
155	def numOf (σ : (weightBlock L).Assignment A) (p : Σ n, L.Relations n) (x : Fin p.1 → A) :
156	A → Prop :=
157	fun i => σ (Sum.inr p) (Fin.snoc (α := fun _ => A) x i)
158
159	/-- The bits of a weight of a fact, read through a symbol of arity one more
160	than the fact's. -/
161	def bitsOf {n : ℕ} (S : WeightedRel L (n + 1)) (x : Fin n → A) : A → Prop :=
162	fun i => RelMap (L := weightedLang L) S (Fin.snoc (α := fun _ => A) x i)
163
164	/-- The order of the positions of a weighted instance. -/
165	def WLe (L : Language.{0, 0}) (A : Type) [(weightedLang L).Structure A] (a b : A) : Prop :=
166	RelMap (L := weightedLang L) WeightedRel.le ![a, b]
167
168	/-- One set of bits is below another, by the highest position at which they
169	differ. -/
170	def BitLt (Le : A → A → Prop) (b w : A → Prop) : Prop :=
171	∃ i, w i ∧ ¬b i ∧ ∀ j, Le i j → j ≠ i → (b j ↔ w j)
172
173	/-- What the kernel asks of an assignment at one fact: the world keeps a
174	certain fact and contains only certain or uncertain ones; at an open fact –
175	uncertain and not certain – the number is below the weight of presence if the
176	world keeps the fact, and below the weight of absence if not; at any other
177	fact the number is zero. -/
178	def WeightCond (σ : (weightBlock L).Assignment A) (p : Σ n, L.Relations n)
179	(x : Fin p.1 → A) : Prop :=
180	((RelMap (L := weightedLang L) (WeightedRel.cert p.2) x → worldOf σ p x) ∧
181	(worldOf σ p x → RelMap (L := weightedLang L) (WeightedRel.cert p.2) x ∨
182	RelMap (L := weightedLang L) (WeightedRel.unc p.2) x)) ∧
183	((RelMap (L := weightedLang L) (WeightedRel.unc p.2) x ∧
184	¬RelMap (L := weightedLang L) (WeightedRel.cert p.2) x →
185	(worldOf σ p x →
186	BitLt (WLe L A) (numOf σ p x) (bitsOf (WeightedRel.pres p.2) x)) ∧
187	(¬worldOf σ p x →
188	BitLt (WLe L A) (numOf σ p x) (bitsOf (WeightedRel.abs p.2) x))) ∧
189	(¬(RelMap (L := weightedLang L) (WeightedRel.unc p.2) x ∧
190	¬RelMap (L := weightedLang L) (WeightedRel.cert p.2) x) →
191	∀ i, ¬numOf σ p x i))
192
193	end Kernel
194
195	section Count
196
197	variable [L.IsRelational] {A : Type} [(weightedLang L).Structure A]
198
199	/-- The facts over a universe: a symbol of the schema and a tuple. -/
200	abbrev Fact (L : Language.{0, 0}) (A : Type) : Type := Σ p : Σ n, L.Relations n, Fin p.1 → A
201
202	/-- The fact is open: uncertain and not certain. -/
203	def IsOpen (q : Fact L A) : Prop :=
204	RelMap (L := weightedLang L) (WeightedRel.unc q.1.2) q.2 ∧
205	¬RelMap (L := weightedLang L) (WeightedRel.cert q.1.2) q.2
206
207	/-- The open facts of a finite instance, as a finite type: the independent
208	Boolean variables of the instance. -/
209	noncomputable instance openFactFintype [Finite A] : Fintype {q : Fact L A // IsOpen q} :=
210	Fintype.ofFinite _
211
212	/-- The weight of presence of an open fact. -/
213	noncomputable def presWeight (x : {q : Fact L A // IsOpen q}) : ℕ :=
214	binNum (WLe L A) (fun _ => True) (bitsOf (WeightedRel.pres x.1.1.2) x.1.2)
215
216	/-- The weight of absence of an open fact. -/
217	noncomputable def absWeight (x : {q : Fact L A // IsOpen q}) : ℕ :=
218	binNum (WLe L A) (fun _ => True) (bitsOf (WeightedRel.abs x.1.1.2) x.1.2)
219
220	/-- The world of a valuation of the open facts: the certain facts, and the
221	open facts the valuation makes true. -/
222	def worldOfVal (v : {q : Fact L A // IsOpen q} → Bool) : (worldBlock L).Assignment A :=
223	fun p x => RelMap (L := weightedLang L) (WeightedRel.cert p.2) x ∨
224	∃ h : IsOpen (⟨p, x⟩ : Fact L A), v ⟨⟨p, x⟩, h⟩ = true
225
226	open Classical in
227	/-- The event “the sentence holds in the world”, as a Boolean function of the
228	valuation of the open facts. -/
229	noncomputable def holdsEvent (φ : L.Sentence) (v : {q : Fact L A // IsOpen q} → Bool) : Bool :=
230	decide (@Sentence.Realize L A (worldStructure (worldOfVal v)) φ)
231
232	open Classical in
233	/-- The probability of a sentence over a weighted instance: each open fact
234	is present independently, with probability its weight of presence over the sum
235	of its two weights, and the probability is that of the event that the sentence
236	holds in the resulting world. -/
237	noncomputable def worldProb [Finite A] (φ : L.Sentence)
238	(hpos : ∀ x : {q : Fact L A // IsOpen q}, 0 < presWeight x + absWeight x) : ℚ :=
239	(ProbAssignment.ofWeights presWeight absWeight hpos).funcProb (holdsEvent φ)
240
241	end Count
242
243	open Lax366625.CountingProblems Lax904597.Machines
244
245	/-- Counting weighted possible worlds: the witnesses are the worlds in which
246	the sentence `φ` holds, each with one number per open fact below the weight
247	that fact takes in the world. -/
248	noncomputable def WeightedWorlds {L : Language.{0, 0}} [Finite
249	(Σ n, L.Relations n)] [L.IsRelational]
250	(φ : L.Sentence) : CountingProblem (weightedLang L) :=
251	CountingProblem.ofFun fun A _ =>
252	Nat.card {σ : (weightBlock L).Assignment A // IsLinOrd (WLe L A) ∧
253	(∀ (p : Σ n, L.Relations n) (x : Fin p.1 → A), WeightCond σ p x) ∧
254	@Sentence.Realize L A (worldStructure (worldOf σ)) φ}
255
256	end Lax794877.WeightedWorlds
257

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

Weighted possible worlds and the probability of a query

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments