Dependencies

For a finite type \(\alpha \) and \(f \colon \alpha \to \mathbb {R}\), \(\mathrm{avg}(f) := \bigl(\sum _{a} f(a)\bigr) / |\alpha |\) is the expectation of \(f\) under the uniform distribution on \(\alpha \).

For a finite type \(\alpha \), \(\mathrm{expList}\ \alpha \ T\ F\) is the expectation of a functional \(F\) of a trajectory of \(T\) i.i.d. uniform draws from \(\alpha \), defined by recursion on \(T\): the head draw is averaged out first, i.e. \(\mathrm{expList}\ \alpha \ 0\ F = F(\, []\, )\) and \(\mathrm{expList}\ \alpha \ (T{+}1)\ F = \mathrm{avg}\bigl(a \mapsto \mathrm{expList}\ \alpha \ T\ (l \mapsto F(a :: l))\bigr)\). This makes “conditioning on the first round” a definitional unfolding rather than a measure-theoretic construction.

A round is good if it multiplies the informed set by \(\ge 9/8\), or if the informed set already exceeds \(n/2\):

\(\mathrm{goodCount}\) counts the good rounds along a trajectory. By Lemma 20 (applied when \(m_t \le n/2\); trivial otherwise), \(\Pr [X_t = 1 \mid \omega _0,\dots ,\omega _{t-1}] \ge \tfrac 18\) for every prefix, since \(\omega _t\) is independent of the prefix and \(\mathrm{expList}\) conditions on it definitionally.

Fix a horizon \(T \in \mathbb {N}\) and a start vertex \(v_0 \in V\). The sample space is \(\Omega = R_n^{\, T}\) (uniform measure, i.e. i.i.d. uniform rounds). For \(\omega = (\omega _0,\dots ,\omega _{T-1}) \in \Omega \) define \(I_0(\omega ) = \{ v_0\} \) and \(I_{t+1}(\omega ) = \mathrm{step}(I_t(\omega ), \omega _t)\) for \(0 \le t {\lt} T\). We write \(m_t = |I_t|\) and \(U_t = n - m_t\) for the numbers of informed and uninformed nodes. Since \(\Omega \) is finite, all probabilities are finite ratios and all expectations are finite sums; “conditioning on \(I_t\)” means partitioning \(\Omega \) according to the first \(t\) coordinates. In the formalization, a trajectory is simply a List of round configurations and \(\mathrm{run}\ I\ l\) folds step over the list \(l\).

\(\mathrm{pullStep}(I,\omega ) = I \cup \{ v : \omega (v) \in I\} \) and \(\mathrm{pushPullStep}(I,\omega ) = \mathrm{step}(I,\omega ) \cup \mathrm{pullStep}(I,\omega )\); trajectories fold these steps over a list of i.i.d. uniform rounds, and the failure probabilities are the probabilities that some node is still uninformed after \(T\) rounds started from \(\{ v_0\} \).

A round configuration is a function \(\omega \colon V \to V\) with \(\omega (v) \ne v\) for all \(v\). Let \(R_n\) denote the (finite) set of round configurations; it carries the uniform probability measure, i.e. every node picks a uniformly random target among the other \(n-1\) nodes, independently of all other nodes.

For an informed set \(I \subseteq V\) and a round configuration \(\omega \in R_n\), the next informed set is

(Only informed nodes actually transmit; letting all nodes draw a target and ignoring the choices of uninformed nodes is an equivalent and formalization-friendlier convention.)

For every \(T\) and every nonempty \(I\),

