Min-entropy and weak random sources

The min-entropy of a distribution is the least information content -log₂ p(a) of a possible outcome, measured in bits like Cslib.Probability.PMF.entropy. A distribution has min-entropy at least k exactly when every outcome has probability at most 2⁻ᵏ (le_minEntropy_iff); such a distribution is called a k-source. A (k, ε)-source is within statistical distance ε of a k-source. These are the weak random sources from which randomness extractors produce nearly uniform bits Chor, Goldreich, Vadhan, Chapter 6.

Min-entropy never exceeds Shannon entropy and bounds the collision probability. A mixture of k-sources is a k-source; conversely, every k-source is a mixture of flat k-sources (Cslib.Probability.PMF.exists_eq_bind_uniformOfFinset_of_le_minEntropy). Discarding rare heavy outcomes turns a distribution into a (k, ε)-source (isSource_of_heavy_le).

Main definitions

• Cslib.Probability.PMF.minEntropy: min-entropy in bits.
• Cslib.Probability.PMF.IsSource: (k, ε)-sources.

Main results

• Cslib.Probability.PMF.le_minEntropy_iff: min-entropy at least k means every outcome has probability at most 2⁻ᵏ.
• Cslib.Probability.PMF.minEntropy_le_entropy: min-entropy is at most Shannon entropy.
• Cslib.Probability.PMF.minEntropy_uniformOfFinset: a flat distribution on K outcomes has min-entropy log₂ K.
• Cslib.Probability.PMF.le_minEntropy_bind: a mixture of k-sources is a k-source.
• Cslib.Probability.PMF.collisionProbability_le_rpow_neg_minEntropy: collision probability is at most 2^(-H∞).
• Cslib.Probability.PMF.isSource_zero_iff: a (k, 0)-source is a k-source.
• Cslib.Probability.PMF.isSource_of_heavy_le: discarding rare heavy outcomes gives a (k, ε)-source.

References

• B. Chor, O. Goldreich, Unbiased Bits from Sources of Weak Randomness and Probabilistic Communication Complexity
• S. Vadhan, Pseudorandomness, Chapter 6

Min-entropy

noncomputable def Cslib.Probability.PMF.minEntropy {α : Type u_1} (p : PMF α) : ℝ

Min-entropy in bits: the least information content -log₂ p(a) of a possible outcome a. Its lower bounds are upper bounds on the outcome probabilities (le_minEntropy_iff).

theorem Cslib.Probability.PMF.le_surprisal_iff_mass_le {α : Type u_1} (p : PMF α) {a : α} (ha : a ∈ p.support) {k : ℝ} : k ≤ surprisal p a ↔ (p a).toReal ≤ 2 ^ (-k)

On the support, a lower information bound is exactly an upper probability bound.

theorem Cslib.Probability.PMF.minEntropy_le_surprisal {α : Type u_1} (p : PMF α) {a : α} (ha : a ∈ p.support) : minEntropy p ≤ surprisal p a

Min-entropy is at most the information content of every possible outcome.

theorem Cslib.Probability.PMF.minEntropy_nonneg {α : Type u_1} (p : PMF α) : 0 ≤ minEntropy p

Min-entropy is nonnegative.

theorem Cslib.Probability.PMF.le_minEntropy_iff {α : Type u_1} (p : PMF α) {k : ℝ} : k ≤ minEntropy p ↔ ∀ (a : α), (p a).toReal ≤ 2 ^ (-k)

Min-entropy lower bounds. A distribution has min-entropy at least k exactly when every outcome has probability at most 2⁻ᵏ.

theorem Cslib.Probability.PMF.toReal_apply_le_rpow_neg_minEntropy {α : Type u_1} (p : PMF α) (a : α) : (p a).toReal ≤ 2 ^ (-minEntropy p)

Every outcome has probability at most 2 to the power of minus the min-entropy.

theorem Cslib.Probability.PMF.collisionProbability_le_rpow_neg_minEntropy {α : Type u_1} (p : PMF α) : collisionProbability p ≤ 2 ^ (-minEntropy p)

Collision probability is at most 2 to the power of minus the min-entropy.

theorem Cslib.Probability.PMF.exists_surprisal_eq_minEntropy {α : Type u_1} [Finite α] (p : PMF α) : ∃ a ∈ p.support, surprisal p a = minEntropy p

