Korten's light-patterns lemma

Let mass be a distribution on the points of the cube ι → Bool with min-entropy deficit at most k, that is, mass x ≤ 2 ^ (k - |ι|). Select each coordinate independently with rate r ≤ 1 / (512 k). With probability at least 63 / 64, at most 2 ^ (|R| - k) patterns on the selected coordinates R are light, of marginal probability at most 2 ^ (-|R| - 2 k - 2) Korten, Lemma 10 (bernoulliAverage_few_light_patterns).

The proof transfers a lower set of masks from rate 1 / 4 to a small rate r: its probability at rate r is at least its probability at rate 1 / 4 to the power 5 r (bernoulliAverage_lowerSet_transfer). The masks on which the harmonic mean transform of the density of mass is large form such a lower set, of probability at least 2 ^ (-k / 2 - 1) at rate 1 / 4 (harmonicTransform_good_probability), so they have probability at least 63 / 64 at rate r (harmonicTransform_sparse_good_probability). On these masks the harmonic mean bounds the number of light patterns.

Main definitions

• Cslib.BitString.coordinateMass: the marginal of a distribution on the selected coordinates.

Main results

• Cslib.BitString.bernoulliAverage_lowerSet_transfer: transference for lower sets at a small rate.
• Cslib.BitString.harmonicTransform_sparse_good_probability: the harmonic mean transform at a sparse random set.
• Cslib.BitString.bernoulliAverage_few_light_patterns: Korten's light-patterns lemma.
• Cslib.BitString.bernoulliAverage_few_light_patterns_density: the same, for densities.

References

• O. Korten, Top-Down Lower Bounds for All Depths

Transference at a small rate

theorem Cslib.BitString.bernoulliAverage_lowerSet_transfer {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : Set (ι → Bool)} (hA : IsLowerSet A) (hA' : A.Nonempty) {r : ℝ} (hr : 0 ≤ r) (hr' : r ≤ 1 / 20) : bernoulliAverage (1 / 4) (A.indicator 1) ^ (5 * r) ≤ bernoulliAverage r (A.indicator 1)

Transference for lower sets at a small rate r ≤ 1 / 20: the probability of a nonempty lower set at rate r is at least its probability at rate 1 / 4 to the power 5 r, as in the proof of Korten, Lemma 10. Nonemptiness covers r = 0, where the right side is one.

The harmonic mean transform at a sparse random set

theorem Cslib.BitString.harmonicTransform_sparse_good_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : ι → Bool) => f x) = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : ι → Bool), f x ≤ 2 ^ k) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : ι → Bool) => if 1 / (4 * 2 ^ k) ≤ harmonicTransform f s then 1 else 0

The harmonic mean transform at a sparse random set, as in the proof of Korten, Lemma 10: for a density f relative to the uniform distribution bounded by 2 ^ k, k ≥ 1, the transform at a random set of rate r ≤ 1 / (512 k) is at least 1 / (4 · 2 ^ k) with probability at least 63 / 64.

theorem Cslib.BitString.bernoulliAverage_few_light_patterns_density {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (hmean : (Finset.univ.expect fun (x : ι → Bool) => f x) = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : ι → Bool), f x ≤ 2 ^ k) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : ι → Bool) => if (Finset.univ.expect fun (z : { i : ι // s i = true } → Bool) => if coordinateMarginal f s z ≤ 2 ^ (-2 * k - 2) then 1 else 0) ≤ 2 ^ (-k) then 1 else 0

Korten's light-patterns lemma for densities: with probability at least 63 / 64, the fraction of patterns of marginal density at most 2 ^ (-2 k - 2) is at most 2 ^ (-k).

Marginal probability masses on coordinate patterns

The marginal of a probability mass function on the cube sums its masses over the completions of a pattern on the selected coordinates. It is the marginal coordinateMarginal of the density relative to the uniform distribution, scaled by the number of patterns.

def Cslib.BitString.coordinateMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (mass : (ι → Bool) → ℝ) (selected : ι → Bool) (pattern : { i : ι // selected i = true } → Bool) : ℝ

Sum of the masses of all completions of a coordinate pattern. For a nonnegative mass function summing to one, this is the probability of the pattern.

theorem Cslib.BitString.sum_coordinateMass {ι : Type u_1} [Fintype ι] [DecidableEq ι] (mass : (ι → Bool) → ℝ) (s : ι → Bool) : ∑ z : { i : ι // s i = true } → Bool, coordinateMass mass s z = ∑ x : ι → Bool, mass x

Marginalization preserves total probability mass.

theorem Cslib.BitString.coordinateMass_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mass : (ι → Bool) → ℝ} (hm : ∀ (x : ι → Bool), 0 ≤ mass x) (s : ι → Bool) (z : { i : ι // s i = true } → Bool) : 0 ≤ coordinateMass mass s z

Marginal masses of a nonnegative mass function are nonnegative.

theorem Cslib.BitString.coordinateMass_eq_mul_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (mass : (ι → Bool) → ℝ) (s : ι → Bool) (z : { i : ι // s i = true } → Bool) : coordinateMass mass s z = 2 ^ Fintype.card { i : ι // s i ≠ true } * coordinateMarginal mass s z

The marginal mass of a pattern is the marginal of mass at the pattern times the number 2 ^ |{i | s i ≠ true}| of its completions.

Korten's light-patterns lemma

theorem Cslib.BitString.bernoulliAverage_few_light_patterns {ι : Type u_1} [Fintype ι] [DecidableEq ι] {mass : (ι → Bool) → ℝ} (hm : ∀ (x : ι → Bool), 0 ≤ mass x) (hmean : ∑ x : ι → Bool, mass x = 1) {k r : ℝ} (hk : 1 ≤ k) (hbound : ∀ (x : ι → Bool), mass x ≤ 2 ^ (k - ↑(Fintype.card ι))) (hr : 0 ≤ r) (hr' : r ≤ 1 / (512 * k)) : 63 / 64 ≤ bernoulliAverage r fun (s : ι → Bool) => if ↑{z : { i : ι // s i = true } → Bool | coordinateMass mass s z ≤ 2 ^ (-↑(Fintype.card { i : ι // s i = true }) - 2 * k - 2)}.card ≤ 2 ^ (↑(Fintype.card { i : ι // s i = true }) - k) then 1 else 0

Korten's light-patterns lemma Korten, Lemma 10, with its constants and pattern count. Nonnegative masses summing to one represent a distribution; the pointwise bound is min-entropy deficit at most the real parameter k.