Kurtz's law of large numbers for SIR: counting one step (CRN-2, helpers)

How one step of the uniformized SIR chain changes the counts count c x, and the total change summed over all Rounds. These are the combinatorial inputs of the drift identity (Epidemics.KurtzDrift). Indicators are written if c' = c then 1 else 0.

theorem Epidemics.Kurtz.count_eq_sum {N : ℕ} (c : Compartment) (x : Config N) : ↑(count c x) = ∑ v : Fin N, if x v = c then 1 else 0

A count is a sum of indicators.

theorem Epidemics.Kurtz.count_update {N : ℕ} (c c' : Compartment) (x : Config N) (v : Fin N) : ↑(count c (Function.update x v c')) = (↑(count c x) - if x v = c then 1 else 0) + if c' = c then 1 else 0

Moving the agent v to the compartment c' removes it from the count of its old compartment and adds it to the count of c'.

theorem Epidemics.Kurtz.count_step_inl {N : ℕ} (β γ : ℕ) (x : Config N) (u v : Fin N) (a : Fin β) (c : Compartment) : ↑(count c (step β γ x (u, v, Sum.inl a))) = ↑(count c x) + if x u = Compartment.infected ∧ x v = Compartment.susceptible then (if Compartment.infected = c then 1 else 0) - if Compartment.susceptible = c then 1 else 0 else 0

The counts after an infection round (u, v, inl a): if u is infected and v susceptible, one agent moves from susceptible to infected.

theorem Epidemics.Kurtz.count_step_inr {N : ℕ} (β γ : ℕ) (x : Config N) (u v : Fin N) (a : Fin γ) (c : Compartment) : ↑(count c (step β γ x (u, v, Sum.inr a))) = ↑(count c x) + if x u = Compartment.infected then (if Compartment.recovered = c then 1 else 0) - if Compartment.infected = c then 1 else 0 else 0

The counts after a recovery round (u, v, inr a): if u is infected, one agent moves from infected to recovered.

theorem Epidemics.Kurtz.sum_count_step {N : ℕ} (β γ : ℕ) (x : Config N) (c : Compartment) : ∑ ρ : Round N β γ, (↑(count c (step β γ x ρ)) - ↑(count c x)) = ↑β * ↑(count Compartment.infected x) * ↑(count Compartment.susceptible x) * ((if Compartment.infected = c then 1 else 0) - if Compartment.susceptible = c then 1 else 0) + ↑γ * ↑N * ↑(count Compartment.infected x) * ((if Compartment.recovered = c then 1 else 0) - if Compartment.infected = c then 1 else 0)

The total change of the count of c over all N² (β + γ) rounds: β I S infection rounds move an agent from S to I, γ N I recovery rounds move one from I to R.

theorem Epidemics.Kurtz.abs_count_step_sub_le {N : ℕ} (β γ : ℕ) (x : Config N) (ρ : Round N β γ) (c : Compartment) : |↑(count c (step β γ x ρ)) - ↑(count c x)| ≤ 1

One step changes every count by at most one.

theorem Epidemics.Kurtz.card_round {N : ℕ} (β γ : ℕ) : ↑(Fintype.card (Round N β γ)) = ↑N * (↑N * (↑β + ↑γ))

The number of rounds.