Finite-probability helpers for EPI-2

Monotonicity of prob is the core's Distribution.prob_mono; congruence, the complement rule prob_not and the union bound prob_exists_le_sum are those of Epidemics.GiantCoins (EPI-3); Markov's inequality on an exponential moment and the expectation of a coin are the core's Distribution.prob_le_expect_exp and Distribution.bernoulli_expect (FND-3). This file adds prob_eq_one, prob_eq_zero and two ways of conditioning an independent product on one coordinate (an arbitrary coordinate, through Function.update, and the first coordinate of Fin (m + 1), through Fin.cons). They are stated for any Distribution; their move to dynamics/ is tracked in issues #42 and #46.

theorem Epidemics.prob_eq_one {α : Type u_1} [Fintype α] (q : Dynamics.Distribution α) {s : α → Prop} (h : ∀ (a : α), s a) : q.prob s = 1

theorem Epidemics.prob_eq_zero {α : Type u_1} [Fintype α] (q : Dynamics.Distribution α) {s : α → Prop} (h : ∀ (a : α), ¬s a) : q.prob s = 0

theorem Epidemics.independent_expect_update {ι : Type u_2} {β : Type u_3} [Fintype ι] [Fintype β] [DecidableEq ι] (q : ι → Dynamics.Distribution β) (i : ι) (f : (ι → β) → ℝ) : (Dynamics.Distribution.independent q).expect f = ∑ b : β, (q i).weight b * (Dynamics.Distribution.independent q).expect fun (x : ι → β) => f (Function.update x i b)

Conditioning an independent product on one coordinate: the expectation is the average, over the value b of coordinate i, of the expectation with that coordinate set to b.

theorem Epidemics.independent_expect_fin_succ {β : Type u_3} [Fintype β] {m : ℕ} (q : Dynamics.Distribution β) (f : (Fin (m + 1) → β) → ℝ) : (Dynamics.Distribution.independent fun (x : Fin (m + 1)) => q).expect f = ∑ b : β, q.weight b * (Dynamics.Distribution.independent fun (x : Fin m) => q).expect fun (r : Fin m → β) => f (Fin.cons b r)

Conditioning on the first coordinate: an i.i.d. product over Fin (m + 1) is the average, over the first coordinate b, of the product over Fin m with b prepended.

theorem Epidemics.coins_prob_split {α : Type u_1} [Fintype α] [DecidableEq α] (p : ℝ) (h0 : 0 ≤ p) (h1 : p ≤ 1) (e : α) (s : (α → Bool) → Prop) : (Dynamics.Distribution.independent fun (x : α) => bernoulli p h0 h1).prob s = (p * (Dynamics.Distribution.independent fun (x : α) => bernoulli p h0 h1).prob fun (ω : α → Bool) => s (Function.update ω e true)) + (1 - p) * (Dynamics.Distribution.independent fun (x : α) => bernoulli p h0 h1).prob fun (ω : α → Bool) => s (Function.update ω e false)

Conditioning the percolation coins on the coin of one pair.