Bernoulli coordinate sampling and transference

A Boolean mask selected : ι → Bool is a set of coordinates. Selecting each coordinate independently with probability p gives it the weight bernoulliWeight p selected, and bernoulliAverage p f is the expectation of f over the random mask, a finite sum. The coordinates of the random mask are independent (bernoulliAverage_prod), the union of independent masks of rates p and q has rate p + q - p q (bernoulliAverage_union), and increasing the rate decreases the expectation of an antitone function (bernoulliAverage_bias_antitone).

The union of h independent masks of rate p lies in a lower set A only if each of them does. So when h p ≤ q, the probability of A at rate q is at most its probability at rate p to the power h (bernoulliAverage_lowerSet_pow_le). This transference principle appears in Section 2 of [Kor26] (Lemma 3) and again in Section 4; Korten attributes it to Zhao, Lemma 4.3.7. Its form at small rates, with a real exponent, is BitString.bernoulliAverage_lowerSet_transfer.

Main definitions

• Cslib.BitString.bernoulliWeight: the probability of a mask.
• Cslib.BitString.bernoulliAverage: the expectation over a random mask.

Main results

• Cslib.BitString.bernoulliAverage_prod: the coordinates of a random mask are independent.
• Cslib.BitString.bernoulliAverage_reindex, Cslib.BitString.bernoulliAverage_sumElim, Cslib.BitString.bernoulliAverage_restrict: reindexing, splitting over a disjoint union, and restricting the coordinates of a random mask.
• Cslib.BitString.bernoulliAverage_coordinate, Cslib.BitString.bernoulliAverage_nonempty, Cslib.BitString.bernoulliAverage_hits, Cslib.BitString.bernoulliAverage_weight: the probability that a coordinate is selected, that some coordinate is, that some coordinate of a given set is, and the expected number of selected coordinates.
• Cslib.BitString.bernoulliAverage_bernoulliAverage_eq_sum: the law of a coordinatewise image of two independent masks.
• Cslib.BitString.bernoulliAverage_union: unions of independent masks.
• Cslib.BitString.bernoulliAverage_bias_antitone: antitone functions have smaller expectations at larger rates.
• Cslib.BitString.bernoulliAverage_lowerSet_union, Cslib.BitString.bernoulliAverage_lowerSet_pow_le: transference for lower sets.

References

• O. Korten, Top-Down Lower Bounds for All Depths
• Y. Zhao, Probabilistic Methods in Combinatorics

def Cslib.BitString.bernoulliWeight {ι : Type u_1} [Fintype ι] (p : ℝ) (selected : ι → Bool) : ℝ

The probability of the mask selected when each coordinate is selected independently with probability p.

def Cslib.BitString.bernoulliAverage {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f : (ι → Bool) → ℝ) : ℝ

The expectation of f over a random mask selecting each coordinate independently with probability p. It is a probability expectation when 0 ≤ p ≤ 1.

Reindexing and splitting the coordinates

theorem Cslib.BitString.bernoulliWeight_cons {n : ℕ} (p : ℝ) (b : Bool) (selected : Fin n → Bool) : bernoulliWeight p (Fin.cons b selected) = (if b = true then p else 1 - p) * bernoulliWeight p selected

The weight of a mask on Fin (n + 1) is the weight of its first coordinate times the weight of the others.

theorem Cslib.BitString.bernoulliAverage_cons {n : ℕ} (p : ℝ) (f : (Fin (n + 1) → Bool) → ℝ) : bernoulliAverage p f = ((1 - p) * bernoulliAverage p fun (x : Fin n → Bool) => f (Fin.cons false x)) + p * bernoulliAverage p fun (x : Fin n → Bool) => f (Fin.cons true x)

Conditioning on the first coordinate: the expectation over a mask on Fin (n + 1) is the average, with weights 1 - p and p, of the expectations with the first coordinate unselected and selected.

