Distribution lemmas for the exponential-growth upper bound

Finite-distribution support, variance of a sum of indicators (Lemma 9), Chebyshev and Cantelli, and the partial geometric sum. Nothing here uses measure theory.

Distribution.prob elaborates its indicator with Classical.propDecidable, while a hand-written if on a decidable predicate (membership, subset) uses that decidable instance. The two functions are propositionally equal but not definitionally equal, so every bridge goes through prob_indicator_eq.

theorem Epidemics.Revisited.prob_indicator_eq {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) (p : α → Prop) (f : α → ℝ) (h0 : ∀ (a : α), ¬p a → f a = 0) (h1 : ∀ (a : α), p a → f a = 1) : D.prob p = D.expect f

prob agrees with the expectation of any function that is the indicator of p.

theorem Epidemics.Revisited.expect_sq_centered {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) (X : α → ℝ) : (D.expect fun (a : α) => (X a - D.expect X) ^ 2) = (D.expect fun (a : α) => X a ^ 2) - D.expect X ^ 2

theorem Epidemics.Revisited.expect_div {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) (W : α → ℝ) (d : ℝ) : (D.expect fun (a : α) => W a / d) = D.expect W / d

theorem Epidemics.Revisited.markov_sq {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) (Z : α → ℝ) {c : ℝ} (hc : 0 < c) : (D.prob fun (a : α) => c ≤ |Z a|) ≤ (D.expect fun (a : α) => Z a ^ 2) / c ^ 2

Markov on the square: P[|Z| ≥ c] ≤ E[Z²] / c².

theorem Epidemics.Revisited.chebyshev {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) (X : α → ℝ) {lam : ℝ} (hlam : 0 < lam) : (D.prob fun (a : α) => lam ≤ |X a - D.expect X|) ≤ (D.expect fun (a : α) => (X a - D.expect X) ^ 2) / lam ^ 2

Chebyshev: P[|X - EX| ≥ lam] ≤ Var(X) / lam².

theorem Epidemics.Revisited.cantelli_lower {α : Type u_1} [Fintype α] (D : Dynamics.Distribution α) (X : α → ℝ) {lam : ℝ} (hlam : 0 < lam) : (D.prob fun (a : α) => X a ≤ D.expect X - lam) ≤ (D.expect fun (a : α) => (X a - D.expect X) ^ 2) / ((D.expect fun (a : α) => (X a - D.expect X) ^ 2) + lam ^ 2)

One-sided Chebyshev (Cantelli), lower tail: P[X ≤ EX - lam] ≤ Var / (Var + lam²).

theorem Epidemics.Revisited.geom_partial_le {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (R : ℕ) : ∑ i ∈ Finset.range R, q ^ i ≤ (1 - q)⁻¹

theorem Epidemics.Revisited.weight_zero_of_not_subset {n : ℕ} (P : RumorProcess n) {S T : Finset (Fin n)} (hT : ¬S ⊆ T) : (P.K S).weight T = 0

States outside the monotone support have weight zero.

theorem Epidemics.Revisited.expect_eq_of_agree_on_superset {n : ℕ} (P : RumorProcess n) (S : Finset (Fin n)) {f g : Finset (Fin n) → ℝ} (h : ∀ (T : Finset (Fin n)), S ⊆ T → f T = g T) : (P.K S).expect f = (P.K S).expect g

theorem Epidemics.Revisited.expect_le_of_weight {n : ℕ} (P : RumorProcess n) (S : Finset (Fin n)) {f g : Finset (Fin n) → ℝ} (h : ∀ (T : Finset (Fin n)), S ⊆ T → f T ≤ g T) : (P.K S).expect f ≤ (P.K S).expect g

theorem Epidemics.Revisited.card_compl_cast {n : ℕ} (S : Finset (Fin n)) : ↑(Finset.univ \ S).card = ↑n - ↑S.card

theorem Epidemics.Revisited.card_eq_add_indicators {n : ℕ} {S T : Finset (Fin n)} (h : S ⊆ T) : ↑T.card = ↑S.card + ∑ x ∈ Finset.univ \ S, if x ∈ T then 1 else 0

theorem Epidemics.Revisited.indicator_mul_indicator {n : ℕ} (x y : Fin n) (T : Finset (Fin n)) : ((if x ∈ T then 1 else 0) * if y ∈ T then 1 else 0) = if x ∈ T ∧ y ∈ T then 1 else 0

theorem Epidemics.Revisited.expect_finset_sum {α : Type u_1} [Fintype α] {ι : Type u_2} (D : Dynamics.Distribution α) (s : Finset ι) (f : ι → α → ℝ) : (D.expect fun (a : α) => ∑ i ∈ s, f i a) = ∑ i ∈ s, D.expect fun (a : α) => f i a

theorem Epidemics.Revisited.indicator_sq {n : ℕ} (x : Fin n) (T : Finset (Fin n)) : (if x ∈ T then 1 else 0) ^ 2 = if x ∈ T then 1 else 0

theorem Epidemics.Revisited.variance_sum_indicator_le {n : ℕ} (D : Dynamics.Distribution (Finset (Fin n))) (comp : Finset (Fin n)) {c : ℝ} (hc : 0 ≤ c) (hcov : ∀ x ∈ comp, ∀ y ∈ comp, x ≠ y → ((D.expect fun (T : Finset (Fin n)) => if x ∈ T ∧ y ∈ T then 1 else 0) - (D.expect fun (T : Finset (Fin n)) => if x ∈ T then 1 else 0) * D.expect fun (T : Finset (Fin n)) => if y ∈ T then 1 else 0) ≤ c) : (D.expect fun (T : Finset (Fin n)) => ((∑ x ∈ comp, if x ∈ T then 1 else 0) - D.expect fun (U : Finset (Fin n)) => ∑ x ∈ comp, if x ∈ U then 1 else 0) ^ 2) ≤ (D.expect fun (T : Finset (Fin n)) => ∑ x ∈ comp, if x ∈ T then 1 else 0) + c * ↑comp.card ^ 2

Variance of ∑_{x ∈ comp} 1[x ∈ T], with pairwise covariances at most c.

theorem Epidemics.Revisited.variance_card_le_proof {n : ℕ} (P : RumorProcess n) (S : Finset (Fin n)) {c : ℝ} (hc : 0 ≤ c) (hcov : ∀ x ∉ S, ∀ y ∉ S, x ≠ y → P.cov S x y ≤ c) : ((P.K S).expect fun (S' : Finset (Fin n)) => (↑S'.card - (P.K S).expect fun (S'' : Finset (Fin n)) => ↑S''.card) ^ 2) ≤ ((P.K S).expect fun (S' : Finset (Fin n)) => ↑S'.card) - ↑S.card + c * (↑n - ↑S.card) ^ 2

Lemma 9, proved for variance_card_le.