Independent edge coins: deferred decisions and symmetry (EPI-3)

Facts about finite distributions and the i.i.d. Bernoulli(p) coins coins p of Epidemics.ReedFrost, used in the proof of the supercritical giant component (Krivelevich–Sudakov, The phase transition in random graphs: a simple proof, Random Structures & Algorithms 43 (2013), arXiv:1201.6529).

• Elementary bounds on Distribution.prob: monotonicity, complement, union bounds.
• Cylinders: the probability that the independent coordinates c 0, …, c (m-1) (distinct) take prescribed values is the product of their weights (prob_forall_eval_eq).
• Principle of deferred decisions. Krivelevich and Sudakov run the depth-first search "fed with a sequence of i.i.d. Bernoulli(p) random variables X̄" and observe that "the so obtained graph is clearly distributed according to G(n, p)" (Section 2). Here the coins come first: an adaptive strategy queries the coordinates of ω : ι → Bool one at a time, the next coordinate being a function of the answers so far. As long as no coordinate is queried twice, the answers are i.i.d. Bernoulli(p) (expect_queryAnswers, prob_queryAnswers). The proof: the answers equal a given list L iff the coordinates queried along L, which are determined by L, take the values of L, a cylinder event.
• Symmetry: relabelling the vertices does not change the law of the coins (coins_prob_perm).

coins is built from Epidemics.bernoulli, which coincides with the coin Dynamics.Distribution.bernoulli of the Chernoff bounds (FND-3): coins_eq_independent.

theorem Epidemics.coins_eq_independent {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) : coins p h0 h1 = Dynamics.Distribution.independent fun (x : Sym2 V) => Dynamics.Distribution.bernoulli p h0 h1

The edge coins are the independent Bernoulli coins of the Chernoff bounds (FND-3).

Elementary bounds on probabilities

Monotonicity and the expectation form of prob are the core's Distribution.prob_mono and Distribution.prob_eq_expect. The bounds below are not in dynamics/ yet (their move there is tracked in issue #42).

theorem Epidemics.prob_congr {α : Type u_1} [Fintype α] (P : Dynamics.Distribution α) {A B : α → Prop} (h : ∀ (a : α), A a ↔ B a) : P.prob A = P.prob B

theorem Epidemics.prob_not {α : Type u_1} [Fintype α] (P : Dynamics.Distribution α) (A : α → Prop) : (P.prob fun (a : α) => ¬A a) = 1 - P.prob A

theorem Epidemics.prob_or_le {α : Type u_1} [Fintype α] (P : Dynamics.Distribution α) (A B : α → Prop) : (P.prob fun (a : α) => A a ∨ B a) ≤ P.prob A + P.prob B

theorem Epidemics.prob_exists_le_sum {α : Type u_1} [Fintype α] {ι : Type u_2} (P : Dynamics.Distribution α) (s : Finset ι) (A : ι → α → Prop) : (P.prob fun (a : α) => ∃ i ∈ s, A i a) ≤ ∑ i ∈ s, P.prob (A i)

theorem Epidemics.one_sub_le_prob {α : Type u_1} [Fintype α] (P : Dynamics.Distribution α) {A B : α → Prop} (h : ∀ (a : α), B a → A a) {ε : ℝ} (hB : (P.prob fun (a : α) => ¬B a) ≤ ε) : 1 - ε ≤ P.prob A

If B fails with probability at most ε and implies A, then A has probability at least 1 - ε.

Cylinders

theorem Epidemics.prob_forall_eval_eq {ι : Type u_1} {α : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype α] (P : ι → Dynamics.Distribution α) {m : ℕ} {c : Fin m → ι} (hc : Function.Injective c) (x : Fin m → α) : ((Dynamics.Distribution.independent P).prob fun (ω : ι → α) => ∀ (k : Fin m), ω (c k) = x k) = ∏ k : Fin m, (P (c k)).weight (x k)

Cylinders: if the coordinates c 0, …, c (m-1) are distinct, the probability that they take the values x 0, …, x (m-1) under an independent product is the product of the weights.

Adaptive queries

def Epidemics.queryAnswers {ι : Type u_1} (next : List Bool → ι) (ω : ι → Bool) : ℕ → List Bool

The answers to the first t queries of the adaptive strategy next on the coins ω, in order: after the answers l, the next query is the coordinate next l.

Equations

