Collision and length bounds for independently sampled paths

Lax263307.PathSampling · concepts/Lax263307/PathSampling.lean · lax-263307

proven

Loading review…

Natural Language Statement

Theorem

Let $Q$ be a random vertex set and let $q_v=\Pr[v\in Q]$ . Two independent samples intersect with probability at most $\sum_v q_v^2$ . The probability that an edge joins their vertex sets is at most the ordered adjacency mass $\sum_{uv\in E(G)}2q_uq_v$ . Also $\mathbb E[|Q|]=\sum_vq_v$ .

Consequently, if $q_v\le\ell x_v/k$ , $0\le x_v\le1$ , $\sum_vx_v\le k$ with $k>0$ , and $e_G(x)\le k^2/p$ with $p>0$ , these bounds are respectively $\ell^2/k$ , $2\ell^2/p$ , and $\ell$ .

Concept map

2 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

Evidence

This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

Show types on hover

1	import Lax263307.Entropy
2	import Mathlib.Data.Finset.Card
3
4	/-!
5	---
6	title: Collision and length bounds for independently sampled paths
7	type: theorem
8	---
9	Let $Q$ be a random vertex set and let $q_v=\Pr[v\in Q]$ . Two independent
10	samples intersect with probability at most $\sum_v q_v^2$ . The probability
11	that an edge joins their vertex sets is at most the ordered adjacency mass
12	$\sum_{uv\in E(G)}2q_uq_v$ . Also $\mathbb E[\|Q\|]=\sum_vq_v$ .
13
14	Consequently, if $q_v\le\ell x_v/k$ , $0\le x_v\le1$ , $\sum_vx_v\le k$ with $k>0$ ,
15	and $e_G(x)\le k^2/p$ with $p>0$ , these bounds are respectively
16	$\ell^2/k$ , $2\ell^2/p$ , and $\ell$ .
17
18	# Formalization notes
19
20	A finite distribution is given explicitly by its outcome probabilities.
21	The pair probabilities are products, expressing independent sampling.
22	The estimates depend only on the vertex sets of the sampled paths, so the
23	definitions allow arbitrary finite vertex sets.
24
25	# Attribution
26
27	Bonnet–Chang, equations (8), (9), and the expected-path-size bound in Lemma 11.
28	-/
29
30	namespace Lax263307.PathSampling
31
32	/-- Finite outcome probabilities and their associated vertex sets. -/
33	structure Distribution (n q : ℕ) where
34	/-- Probability of each outcome. -/
35	probability : Fin q → ℝ
36	/-- Probabilities are nonnegative. -/
37	nonnegative : ∀ i, 0 ≤ probability i
38	/-- Total probability is one. -/
39	normalized : (∑ i, probability i) = 1
40	/-- The vertices used by each outcome. -/
41	vertices : Fin q → Finset (Fin n)
42
43	/-- Probability of using a particular vertex. -/
44	noncomputable def load {n q : ℕ} (P : Distribution n q) (v : Fin n) : ℝ :=
45	∑ i, if v ∈ P.vertices i then P.probability i else 0
46
47	/-- Expected number of used vertices. -/
48	noncomputable def expectedSize {n q : ℕ} (P : Distribution n q) : ℝ :=
49	∑ i, P.probability i * ((P.vertices i).card : ℝ)
50
51	/-- Probability that independent outcomes have a common vertex. -/
52	noncomputable def collisionProbability {n q : ℕ} (P : Distribution n q) : ℝ :=
53	∑ i, ∑ j, if ¬Disjoint (P.vertices i) (P.vertices j) then
54	P.probability i * P.probability j else 0
55
56	/-- Probability that a graph edge joins independent outcomes. -/
57	noncomputable def adjacencyProbability {n q : ℕ} (G : SimpleGraph (Fin n))
58	[DecidableRel G.Adj] (P : Distribution n q) : ℝ :=
59	∑ i, ∑ j, if ∃ u ∈ P.vertices i, ∃ v ∈ P.vertices j, G.Adj u v then
60	P.probability i * P.probability j else 0
61
62	/-- Sum of vertex-use probabilities equals expected size. -/
63	axiom expected_size_identity {n q : ℕ} (P : Distribution n q) :
64	expectedSize P = ∑ v, load P v
65
66	/-- The union bound for intersection of two independent samples. -/
67	axiom collision_union_bound {n q : ℕ} (P : Distribution n q) :
68	collisionProbability P ≤ ∑ v, (load P v) ^ 2
69
70	/-- The union bound for edges joining two independent samples. -/
71	axiom adjacency_union_bound {n q : ℕ} (G : SimpleGraph (Fin n))
72	[DecidableRel G.Adj] (P : Distribution n q) :
73	adjacencyProbability G P ≤ Entropy.adjacencyMass G (load P)
74
75	/-- The load hypotheses imply the three estimates used in sampling. -/
76	axiom sampling_bounds {n q : ℕ} (G : SimpleGraph (Fin n))
77	[DecidableRel G.Adj] (P : Distribution n q) (x : Fin n → ℝ) (k ℓ p : ℝ)
78	(k_positive : 0 < k) (ℓ_nonnegative : 0 ≤ ℓ) (p_positive : 0 < p)
79	(cost_bounds : ∀ v, 0 ≤ x v ∧ x v ≤ 1) (mass : (∑ v, x v) ≤ k)
80	(load_bound : ∀ v, load P v ≤ ℓ * x v / k)
81	(edge_bound : Entropy.edgeCost G x ≤ k ^ 2 / p) :
82	collisionProbability P ≤ ℓ ^ 2 / k ∧
83	adjacencyProbability G P ≤ 2 * ℓ ^ 2 / p ∧ expectedSize P ≤ ℓ
84
85	end Lax263307.PathSampling
86

Show ProofShow ProofShow ProofShow Proof

Formalization notes

A finite distribution is given explicitly by its outcome probabilities. The pair probabilities are products, expressing independent sampling. The estimates depend only on the vertex sets of the sampled paths, so the definitions allow arbitrary finite vertex sets.

Attribution

Bonnet–Chang, equations (8), (9), and the expected-path-size bound in Lemma 11.

Builds on

Lax263307.Entropy

Used by

From Mathlib

Mathlib.Data.Finset.Card

Discussion

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

Loading discussion…

Lax Lean Archive

Collision and length bounds for independently sampled paths

Flags

Flag this concept

Natural Language Statement

Theorem

1 `adjacency_union_bound` proven

2 `collision_union_bound` proven

3 `expected_size_identity` proven

4 `sampling_bounds` proven

Lean source view on GitHub

Attribution

Discussion

Settings

Your comments

Collision and length bounds for independently sampled paths

Natural Language Statement

Theorem

1 adjacency_union_bound proven

2 collision_union_bound proven

3 expected_size_identity proven

4 sampling_bounds proven

Lean source view on GitHub

Attribution

Discussion

1 `adjacency_union_bound` proven

2 `collision_union_bound` proven

3 `expected_size_identity` proven

4 `sampling_bounds` proven