Elementary tail bounds

Probability facts that several model packages used to prove locally, stated once for the shared finite layer (monotonicity of probability in the event is Distribution.prob_mono).

• Distribution.expect_lt_one, avg_lt_one: an observable bounded by 1 that is strictly below 1 at a point of positive weight has expectation strictly below 1.
• avg_markov: Markov's inequality P(X ≥ c) ≤ 𝔼X / c for uniform averages, and avg_markov_one: its form P(X ≥ 1) ≤ 𝔼X for a sum of independent nonnegative coordinates.
• Kernel.one_sub_avg_le_prob_ofStep: one uniformly random round lands in an event with probability at least 1 - 𝔼[bad], when bad ≥ 0 charges every miss at least 1.
• Kernel.iterate_monotone: a subharmonic observable (f ≤ K f) has nondecreasing finite-time expectations, and Kernel.event_monotone: the occupation probability of an absorbing event is nondecreasing in time.
• exp_neg_two_log, one_le_of_log_pos: the scalar conversions used to state high-probability bounds in regimes C ≤ log n.

As everywhere in this library, the source has no paper numbering; each docstring names the package lemmas that the statement replaces.

Distributions

theorem Dynamics.Distribution.expect_lt_one {α : Type u_1} [Fintype α] (p : Distribution α) (f : α → ℝ) (hf : ∀ (a : α), f a ≤ 1) (b : α) (hb : 0 < p.weight b) (hfb : f b < 1) : p.expect f < 1

An observable bounded by 1 that is strictly below 1 at a point of positive weight has expectation strictly below 1 (the statement of Moran.expect_lt_one and Voter.expect_lt_one).

Uniform averages: strict bound and Markov's inequality

theorem Dynamics.avg_lt_one {α : Type u_1} [Fintype α] [Nonempty α] {f : α → ℝ} (hf : ∀ (a : α), f a ≤ 1) {b : α} (hb : f b < 1) : avg f < 1

The uniform case of Distribution.expect_lt_one: on a nonempty type, an observable bounded by 1 and strictly below 1 somewhere has average strictly below 1. (The statement of Undecided.avg_lt_one.)

theorem Dynamics.avg_markov {α : Type u_1} [Fintype α] {X : α → ℝ} (hX : ∀ (a : α), 0 ≤ X a) {c : ℝ} (hc : 0 < c) : (avg fun (a : α) => if c ≤ X a then 1 else 0) ≤ avg X / c

Markov's inequality for uniform averages: if X ≥ 0 and c > 0, then P(X ≥ c) ≤ 𝔼X / c.

theorem Dynamics.avg_markov_one {n : ℕ} {γ : Type u_2} [Fintype γ] (Y : Fin n → γ → ℝ) (hY : ∀ (i : Fin n) (x : γ), 0 ≤ Y i x) : (avg fun (ω : Fin n → γ) => if 1 ≤ ∑ i : Fin n, Y i (ω i) then 1 else 0) ≤ ∑ i : Fin n, avg (Y i)

Markov's inequality for a sum of independent nonnegative coordinates: P(X ≥ 1) ≤ 𝔼X for X = ∑ᵢ Yᵢ(ωᵢ), ω : Fin n → γ uniform. Replaces Plurality.markov_one (plurality blueprint lem:tails) and the Markov steps proved inline in Median.falses_tail_markov and ThreeMajority.saturation_stage2c.

One random round, and absorbing events

theorem Dynamics.Kernel.one_sub_avg_le_prob_ofStep {S : Type u_2} {R : Type u_3} [Fintype S] [Fintype R] [Nonempty R] (step : S → R → S) (P : S → Prop) (s : S) (bad : R → ℝ) (h0 : ∀ (r : R), 0 ≤ bad r) (h1 : ∀ (r : R), ¬P (step s r) → 1 ≤ bad r) : 1 - avg bad ≤ (ofStep step s).prob P

One round lands in an event with probability at least 1 - 𝔼[bad], whenever the nonnegative charge bad is at least 1 on every round that misses the event (Markov's inequality for the complement). Replaces Median.prob_step_ge and Plurality.le_prob_step.

theorem Dynamics.Kernel.iterate_monotone {α : Type u_1} [Fintype α] (K : Kernel α) (f : α → ℝ) (h : ∀ (a : α), f a ≤ K.apply f a) (a : α) : Monotone fun (n : ℕ) => K.iterate n f a

An observable with f ≤ K f (subharmonic) has nondecreasing finite-time expectations: the counterpart of iterate_antitone. It is the induction behind Voter.colorProbability_mono and the former Median.event_absorb_mono.

theorem Dynamics.Kernel.event_monotone {α : Type u_1} [Fintype α] (K : Kernel α) {P : α → Prop} (habs : ∀ (a : α), P a → (K a).prob P = 1) (a : α) : Monotone fun (n : ℕ) => K.event P n a

The occupation probability of an absorbing event is nondecreasing in time: if every state of P stays in P with probability one, then n ↦ P(Xₙ ∈ P) is monotone. Replaces Median.event_absorb_mono.

Scalar facts for high-probability statements

theorem Dynamics.exp_neg_two_log {n : ℕ} (hn : 1 ≤ n) : Real.exp (-(2 * Real.log ↑n)) = 1 / ↑n ^ 2

exp (-2 log n) = 1/n², the conversion of a tail bound exp (-c) with c ≥ 2 log n into a failure probability 1/n². Replaces Plurality.exp_neg_two_log and Median.exp_neg_two_log.

theorem Dynamics.one_le_of_log_pos {n : ℕ} (h : 0 < Real.log ↑n) : 1 ≤ n

A hypothesis 0 < log n, as implied by the regimes C ≤ log n with C > 0, forces 1 ≤ n. Replaces Plurality.one_le_of_log_pos and Median.one_le_of_log_pos.