• Epidemics.queryAnswers next ω 0 = []
• Epidemics.queryAnswers next ω t.succ = Epidemics.queryAnswers next ω t ++ [ω (next (Epidemics.queryAnswers next ω t))]

def Epidemics.FreshUpTo {ι : Type u_1} (next : List Bool → ι) (m : ℕ) : Prop

The strategy next never queries a coordinate twice among its first m queries: after any k < m answers, the next coordinate differs from the k coordinates queried before.

Equations

• Epidemics.FreshUpTo next m = ∀ (l : List Bool), l.length < m → ∀ j < l.length, next (List.take j l) ≠ next l

theorem Epidemics.FreshUpTo.mono {ι : Type u_1} {next : List Bool → ι} {m m' : ℕ} (h : FreshUpTo next m) (hm : m' ≤ m) : FreshUpTo next m'

theorem Epidemics.length_queryAnswers {ι : Type u_1} (next : List Bool → ι) (ω : ι → Bool) (t : ℕ) : (queryAnswers next ω t).length = t

theorem Epidemics.take_queryAnswers {ι : Type u_1} (next : List Bool → ι) (ω : ι → Bool) {s t : ℕ} (hst : s ≤ t) : List.take s (queryAnswers next ω t) = queryAnswers next ω s

theorem Epidemics.queryAnswers_eq_iff {ι : Type u_1} (next : List Bool → ι) (ω : ι → Bool) (L : List Bool) : queryAnswers next ω L.length = L ↔ ∀ k < L.length, some (ω (next (List.take k L))) = L[k]?

The answers are a given list L iff the coordinates queried along L take its values.

theorem Epidemics.prob_queryAnswers_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (next : List Bool → ι) {m : ℕ} (hfresh : FreshUpTo next m) (x : Fin m → Bool) : ((Dynamics.Distribution.independent fun (x : ι) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (ω : ι → Bool) => queryAnswers next ω m = List.ofFn x) = ∏ k : Fin m, (Dynamics.Distribution.bernoulli p h0 h1).weight (x k)

The answers to a fresh strategy form a cylinder: they equal L with probability ∏ₖ w(Lₖ).

theorem Epidemics.expect_queryAnswers {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (next : List Bool → ι) {m : ℕ} (hfresh : FreshUpTo next m) (F : List Bool → ℝ) : ((Dynamics.Distribution.independent fun (x : ι) => Dynamics.Distribution.bernoulli p h0 h1).expect fun (ω : ι → Bool) => F (queryAnswers next ω m)) = (Dynamics.Distribution.independent fun (x : Fin m) => Dynamics.Distribution.bernoulli p h0 h1).expect fun (x : Fin m → Bool) => F (List.ofFn x)

Principle of deferred decisions (the coupling behind Krivelevich–Sudakov, Section 2): if the strategy next is fresh for m queries, its first m answers on i.i.d. Bernoulli(p) coins are distributed as m i.i.d. Bernoulli(p) trials.

theorem Epidemics.prob_queryAnswers {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (next : List Bool → ι) {m : ℕ} (hfresh : FreshUpTo next m) (E : List Bool → Prop) : ((Dynamics.Distribution.independent fun (x : ι) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (ω : ι → Bool) => E (queryAnswers next ω m)) = (Dynamics.Distribution.independent fun (x : Fin m) => Dynamics.Distribution.bernoulli p h0 h1).prob fun (x : Fin m → Bool) => E (List.ofFn x)

The principle of deferred decisions for events.

Symmetry

def Epidemics.permSym2 {V : Type u_1} (σ : Equiv.Perm V) : Equiv.Perm (Sym2 V)

A permutation of the vertices permutes the pairs.

Equations

• Epidemics.permSym2 σ = { toFun := Sym2.map ⇑σ, invFun := Sym2.map ⇑(Equiv.symm σ), left_inv := ⋯, right_inv := ⋯ }

theorem Epidemics.coins_prob_perm {V : Type u_1} [Fintype V] [DecidableEq V] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (σ : Equiv.Perm V) (E : (Sym2 V → Bool) → Prop) : ((coins p h0 h1).prob fun (ω : Sym2 V → Bool) => E fun (e : Sym2 V) => ω (Sym2.map (⇑σ) e)) = (coins p h0 h1).prob E

Symmetry: relabelling the vertices by a permutation σ preserves the law of the coins.