- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Nobody is infected in round \(t\) as soon as every finite \(d(v)\) is \({\lt}t\), in particular for \(t\ge |V|\); the nodes recovered after \(|V|\) rounds are those connected to \(I_0\) in \(G_\omega \).
On \(K_n\) with \(pn=R_0{\gt}1\), the Reed–Frost epidemic started from any single node infects at least \(cn\) nodes with probability at least \(q{\gt}0\) for \(n\ge n_0\); for \(R_0=1+\varepsilon \) with \(\varepsilon \) small, at least \(\varepsilon n/2\) nodes with probability at least \(\varepsilon /2-C/n\).
With probability at least \(1 - 1/n\), the Reed–Frost epidemic with \(R_0 = p(d-1) \le 1 - \varepsilon \) infects at most \(|I_0| (10/\varepsilon ^2)\log n\) nodes and nobody is infected in round \(\lfloor (10/\varepsilon ^2)\log n \rfloor \); and every component of \(G(n, c/n)\) with \(c \le 1 - \varepsilon \) has at most \((10/\varepsilon ^2)\log n\) vertices.
In a round \(r\), every vertex \(x\) of a finite graph \(G\) samples \(k\) neighbours \(r(x,0),\dots ,r(x,k-1)\). A uniform round is exactly the paper’s sampling: \(k\) uniform neighbours with replacement, independently for every vertex; \(t\) i.i.d. uniform rounds are averaged with Dynamics.expList. If \(G\) is connected and has at least two vertices, rounds exist.
COBRA from \(C_0=C\): \(C_{s+1}=\{ r_{s+1}(x,i) : x\in C_s,\ i{\lt}k\} \). BIPS with persistent source \(v\) from \(A_0\): \(A_{s+1}=\{ v\} \cup \{ u : \exists i,\ r_{s+1}(u,i)\in A_s\} \).
The search of Krivelevich–Sudakov (Section 2) with the sets \(S\) (done), \(U\) (stack) and \(T\) (unvisited), stopped before each query; after \(U=T=\emptyset \) the remaining pairs are queried.
Let \(\beta ,\gamma {\gt}0\) and \(R_0=\beta /\gamma \). A solution is a triple \((s,i,r)\) of real functions such that \(t\mapsto (s,i,r)(t)\) is an integral curve on \([0,\infty )\) (one-sided derivative at \(0\)) of the field \((s,i,r)\mapsto (-\beta si,\ \beta si-\gamma i,\ \gamma i)\), with \(s(0),i(0){\gt}0\), \(r(0)=0\) and \(s(0)+i(0)+r(0)=1\). Solutions are assumed, not constructed.
Let \(\beta ,\gamma \in \mathbb N\). A configuration assigns to each of \(N\) agents a compartment \(S\), \(I\) or \(R\); \(X=(S,I,R)/N\) are the scaled counts. One step draws \((u,v)\) uniformly in \([N]^2\) and one of \(\beta +\gamma \) equally likely clocks: on one of the \(\beta \) infection clocks an infected \(u\) infects a susceptible \(v\), on one of the \(\gamma \) recovery clocks an infected \(u\) recovers. This is the continuous-time chain (\(S+I\to 2I\) at rate \(\beta SI/N\), \(I\to R\) at rate \(\gamma I\)) uniformized at rate \((\beta +\gamma )N\). The deviation probability is the probability that \(\| X_k-x(k/((\beta +\gamma )N))\| _\infty {\gt}\theta \) for some \(k\le n\).
Every edge \(e\) of a finite graph \(G\) carries a coin \(\omega (e)\in \{ \mathrm{true},\mathrm{false}\} \); the percolated graph \(G_\omega \) keeps the edges whose coin is true. In one round, a susceptible node becomes infected if it has an infected neighbour across an open edge, and every infected node recovers. Initially the set \(I_0\) is infected and nobody is recovered. We write \(d(v)\in \mathbb N\cup \{ \infty \} \) for the distance from \(I_0\) to \(v\) in \(G_\omega \).
Upper exponential growth (Definition 9): for \(1\le |S|=k{\lt}fn\), every uninformed node is informed with probability at least \(\gamma \frac kn(1-a\frac kn-\frac b{\ln n})\) and covariances are at most \(ck/n^2\). Upper exponential shrinking (Definition 11): when \(u=n-|S|\le gn\), every uninformed node stays uninformed with probability at most \(e^{-\rho }+au/n\) and covariances are at most \(c/u\).
A rumor-spreading process on \(n\) nodes is a Markov kernel on the set \(S\) of informed nodes under which informed nodes stay informed. For a round started from \(S\), \(\mathrm{informProb}(S,x)\) is the probability that \(x\) is informed after the round and \(\mathrm{cov}(S,x,y)\) the covariance of the events that \(x\) and \(y\) are. The tail of the spreading time is \(\mathrm{notYet}(m,t,S)=\Pr [\text{fewer than }m\text{ nodes informed after }t\text{ rounds from }S]=\Pr [T(|S|,m){\gt}t]\); expected times are bounded through all partial sums of \(\sum _t\Pr [T{\gt}t]\). Homogeneity (Definition 6) is defined but not assumed.
The deterministic steps of the proofs of Theorems 1 and 2 of the paper: \(|S\cup U|{\lt}n/3\) at time \(N_0\), \(|U|\ge \ell n+1\), and the current epoch started before \(t_1\).
If increments \(D(X_j,\rho _j)\) along i.i.d. uniform rounds have zero conditional mean and \(|D|\le c\), their partial sums \(M_k\) satisfy \(\mathbb P(\exists k\le n,\ M_k\ge \lambda )\le e^{-\lambda ^2/(2nc^2)}\).
At least \(t\) successes among \(t(d-1)+1\) independent Bernoulli\((p)\) trials occur with probability at most \(\exp (\varepsilon - \varepsilon ^2 t/2)\).
If an adaptive strategy queries the coins one at a time, the next coordinate being a function of the answers so far, and never queries a coordinate twice among its first \(m\) queries, then its first \(m\) answers are i.i.d. Bernoulli\((p)\).
Every pair is queried at most once; all pairs between \(S\) and \(T\) have been queried negatively; \(U\) spans a path; \(|U|\le 1+\sum X_i\) and, while \(T\ne \emptyset \), \(|S\cup U|\ge \sum X_i\); the vertices of one epoch are connected; when an epoch starts, the explored set \(D\) has all its pairs with \(V\setminus D\) queried.
- Epidemics.DFS.State.Inv
- Epidemics.DFS.State.move_settle
- Epidemics.DFS.fresh_nextQuery
- Epidemics.DFS.card_queried_ofAnswers
- Epidemics.DFS.mem_found_iff_of_queryAnswers
- Epidemics.DFS.queried_of_mem_done_of_mem_unvisited
- Epidemics.DFS.stack_chain_ofAnswers
- Epidemics.DFS.length_stack_le
- Epidemics.DFS.count_true_le_card
- Epidemics.DFS.card_union_append_le
- Epidemics.DFS.reachable_of_mem_comp
- Epidemics.DFS.count_drop_le_card_comp
- Epidemics.DFS.exists_of_epochs_lt
\(d(v)=0\) iff \(v\in I_0\); if \(u\) and \(v\) are adjacent in \(G_\omega \) then \(d(v)\le d(u)+1\); if \(d(v)=t+1\) then \(v\) has a neighbour \(u\) in \(G_\omega \) with \(d(u)=t\); \(d(v){\lt}\infty \) iff \(v\) is connected to \(I_0\) in \(G_\omega \), and then \(d(v){\lt}|V|\).
Among \(N_0\) i.i.d. Bernoulli\((p)\) trials, the number of successes deviates from \(N_0p\) by \(\delta N_0p\) with probability at most \(2e^{-\delta ^2N_0p/3}\) (Chernoff bounds of FND-3 instead of Chebyshev, as in the paper’s Discussion, item 1); the same holds at every time of a window.
\(\mathbb E[X_{k+1}-X_k\mid X_k=x]=F(x)/((\beta +\gamma )N)\) with \(F\) the Kermack–McKendrick field, and \(\| X_{k+1}-X_k\| _\infty \le 1/N\).
For every functional \(F\) of \(T\) i.i.d. uniform rounds, \(\mathbb E[F(r_T,\dots ,r_1)]=\mathbb E[F(r_1,\dots ,r_T)]\).
If every uninformed node is informed with probability at least \(p\) in every round started with \(\ell \le |S|{\lt}m\) informed nodes, then \(\Pr [T(\ell ,m){\gt}r]\le \frac{n-\ell }{n-m}(1-p)^r\) and \(E[T(\ell ,m)]\le \frac{n-\ell }{n-m}\cdot \frac1p\).
If every round started with \(1\le |S|{\lt}fn\) has \(p_k\le p\) and covariances at most \(c/n\), then (one round) for every \(f'\in \, ]f+p(1-f),1[\), a round from \(|S|{\lt}fn\) ends with at least \(f'n\) informed nodes with probability at most \(C/n\); and (path form) there is \(f'\in \, ]f,1[\) such that the probability of jumping over \([fn,f'n[\) within \(t\) rounds is at most \(\frac Cn\) times the expected number of these rounds started below \(fn\), i.e. \(O(E[T(|S|,fn)]/n)\).
The component of \(s\) in \(G_p\) has more than \(t\) vertices with probability at most that of at least \(t\) successes in \(t(d-1)+1\) independent Bernoulli\((p)\) trials.
For every finite graph, every \(k\), every vertex \(v\), set \(C\) and time \(t\): \(\hat{\mathbb P}(\mathrm{Hit}_C(v){\gt}t\mid C_0=C)=\mathbb P(C\cap A_t=\emptyset \mid A_0=\{ v\} )\). In particular (equation (2)), \(\hat{\mathbb P}(\mathrm{Hit}_u(v){\gt}t)=\mathbb P(u\notin A_t\mid A_0=\{ v\} )\). The paper assumes \(G\) connected and regular and \(k\ge 1\); none of this is needed.
For every small enough \(\varepsilon {\gt}0\) there is \(C\) such that \(G(n,(1+\varepsilon )/n)\) has a component with at least \(\varepsilon n/2\) vertices with probability at least \(1-C/n\); for every \(\varepsilon {\gt}0\) there are \(c{\gt}0\) and \(C\) such that it has a component with at least \(cn\) vertices with probability at least \(1-C/n\).
On \([0,\infty )\): \(s+i+r=1\); \(s,i{\gt}0\) and \(r\ge 0\); \(s\) is strictly decreasing and \(r\) strictly increasing; and \(s(t)=s(0)e^{-R_0r(t)}\).
- Epidemics.KermackMcKendrick.IsSolution.sum_eq_one
- Epidemics.KermackMcKendrick.IsSolution.s_pos
- Epidemics.KermackMcKendrick.IsSolution.i_pos
- Epidemics.KermackMcKendrick.IsSolution.r_nonneg
- Epidemics.KermackMcKendrick.IsSolution.strictAntiOn_s
- Epidemics.KermackMcKendrick.IsSolution.strictMonoOn_r
- Epidemics.KermackMcKendrick.IsSolution.s_eq_mul_exp
\(i(t)\to 0\), \(s(t)\to s_\infty \) and \(r(t)\to 1-s_\infty \); moreover \(s_\infty =s(0)e^{-R_0(1-s_\infty )}\), \(0{\lt}s_\infty {\lt}1/R_0\), and \(s_\infty \) is the unique root of this equation in \((0,1/R_0]\) and in \((0,1]\).
- Epidemics.KermackMcKendrick.IsSolution.tendsto_i
- Epidemics.KermackMcKendrick.IsSolution.exists_tendsto_s
- Epidemics.KermackMcKendrick.IsSolution.tendsto_r
- Epidemics.KermackMcKendrick.IsSolution.final_size
- Epidemics.KermackMcKendrick.IsSolution.limit_pos
- Epidemics.KermackMcKendrick.IsSolution.R₀_mul_limit_lt_one
- Epidemics.KermackMcKendrick.IsSolution.final_size_unique
- Epidemics.KermackMcKendrick.IsSolution.final_size_unique_of_le_one
If \(R_0s(0)\le 1\), then \(i\) is strictly decreasing on \([0,\infty )\). The function \(i\) is strictly increasing on some \([0,\varepsilon ]\), \(\varepsilon {\gt}0\), iff \(R_0s(0){\gt}1\).
Let \(\beta ,\gamma ,T{\gt}0\). There are \(C,c{\gt}0\) and \(L\) such that for every \(N\), every initial configuration, every solution \(x\) of the Kermack–McKendrick system started in the simplex and every \(\varepsilon {\gt}0\), with probability at least \(1-Ce^{-c\varepsilon ^2N}\), \(\| X_k-x(k/((\beta +\gamma )N))\| _\infty \le L\| X_0-x(0)\| _\infty +\varepsilon \) for all \(k\le T(\beta +\gamma )N\). Hence, if \(X_0\to x(0)\), the scaled chain converges to \(x\) in probability, uniformly on \([0,T]\).
For every coin assignment and every \(t\), the nodes infected in round \(t\) are those with \(d(v)=t\), and the nodes recovered by round \(t\) are those with \(d(v){\lt}t\).
For every small enough \(\varepsilon {\gt}0\) there is \(C\) such that \(G(n,(1+\varepsilon )/n)\) contains a path with at least \(\varepsilon ^2n/5\) edges with probability at least \(1-C/n\).
With independent Bernoulli\((p)\) coins, each edge is open with probability \(p\), and the probability that \(v\) is eventually infected equals the probability that \(v\) is connected to \(I_0\) by open edges.
Under the upper exponential growth conditions, with \(\gamma \) between two positive constants and \(af{\lt}1\), from any nonempty \(S\): \(\Pr [T(|S|,fn){\gt}\lceil \log _{1+\gamma }n\rceil +r]\le Ae^{-\alpha r}\) and \(E[T(|S|,fn)]\le \log _{1+\gamma }n+B\), with constants depending only on the parameters.
Under the upper exponential shrinking conditions, with \(\rho \) between two positive constants and \(e^{-\rho _{lo}}+ag{\lt}1\), from any \(S\) with \(n-|S|\le gn\): \(\Pr [T(|S|,n){\gt}\lceil \ln n/\rho \rceil +r]\le Ae^{-\alpha r}\) and \(E[T(|S|,n)]\le \ln n/\rho +B\).
Under the growth conditions on \([1,fn[\), the shrinking conditions below \(gn\) uninformed nodes and a probability at least \(p{\gt}0\) of being informed in between, from any nonempty \(S\): \(\Pr [T{\gt}\lceil \log _{1+\gamma }n\rceil +\lceil \ln n/\rho \rceil +r]\le Ae^{-\alpha r}\) and \(E[T]\le \log _{1+\gamma }n+\ln n/\rho +B\).
The component of any vertex has more than \(t\) vertices with probability at most \(\exp (\varepsilon - \varepsilon ^2 t/2)\), and with probability at least \(1 - 1/n\) every component of \(G_p\) has at most \((10/\varepsilon ^2)\log n\) vertices.