over \(T\) rounds started at \(I\). (This specializes the textbook “\(\mathbb {E}[s^G] \le (1-p(1-s))^T\) for adaptive \(\{ 0,1\} \)-trials with per-step success probability \(\ge p\)” at \(p = 1/8\), \(s = 1/2\); the formalization proves the specialized statement directly by induction on \(T\) rather than the general one, since only this instance is needed. The ensuing tail bound \(\Pr [G {\lt} L] \le 2^{L}(15/16)^{T}\) — via \(s^{L}\Pr [G{\lt}L] \le \mathbb {E}[s^G]\) — is likewise not isolated as a separate lemma; it is proved inline inside Lemma 25 (phase1).

\(|I_{t+1}(\omega ) \smallsetminus I_t(\omega )| \le |I_t(\omega )|\); equivalently \((\mathrm{step}(I,\omega )).\mathrm{card} \le 2\, I.\mathrm{card}\).

\(\mathrm{avg}\) and \(\mathrm{expList}\) are monotone, additive, and homogeneous, and constants pass through unchanged. These pointwise inequalities pushed through \(\mathrm{avg\_ le\_ avg}\) / \(\mathrm{expList\_ le\_ expList}\) are the only form in which Markov’s inequality and union bounds are used below (Lemmas 16 and 17); they are not separately formalized lemmas.

For all real \(y \ge -1\) (we only use \(y\in [-1,1]\)) and \(m \in \mathbb {N}\): \((1+y)^m \ge 1 + my\). Equivalently, with \(y = -x\): \(1 - mx \le (1-x)^m\).

For \(0 \le x \le 1\) and \(m \in \mathbb {N}\):

and consequently \(mx/2 \le 1-(1-x)^m\) whenever \(mx \le 1\).

With \(L = \left\lceil 9 \log n \right\rceil + 1\) we have \((9/8)^L \ge n\) (numeric_A), and with \(T_1 = \left\lceil 117 \log n \right\rceil + 23\) we have \(2^{L}(15/16)^{T_1} \le 1/n\) (numeric_B), using \(\log \tfrac 98 \ge \tfrac 19\), \(\log \tfrac {16}{15} \ge \tfrac 1{16}\) and \(\log 2 {\lt} 0.6932\). Combined with Lemma 25: \(\Pr [m_{T_1} \le n/2] \le 1/n\). The clean statement to formalize is that any \(L, T_1\) satisfying these two numeric inequalities work; the values above merely exhibit admissible ones.

For any fixed \(u \notin I\),

The Lean proof is the only place where a probability is computed rather than estimated: it counts round configurations avoiding \(u\) on \(I\) via an explicit equivalence to a product of subtypes and Fintype.card_pi.

If \(m \ge n/2\), then for every fixed \(u \notin I\), \(\Pr _\omega [u \notin \mathrm{step}(I,\omega )] = (1-x)^m \le \tfrac 23\), and consequently, with \(U' := n - |\mathrm{step}(I,\omega )|\), \(\mathbb {E}_\omega [U'] \le \tfrac 23(n-m)\).

Let \(N(\omega ) = |\mathrm{step}(I,\omega )| - m\) be the number of newly informed nodes. The formalization gives the exact formula

from which, if \(1 \le m \le n/2\): \(\mathbb {E}_\omega [N] \ge m/4\) (using Lemma 13 and \(n - m \ge n/2\), \(mx \le 1\)).

Let \(L \in \mathbb {N}\) satisfy \((9/8)^L {\gt} n/2\). If the informed set never exceeds \(n/2\) up to time \(T_1\), then along that trajectory \(m_{T_1} \ge (9/8)^{\mathrm{goodCount}} \cdot m_0\): every good round multiplies \(m_t\) by \(\ge 9/8\) and every round is non-decreasing (Lemma 4), so \(\mathrm{goodCount} \ge L\) would force \(m_{T_1} {\gt} n/2\), a contradiction — hence \(\mathrm{goodCount} {\lt} L \Rightarrow m_{T_1} \le n/2\) is impossible to rule out only via the deterministic growth bound stated here.

Let \(\mathrm{prNotAllInformed}(n,v_0,T)\) be the probability that some node is still uninformed after \(T\) rounds started at \(v_0\). For all \(L, T_1, T_2\) with \((9/8)^L \le n\):

Failure requires either phase 1 to fail (informed set still \(\le n/2\) after \(T_1\) rounds, Lemma 25) or phase 2 to leave an uninformed node on the complementary event, controlled by Lemma 27 via Markov.

If \(1 \le m \le n/2\), then \(\Pr _\omega \bigl[\, |\mathrm{step}(I,\omega )| \ge \tfrac {9}{8}\, m\, \bigr] \ge \tfrac 18\).

For \(x {\gt} 0\): \(1 - \tfrac 1x \le \log x\). (The formalization only needs this left inequality, applied at \(x = 9/8,\ 16/15,\ 3/2\), together with Mathlib’s numeric bound \(\log 2 {\lt} 0.6931471808\).)

Let \(\Omega \) be a finite nonempty set with the uniform measure, \(f \colon \Omega \to \mathbb {R}\) with \(f \ge 0\), and \(a {\gt} 0\). Then \(\Pr [f \ge a] \le \mathbb {E}[f]/a\). In particular, if \(f\) takes values in \(\mathbb {N}\), then \(\Pr [f \ne 0] \le \mathbb {E}[f]\).

\(I_t(\omega ) \subseteq I_{t+1}(\omega )\) for all \(t\) and all \(\omega \); hence \(m_t\) is non-decreasing and \(U_t\) is non-increasing in \(t\), pointwise on \(\Omega \).