On a finite type the least information content is attained by some possible outcome.

theorem Cslib.Probability.PMF.minEntropy_le_entropy {α : Type u_1} [Finite α] (p : PMF α) : minEntropy p ≤ entropy p

Min-entropy is at most Shannon entropy, which averages the information content.

theorem Cslib.Probability.PMF.minEntropy_le_logb_card {α : Type u_1} [Fintype α] (p : PMF α) : minEntropy p ≤ Real.logb 2 ↑(Fintype.card α)

Min-entropy is at most the logarithm of the size of a finite type.

theorem Cslib.Probability.PMF.minEntropy_uniformOfFinset {α : Type u_1} (s : Finset α) (hs : s.Nonempty) : minEntropy (uniformOfFinset s hs) = Real.logb 2 ↑s.card

The uniform distribution on a nonempty finite set s has min-entropy log₂ |s|.

@[simp]

theorem Cslib.Probability.PMF.minEntropy_uniformOfFintype {α : Type u_1} [Fintype α] [Nonempty α] : minEntropy (uniformOfFintype α) = Real.logb 2 ↑(Fintype.card α)

The uniform distribution on a finite type has min-entropy the logarithm of its size.

@[simp]

theorem Cslib.Probability.PMF.minEntropy_pure {α : Type u_1} (a : α) : minEntropy (PMF.pure a) = 0

A deterministic value has no min-entropy.

theorem Cslib.Probability.PMF.le_minEntropy_bind {α : Type u_1} {β : Type u_2} (μ : PMF β) (f : β → PMF α) {k : ℝ} (h : ∀ b ∈ μ.support, k ≤ minEntropy (f b)) : k ≤ minEntropy (μ.bind f)

Mixtures of k-sources are k-sources. If every possible component of a mixture has min-entropy at least k, so does the mixture.

Weak random sources

def Cslib.Probability.PMF.IsSource {α : Type u_1} [Fintype α] (p : PMF α) (k : ℝ) (ε : NNReal) : Prop

A (k, ε)-source: a distribution within statistical distance ε of one with min-entropy at least k. A k-source is a (k, 0)-source (isSource_zero_iff).

@[simp]

theorem Cslib.Probability.PMF.isSource_zero_iff {α : Type u_1} [Fintype α] (p : PMF α) {k : ℝ} : IsSource p k 0 ↔ k ≤ minEntropy p

A (k, 0)-source is exactly a distribution of min-entropy at least k.

theorem Cslib.Probability.PMF.isSource_of_le_minEntropy {α : Type u_1} [Fintype α] {p : PMF α} {k : ℝ} (h : k ≤ minEntropy p) (ε : NNReal) : IsSource p k ε

A distribution of min-entropy at least k is a (k, ε)-source for every ε.

theorem Cslib.Probability.PMF.IsSource.mono {α : Type u_1} [Fintype α] {p : PMF α} {k k' : ℝ} {ε ε' : NNReal} (h : IsSource p k ε) (hk : k' ≤ k) (hε : ε ≤ ε') : IsSource p k' ε'

Sources remain sources with less min-entropy and more error.

theorem Cslib.Probability.PMF.IsSource.of_statisticallyClose {α : Type u_1} [Fintype α] {p q : PMF α} {k : ℝ} {ε δ : NNReal} (h : IsSource q k ε) (hpq : StatisticallyClose p q δ) : IsSource p k (δ + ε)

A distribution δ-close to a (k, ε)-source is a (k, δ + ε)-source.

theorem Cslib.Probability.PMF.isSource_of_heavy_le {α : Type u_1} [Fintype α] (p : PMF α) {k : ℝ} {δ : NNReal} (hδ : ↑δ < 1) (hheavy : (p.toOuterMeasure {a : α | 2 ^ (-k) < (p a).toReal}).toReal ≤ ↑δ) : IsSource p (k + Real.logb 2 (1 - ↑δ)) δ

Smoothing by discarding heavy outcomes. If the outcomes of probability more than 2⁻ᵏ have total probability at most δ < 1, the distribution is a (k + log₂ (1 - δ), δ)-source. Conditioning on the light outcomes moves it by the discarded probability and multiplies each remaining mass by at most 1 / (1 - δ). For δ ≤ 1 / 2 the min-entropy loss is at most one bit.