PFR

Let X,Y,X' be independent G-valued random variables, with X' a copy of X, and let a be an integer. Then H[X - (a-1)Y] ≤ H[X - aY] + H[X - Y - X'] - H[X]

Let X,Y be independent G-valued random variables, and let a be an integer. Then H[X - aY] - H[X] ≤ 4 |a| d[X ; Y].

Move to Mathlib?

If φ : {1, ..., m} → {1, ...,m} is a bijection, then D[X_[m]] = D[(X_φ(1), ..., X_φ(m))].

To prove multidist_ruzsa_I, we first establish a special case when the random variables are defined on the same space and are jointly independent.

Let m ≥ 1, and let X_[m] be a tuple of G-valued random variables. Then ∑ (1 ≤ j, k ≤ m, j ≠ k), d[X_j; -X_k] ≤ m(m - 1) D[X_[m]].

Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Then ∑ j, d[X_j;X_j] ≤ 2 m D[X_[m]].

A version of multidist_ruzsa_III assuming independence.

Let I be an indexing set of size m ≥ 2, and let X_[m] be a tuple of G-valued random variables. If the X_i all have the same distribution, then D[X_[m]] ≤ m d[X_i;X_i] for any 1 ≤ i ≤ m.

Let m ≥ 2, and let X_[m] be a tuple of G-valued random variables. Let W := ∑ X_i. Then d[W;-W] ≤ 2 D[X_i].

If D[X_[m]]=0, then for each i ∈ I there is a finite subgroup H_i ≤ G such that d[X_i; U_{H_i}] = 0.

Conditional multidistance is unchanged if we apply an injection to the conditioned variables

Conditional multidistance against a constant is just multidistance

Conditional multidistance is nonnegative.

If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = H[∑ i, X_i | (Y_1, ..., Y_m)] - 1/m * ∑ i, H[X_i | Y_i]

If (X_i, Y_i), 1 ≤ i ≤ m are independent, then D[X_[m] | Y_[m]] = ∑_{(y_i)_{1 ≤ i ≤ m}} P(Y_i=y_i ∀ i) D[(X_i | Y_i=y_i ∀ i)_{i=1}^m].

Let π : G → H be a homomorphism of abelian groups and let X_[m] be a tuple of jointly independent G-valued random variables. Then D[X_[m]] is equal to D[X_[m] | π(X_[m])] + D[π(X_[m])] + I[∑ i, X_i : π(X_[m]) ; | ; π(∑ i, X_i)] where π(X_[m]) := (π(X_1), ..., π(X_m)).

Let π : G → H be a homomorphism of abelian groups. Let I be a finite index set and let X_[m] be a tuple of G-valued random variables. Let Y_[m] be another tuple of random variables (not necessarily G-valued). Suppose that the pairs (X_i, Y_i) are jointly independent of one another (but X_i need not be independent of Y_i). Then D[X_[m] | Y_[m]] = D[X_[m] ,|, π(X_[m]), Y_[m]] + D[π(X_[m]) ,| , Y_[m]] + I[∑ i, X_i : π(X_[m]) ; | ; π(∑ i, X_i), Y_[m]].