If \((9/8)^L \ge n\), then after \(T_1\) rounds the informed set is still \(\le n/2\) with probability at most \(2^{L}\, (15/16)^{T_1}\).

Let \(A = \{ m_{T_1} {\gt} n/2\} \) (an event determined by the first \(T_1\) coordinates). Then for every \(s \ge 0\), \(\mathbb {E}\bigl[\, U_{T_1 + s}\, \mathbf{1}_A \, \bigr] \le (2/3)^{s}\, n\), by induction on \(s\) using Lemma 21 at each step (monotonicity keeps \(m_{T_1+s} {\gt} n/2\) on \(A\)).

With \(T_2 = \left\lceil 6 \log n \right\rceil \): \(\Pr [\, U_T \ge 1 \text{ and } A \, ] \le n\, (2/3)^{T_2} \le 1/n\). (\(U_T\) is \(\mathbb {N}\)-valued, so Markov applied to \(U_T \mathbf{1}_A\) and Lemma 27 give the first inequality; \((2/3)^{T_2} n \le 1/n\) — numeric_C — follows from \(\log \tfrac 32 \ge \tfrac 13\) and \(T_2 \ge 6\log n\).)

With the same calls, the PUSH–PULL informed set contains the PUSH and the PULL informed sets after every number of rounds.

A PULL round is good with probability at least \(1/8\), and for \(|I| \ge n/2\) it contracts the expected uninformed count by \(2/3\).

The calls \(\omega (v)\), \(v \in V\), of a uniform round are independent, each uniform among the other \(n-1\) nodes; in particular a caller \(v \notin I\) calls into \(I\) with probability \(|I|/(n-1)\).

Let \(m = |I|\) and \(u = n - m\). From a single informed node a PULL round informs nobody with probability \((1 - \frac1{n-1})^{n-1}\). After one PULL round, \(\mathbb {E}|I'| = m + u\, \frac{m}{n-1}\) and \(\mathbb {E}[n - |I'|] = \frac{u(u-1)}{n-1} \le \frac{u^2}{n}\) (quadratic shrinking). After one PUSH–PULL round, \(\mathbb {E}[n - |I'|] = \frac{u(u-1)}{n-1}\bigl(1 - \frac1{n-1}\bigr)^{m}\).

Let \(f(I,a) \supseteq I\) be a spreading step driven by i.i.d. uniform rounds \(a\). Suppose that from every nonempty \(I\) a round is good (\(|f(I,a)| \ge \frac98 |I|\), or \(|I| {\gt} n/2\)) with probability at least \(1/8\), and that for \(|I| \ge n/2\) the expected number of uninformed nodes contracts by \(2/3\). Then after \(\left\lceil 160 \log n \right\rceil \) rounds from \(\{ v_0\} \), some node is uninformed with probability at most \(2/n\). The proof is the PUSH proof of Sections 6–9, which uses no other property of \(\mathrm{step}\).

Let \(f \colon \Omega \to \mathbb {R}\) with \(0 \le f \le b\) pointwise, \(b {\gt} 0\), and let \(0 {\lt} a {\lt} b\). Then \(\Pr [f \ge a] \ge \dfrac {\mathbb {E}[f] - a}{b}\). (As with Lemma 16, the formalization does not isolate this as a named lemma: each use site supplies its own pointwise bound and pushes it through \(\mathrm{avg\_ le\_ avg}\), e.g. in the proof of Lemma 20.)

For \(0 \le x \le 1\) and \(m \in \mathbb {N}\): \((1-x)^m \le \dfrac {1}{1+mx}\).

\(\mathrm{expList}\ \alpha \ T\ F\) equals the uniform average of \(F\) over all length-\(T\) sequences of draws, i.e. over the product probability space \(\mathrm{Fin}\ T \to \alpha \) of \(T\) i.i.d. uniform rounds. This confirms that the recursive definition of Definition 9 is the textbook object.

Let \(n \ge 2\), let \(v_0 \in V\), and set

Then \(\Pr \bigl[\, I_T = V \, \bigr] \; \ge \; 1 - \frac{2}{n}\). In particular all nodes are informed after \(O(\log n)\) rounds with high probability.

Let \(n \ge 2\) and \(v_0 \in V\). After \(\left\lceil 160 \log n \right\rceil \) rounds of PULL, or of PUSH–PULL, started from \(\{ v_0\} \), all nodes are informed with probability at least \(1 - 2/n\).