theorem Cslib.BitString.bernoulliWeight_reindex {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (e : ι ≃ κ) (p : ℝ) (s : κ → Bool) : (bernoulliWeight p fun (i : ι) => s (e i)) = bernoulliWeight p s

An equivalence of coordinate types preserves the weights of masks.

theorem Cslib.BitString.bernoulliAverage_reindex {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (e : ι ≃ κ) (p : ℝ) (f : (κ → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => f fun (j : κ) => x (e.symm j)) = bernoulliAverage p f

An equivalence of coordinate types preserves Bernoulli expectations.

theorem Cslib.BitString.bernoulliAverage_sumElim {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] [DecidableEq ι] [DecidableEq κ] (p : ℝ) (h : (ι ⊕ κ → Bool) → ℝ) : bernoulliAverage p h = bernoulliAverage p fun (P₁ : ι → Bool) => bernoulliAverage p fun (P₂ : κ → Bool) => h (Sum.elim P₁ P₂)

Random masks on a disjoint union of coordinates are pairs of independent masks: the expectation over a mask on ι ⊕ κ is the iterated expectation over a mask on ι and one on κ.

Linearity and positivity

theorem Cslib.BitString.bernoulliAverage_mono {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) {f g : (ι → Bool) → ℝ} (hfg : ∀ (x : ι → Bool), f x ≤ g x) : bernoulliAverage p f ≤ bernoulliAverage p g

Bernoulli expectation preserves pointwise inequalities at probability rates.

theorem Cslib.BitString.bernoulliAverage_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p c : ℝ) : (bernoulliAverage p fun (x : ι → Bool) => c) = c

The weights of the masks sum to one, so constants are their own expectations. This holds for every p; the weights are nonnegative when p ∈ [0, 1].

theorem Cslib.BitString.bernoulliAverage_add {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f g : (ι → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => f x + g x) = bernoulliAverage p f + bernoulliAverage p g

Bernoulli expectation is additive.

theorem Cslib.BitString.bernoulliAverage_sub {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f g : (ι → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => f x - g x) = bernoulliAverage p f - bernoulliAverage p g

Bernoulli expectation commutes with subtraction.

theorem Cslib.BitString.bernoulliAverage_const_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p a : ℝ) (f : (ι → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => a * f x) = a * bernoulliAverage p f

Bernoulli expectation commutes with multiplication by a constant.

theorem Cslib.BitString.bernoulliAverage_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} (s : Finset α) (p : ℝ) (f : α → (ι → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => ∑ a ∈ s, f a x) = ∑ a ∈ s, bernoulliAverage p (f a)

Bernoulli expectation commutes with finite sums.

theorem Cslib.BitString.bernoulliAverage_expect_comm {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} (A : Finset α) (p : ℝ) (f : (ι → Bool) → α → ℝ) : (bernoulliAverage p fun (s : ι → Bool) => A.expect fun (x : α) => f s x) = A.expect fun (x : α) => bernoulliAverage p fun (s : ι → Bool) => f s x

Bernoulli expectation commutes with finite averages.

theorem Cslib.BitString.bernoulliAverage_indicator_mem_Icc {ι : Type u_1} [Fintype ι] [DecidableEq ι] (A : Set (ι → Bool)) {p : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) : bernoulliAverage p (A.indicator 1) ∈ Set.Icc 0 1

The probability of a set of masks is between zero and one.

Independence of the coordinates

theorem Cslib.BitString.bernoulliAverage_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (g : ι → Bool → ℝ) : (bernoulliAverage p fun (P : ι → Bool) => ∏ i : ι, g i (P i)) = ∏ i : ι, ((1 - p) * g i false + p * g i true)

The coordinates of a random mask are independent: the average of a product of functions of the separate coordinates is the product of their averages.

theorem Cslib.BitString.bernoulliAverage_restrict {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (s : ι → Bool) (f : ({ i : ι // s i = true } → Bool) → ℝ) : (bernoulliAverage p fun (x : ι → Bool) => f fun (i : { i : ι // s i = true }) => x ↑i) = bernoulliAverage p f

Restricting a Bernoulli mask to fixed coordinates preserves its product law.

theorem Cslib.BitString.bernoulliAverage_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : bernoulliAverage 0 f = f fun (x : ι) => false

Sampling at rate zero selects the empty coordinate set.

theorem Cslib.BitString.bernoulliAverage_coordinate {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (i : ι) : (bernoulliAverage p fun (s : ι → Bool) => if s i = true then 1 else 0) = p

A coordinate is selected with probability p.

theorem Cslib.BitString.bernoulliAverage_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) : (bernoulliAverage p fun (P : ι → Bool) => if ∃ (i : ι), P i = true then 1 else 0) = 1 - (1 - p) ^ Fintype.card ι

A mask is nonempty with probability 1 - (1 - p) ^ |ι|.

theorem Cslib.BitString.bernoulliAverage_weight {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) : (bernoulliAverage p fun (P : ι → Bool) => ↑(weight P)) = ↑(Fintype.card ι) * p

A mask of rate p has |ι| p coordinates on average.

theorem Cslib.BitString.bernoulliAverage_hits {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (s : ι → Bool) : (bernoulliAverage p fun (P : ι → Bool) => if ∃ (i : ι), s i = true ∧ P i = true then 1 else 0) = 1 - (1 - p) ^ weight s

A mask of rate p meets the coordinates selected by s with probability 1 - (1 - p) ^ |s|.

Unions of independent masks

theorem Cslib.BitString.bernoulliAverage_bernoulliAverage_eq_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] {β : Type u_2} [Fintype β] [DecidableEq β] (p q : ℝ) (φ : Bool → Bool → β) (f : (ι → β) → ℝ) : (bernoulliAverage p fun (P : ι → Bool) => bernoulliAverage q fun (Q : ι → Bool) => f fun (i : ι) => φ (P i) (Q i)) = ∑ a : ι → β, f a * ∏ i : ι, ((1 - p) * (((1 - q) * if φ false false = a i then 1 else 0) + q * if φ false true = a i then 1 else 0) + p * (((1 - q) * if φ true false = a i then 1 else 0) + q * if φ true true = a i then 1 else 0))

Coordinatewise images of two independent masks: the expectation of f at the image i ↦ φ (P i) (Q i) of independent masks P and Q of rates p and q is the sum of its values against a product weight, in which each coordinate takes the value b with weight `(1 - p) (1 - q) [φ false false = b] + (1 - p) q [φ false true = b] + p (1 - q) [φ true false = b]

• p q [φ true true = b]`.

theorem Cslib.BitString.bernoulliAverage_union {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p q : ℝ) (f : (ι → Bool) → ℝ) : (bernoulliAverage p fun (r : ι → Bool) => bernoulliAverage q fun (s : ι → Bool) => f fun (i : ι) => r i || s i) = bernoulliAverage (p + q - p * q) f

The union of independent masks of rates p and q has rate p + q - p * q.

theorem Cslib.BitString.bernoulliAverage_bias_antitone {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : Antitone f) {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) (hq : q ≤ 1) : bernoulliAverage q f ≤ bernoulliAverage p f

Increasing the sampling rate decreases the expectation of an antitone function.

Transference for lower sets

theorem Cslib.BitString.bernoulliAverage_lowerSet_union {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Set (ι → Bool)} (hA : IsLowerSet A) {p q : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (hq : 0 ≤ q) (hq' : q ≤ 1) : bernoulliAverage (p + q - p * q) (A.indicator 1) ≤ bernoulliAverage p (A.indicator 1) * bernoulliAverage q (A.indicator 1)

The union of independent masks of rates p and q lies in a lower set only if both masks do, so the probability of a lower set at rate p + q - p q is at most the product of its probabilities at rates p and q.

theorem Cslib.BitString.bernoulliAverage_lowerSet_pow_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Set (ι → Bool)} (hA : IsLowerSet A) {p q : ℝ} (hp : 0 ≤ p) (hp' : p ≤ 1) (hq : q ≤ 1) (h : ℕ) (hh : ↑h * p ≤ q) : bernoulliAverage q (A.indicator 1) ≤ bernoulliAverage p (A.indicator 1) ^ h

Transference for lower sets, with an integer number of repetitions: if h independent masks of rate p have a union of rate at most q (h p ≤ q), then the probability of a lower set at rate q is at most the h-th power of its probability at rate p.