One-round lemmas for COBRA and BIPS (EPI-4)

Membership in one COBRA or BIPS round, the recursions of cobraRun and bipsRun, and the unfolding of the COBRA hitting event "v ∈ C_s for some s ≤ t" over the first round.

theorem Epidemics.mem_cobraStep {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {k : ℕ} {D : Finset V} {r : Choices G k} {y : V} : y ∈ cobraStep D r ↔ ∃ x ∈ D, ∃ (i : Fin k), ↑(r x i) = y

A vertex is reached by a COBRA round from D iff some vertex of D sampled it.

theorem Epidemics.mem_bipsStep {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {k : ℕ} {v : V} {A : Finset V} {r : Choices G k} {u : V} : u ∈ bipsStep v A r ↔ u = v ∨ ∃ (i : Fin k), ↑(r u i) ∈ A

A vertex is infected after a BIPS round iff it is the source or sampled an infected vertex.

@[simp]

theorem Epidemics.cobraRun_nil {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (C : Finset V) : cobraRun C [] = C

@[simp]

theorem Epidemics.cobraRun_cons {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (C : Finset V) (r : Choices G k) (l : List (Choices G k)) : cobraRun C (r :: l) = cobraRun (cobraStep C r) l

COBRA after the rounds r :: l is COBRA from cobraStep C r after the rounds l.

theorem Epidemics.bipsRun_append_singleton {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (v : V) (A₀ : Finset V) (l : List (Choices G k)) (r : Choices G k) : bipsRun v A₀ (l ++ [r]) = bipsStep v (bipsRun v A₀ l) r

BIPS after the rounds l ++ [r] is one more round r after the rounds l.

theorem Epidemics.hits_cons {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} {k : ℕ} (v : V) (C : Finset V) (r : Choices G k) (l : List (Choices G k)) : (∃ s ≤ (r :: l).length, v ∈ cobraRun C (List.take s (r :: l))) ↔ v ∈ C ∨ ∃ s ≤ l.length, v ∈ cobraRun (cobraStep C r) (List.take s l)

The COBRA hitting event over the rounds r :: l: either v is in the start set, or COBRA restarted from the first round's image hits v within the rounds l.