Finite concentration inequalities

The upper-bound proof only uses uniform probability on finite sample spaces. This file proves the finite Markov/Chernoff mechanism in that setting, with real-valued expectations so that exponential moment bounds can be stated directly.

noncomputable def PebblingLean.FiniteProbability.uniformProbabilityReal {Ω : Type u_1} [Fintype Ω] (P : Ω → Prop) [DecidablePred P] : ℝ

Uniform probability of an event on a finite sample space, as a real number.

Equations

• PebblingLean.FiniteProbability.uniformProbabilityReal P = ↑(Finset.filter P Finset.univ).card / ↑(Fintype.card Ω)

noncomputable def PebblingLean.FiniteProbability.uniformExpectationReal {Ω : Type u_1} [Fintype Ω] (X : Ω → ℝ) : ℝ

Uniform expectation of a real-valued random variable on a finite sample space.

Equations

• PebblingLean.FiniteProbability.uniformExpectationReal X = (∑ ω : Ω, X ω) / ↑(Fintype.card Ω)

theorem PebblingLean.FiniteProbability.uniformProbabilityReal_eq_coe_uniformProbability {Ω : Type u_1} [Fintype Ω] (P : Ω → Prop) [DecidablePred P] : uniformProbabilityReal P = ↑(uniformProbability P)

theorem PebblingLean.FiniteProbability.uniformProbability_le_of_uniformProbabilityReal_le {Ω : Type u_1} [Fintype Ω] {P : Ω → Prop} [DecidablePred P] {eps : ℚ} (h : uniformProbabilityReal P ≤ ↑eps) : uniformProbability P ≤ eps

theorem PebblingLean.FiniteProbability.uniformProbabilityReal_le_expect_div_of_event_le {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] {P : Ω → Prop} [DecidablePred P] (X : Ω → ℝ) {a : ℝ} (ha : 0 < a) (hnonneg : ∀ (ω : Ω), 0 ≤ X ω) (hP : ∀ (ω : Ω), P ω → a ≤ X ω) : uniformProbabilityReal P ≤ uniformExpectationReal X / a

Finite Markov inequality for uniform probability. The event is allowed to be any predicate implied by a ≤ X.

theorem PebblingLean.FiniteProbability.uniformProbabilityReal_lt_le_exponentialMoment {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] (X : Ω → ℝ) {T lam : ℝ} (hlam : 0 < lam) : (uniformProbabilityReal fun (ω : Ω) => X ω < T) ≤ uniformExpectationReal fun (ω : Ω) => Real.exp (lam * (T - X ω))

Chernoff's exponential-moment step for a lower tail, proved here as Markov's inequality applied to exp(λ(T - X)).

theorem PebblingLean.FiniteProbability.uniformProbabilityReal_lt_le_of_exponentialMoment_le {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] (X : Ω → ℝ) {T lam B : ℝ} (hlam : 0 < lam) (hmoment : (uniformExpectationReal fun (ω : Ω) => Real.exp (lam * (T - X ω))) ≤ B) : (uniformProbabilityReal fun (ω : Ω) => X ω < T) ≤ B

theorem PebblingLean.FiniteProbability.uniformProbabilityReal_lt_le_exp_neg_of_exponentialMoment_le {Ω : Type u_1} [Fintype Ω] [Nonempty Ω] (X : Ω → ℝ) {T lam exponent : ℝ} (hlam : 0 < lam) (hmoment : (uniformExpectationReal fun (ω : Ω) => Real.exp (lam * (T - X ω))) ≤ Real.exp (-exponent)) : (uniformProbabilityReal fun (ω : Ω) => X ω < T) ≤ Real.exp (-exponent)

theorem PebblingLean.FiniteProbability.exp_neg_mul_le_chord {lam B z : ℝ} (hB : 0 < B) (hz0 : 0 ≤ z) (hzB : z ≤ B) : Real.exp (-(lam * z)) ≤ 1 - (1 - Real.exp (-(lam * B))) * (z / B)

Convexity of the exponential gives the chord bound used for bounded nonnegative summands: on 0 ≤ z ≤ B, exp(-λ z) is below the chord joining 0 and B.

theorem PebblingLean.FiniteProbability.one_sub_exp_neg_ge_sub_sq {x : ℝ} (hx : 0 ≤ x) : x - x ^ 2 ≤ 1 - Real.exp (-x)

A scalar lower bound for 1 - exp(-x) that follows from 1 + x ≤ exp x. This is the elementary replacement for the usual Taylor estimate in the bounded-nonnegative Chernoff optimization.

theorem PebblingLean.FiniteProbability.one_sub_le_exp_neg (u : ℝ) : 1 - u ≤ Real.exp (-u)

theorem PebblingLean.FiniteProbability.pow_le_exp_neg_mul_of_le_one_sub {a u : ℝ} (N : ℕ) (ha_nonneg : 0 ≤ a) (ha_le : a ≤ 1 - u) : a ^ N ≤ Real.exp (-(↑N * u))

If a nonnegative one-step moment is at most 1-u, then its N-fold product is at most exp(-N u). This is the product step in the bounded-nonnegative Chernoff argument.

theorem PebblingLean.FiniteProbability.exp_chord_quadratic_optimized {T gap B mu lam : ℝ} (hB : 0 < B) (hmu : 0 < mu) (hgap : 0 ≤ gap) (hmean : T + gap ≤ mu) (hlam : lam = gap / (2 * B * mu)) : Real.exp (lam * T - (lam - lam ^ 2 * B) * mu) ≤ Real.exp (-(gap ^ 2 / (4 * B * mu)))

Algebraic optimization for the chord-based bounded-nonnegative Chernoff bound. If mu exceeds the threshold T by gap, then the choice λ = gap/(2 B mu) gives the usual quadratic exponent.

theorem PebblingLean.FiniteProbability.exp_neg_le_inv_two_pow_succ_of_log_le (n : ℕ) {exponent : ℝ} (hlog : ↑(n + 1) * Real.log 2 ≤ exponent) : Real.exp (-exponent) ≤ ↑(1 / 2 ^ (n + 1))

A convenient way to discharge the hypercube union bound: an exponent at least (n+1) log 2 makes the fixed-target failure probability at most 2^-(n+1).