Kurtz's law of large numbers for SIR in discrete time: the chain (CRN-2)

The stochastic SIR epidemic of the roadmap (row CRN-2) is the continuous-time Markov chain on N agents with reactions S + I → 2I at rate β S I / N and I → R at rate γ I. Its total jump rate is at most Λ = (β + γ) N; uniformizing at rate Λ, each ring of a rate-Λ Poisson clock is an infection with probability β S I / (N Λ), a recovery with probability γ I / Λ, and otherwise nothing. We formalize this discrete-time chain (the jump chain of the uniformization), with one step per unit 1 / ((β + γ) N) of time:

• a Round draws an ordered pair (u, v) of agents uniformly with replacement and one of β + γ equally likely clocks: β infection clocks (Sum.inl) and γ recovery clocks (Sum.inr), so β, γ are natural numbers (rates with a rational ratio, up to a time change);
• step: on an infection clock, if u is infected and v susceptible then v becomes infected; on a recovery clock, if u is infected then u recovers; otherwise nothing changes.

Then the expected increment of the scaled counts scaled x = (S, I, R) / N is exactly sirField β γ (scaled x) / ((β + γ) N), the Kermack–McKendrick field of EPI-7 (Epidemics.KermackMcKendrickDefs) times the time step, and each step moves scaled x by at most 1 / N (Epidemics.KurtzDrift). The chain is the kernel Dynamics.Kernel.ofStep (step β γ); path probabilities are Dynamics.expList averages over i.i.d. uniform rounds, the state after the rounds l being l.foldl (step β γ) x₀. deviationProb is the probability that the chain leaves a tube around a curve during a finite horizon; the law of large numbers is in Epidemics.Kurtz.

inductive Epidemics.Kurtz.Compartment : Type

The three compartments of the SIR model.

• susceptible : Compartment
• infected : Compartment
• recovered : Compartment

@[implicit_reducible]

instance Epidemics.Kurtz.instDecidableEqCompartment : DecidableEq Compartment

Equations

• Epidemics.Kurtz.instDecidableEqCompartment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Epidemics.Kurtz.instFintypeCompartment : Fintype Compartment

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Epidemics.Kurtz.Config (N : ℕ) : Type

A configuration of N agents: the compartment of every agent.

Equations

• Epidemics.Kurtz.Config N = (Fin N → Epidemics.Kurtz.Compartment)

def Epidemics.Kurtz.count {N : ℕ} (c : Compartment) (x : Config N) : ℕ

The number of agents of the configuration x in the compartment c.

Equations

• Epidemics.Kurtz.count c x = {v : Fin N | x v = c}.card

noncomputable def Epidemics.Kurtz.scaled {N : ℕ} (x : Config N) : ℝ × ℝ × ℝ

The scaled counts (S / N, I / N, R / N) of a configuration, as a point of the state space ℝ × ℝ × ℝ of the Kermack–McKendrick field sirField.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Epidemics.Kurtz.Round (N β γ : ℕ) : Type

The randomness of one step: an ordered pair (u, v) of agents, drawn with replacement, and one of β + γ equally likely clocks, β infection clocks (Sum.inl) and γ recovery clocks (Sum.inr).

Equations

• Epidemics.Kurtz.Round N β γ = (Fin N × Fin N × (Fin β ⊕ Fin γ))

def Epidemics.Kurtz.step (β γ : ℕ) {N : ℕ} (x : Config N) (ρ : Round N β γ) : Config N

One step of the uniformized SIR chain with infection weight β and recovery weight γ: on an infection clock, an infected u infects a susceptible v; on a recovery clock, an infected u recovers; otherwise nothing changes. A uniform round thus infects with probability β / (β + γ) · (I / N) · (S / N) and recovers with probability γ / (β + γ) · I / N, the jump probabilities of the continuous-time chain (S + I → 2I at rate β S I / N, I → R at rate γ I) uniformized at rate (β + γ) N.

Equations

• One or more equations did not get rendered due to their size.
• Epidemics.Kurtz.step β γ x (u, fst, Sum.inr val) = if x u = Epidemics.Kurtz.Compartment.infected then Function.update x u Epidemics.Kurtz.Compartment.recovered else x

noncomputable def Epidemics.Kurtz.chain (β γ N : ℕ) [Nonempty (Round N β γ)] : Dynamics.Kernel (Config N)

The uniformized SIR chain as a finite Markov kernel on configurations: one uniformly random Round of step.

Equations

• Epidemics.Kurtz.chain β γ N = Dynamics.Kernel.ofStep (Epidemics.Kurtz.step β γ)

noncomputable def Epidemics.Kurtz.deviationProb (β γ : ℕ) {N : ℕ} (x₀ : Config N) (x : ℝ → ℝ × ℝ × ℝ) (δ : ℝ) (n : ℕ) : ℝ

The probability that the SIR chain started at x₀ is, at some step k ≤ n, at distance more than δ from the curve x at the matching time k / ((β + γ) N). The n rounds are i.i.d. uniform (Dynamics.expList), the state after k of them is (l.take k).foldl (step β γ) x₀, and dist on ℝ × ℝ × ℝ is the sup distance (Prod.dist_eq).

Equations

• One or more equations did not get rendered due to their size.