Documentation

Complexity.Probability.IID

Independent draws from a distribution #

Cslib.Probability.PMF.iid μ k draws k independent samples from μ, one coordinate at a time. A tuple has the product of the masses of its coordinates (iid_apply), as for the product Cslib.Probability.PMF.pi, but unlike pi it needs no finiteness of the sample space, so it applies to distributions on infinite types such as the public-coin protocols of communication complexity. Applying a function to each sample gives independent samples of the image (iid_map), and on finite types the draws form the product distribution (iid_eq_pi).

The majority tail bound (iid_card_ge_le): among 2 r independent bits, each true with probability q ≤ ε ≤ 1 / 2, at least r are true with probability at most (4 ε (1 - ε)) ^ r. Each outcome with t ≥ r true bits has probability q ^ t (1 - q) ^ (2 r - t) ≤ (q (1 - q)) ^ r, and there are at most 4 ^ r outcomes. The counting form Cslib.card_filter_card_filter_le_le (majority votes over a uniform sample space) and the Chernoff bounds Cslib.Probability.PMF.pi_sum_ge_le_exp (for finite products) give related tail bounds.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Probability.PMF.iid {α : Type u_1} (μ : PMF α) (k : ℕ) :
PMF (Fin k → α)

k independent draws from μ, as a tuple: draw the first coordinate, then the others.

Instances For
    source
    @[simp]
    theorem Cslib.Probability.PMF.iid_apply {α : Type u_1} (μ : PMF α) {k : ℕ} (v : Fin k → α) :
    (iid μ k) v = ∏ i : Fin k, μ (v i)

    A tuple of independent draws has the product of the masses of its coordinates.

    source
    theorem Cslib.Probability.PMF.mem_support_iid_iff {α : Type u_1} (μ : PMF α) {k : ℕ} (v : Fin k → α) :
    v ∈ (iid μ k).support ↔ ∀ (i : Fin k), v i ∈ μ.support

    A tuple can be drawn exactly when each of its coordinates can.

    source
    theorem Cslib.Probability.PMF.iid_map {α : Type u_1} {β : Type u_2} (μ : PMF α) (g : α → β) (k : ℕ) :
    iid (PMF.map g μ) k = PMF.map (fun (v : Fin k → α) (i : Fin k) => g (v i)) (iid μ k)

    Applying a function to each coordinate of independent draws gives independent draws of the image.

    source
    theorem Cslib.Probability.PMF.iid_eq_pi {α : Type u_1} [Finite α] (μ : PMF α) (k : ℕ) :
    iid μ k = pi fun (x : Fin k) => μ

    On a finite type, independent draws form the product distribution pi.

    source
    theorem Cslib.Probability.PMF.iid_card_ge_le {q : PMF Bool} {ε : ℝ} (hq : (q true).toReal ≤ ε) (hε : ε ≤ 1 / 2) (r : ℕ) :
    ((iid q (2 * r)).toOuterMeasure {v : Fin (2 * r) → Bool | r ≤ {i : Fin (2 * r) | v i = true}.card}).toReal ≤ (4 * ε * (1 - ε)) ^ r

    The majority tail bound: among 2 r independent bits that are each true with probability at most ε ≤ 1 / 2, at least r are true with probability at most (4 ε (1 - ε)) ^ r.