Coordinate fibers and Korten's entropy lemma

Fix a set s : ι → Bool of coordinates of the cube ι → Bool. Completing a pattern on s by the coordinates of a point x outside s (completePattern) and replacing the coordinates of x in s by those of a point y (resample) glue points of the cube along s. The fiber of a set X of points over the coordinates of x outside s is a set of patterns on s (coordinateFiber), and its density (coordinateDensity) is the probability that resampling the coordinates in s lands in X (coordinateDensity_eq_expect). Averaging a function over the coordinates outside s projects it to s, either as a function on the cube (projectionAverage) or as a function of the patterns on s (coordinateMarginal).

The min-entropy deficit of a nonempty set X of points is |ι| - log₂ |X| (uniformDeficit). Conditioning on the coordinates outside s does not increase the average deficit Korten, Lemma 4 (expect_uniformDeficit_coordinateFiber), so by Markov's inequality most points of X have fibers of small deficit (coordinateFiber_good_probability). By the pigeonhole principle, a map from X to at most 2 ^ m values has a nonempty fiber of deficit at most m more than that of X (exists_uniformDeficit_fiber_le). The density of X relative to the uniform distribution (uniformDensity) connects deficits to the pointwise bounds of the light-patterns lemma.

Main definitions

• Cslib.BitString.uniformMass, Cslib.BitString.uniformDensity: the uniform distribution on a set, and its density.
• Cslib.BitString.uniformDeficit: the min-entropy deficit of a set.
• Cslib.BitString.completePattern, Cslib.BitString.resample: gluing points along a set of coordinates.
• Cslib.BitString.coordinateFiber, Cslib.BitString.coordinateDensity: the fiber of a set over the coordinates outside s, and its density.
• Cslib.BitString.projectionAverage, Cslib.BitString.coordinateMarginal: averages over the coordinates outside s.

Main results

• Cslib.BitString.expect_uniformDeficit_coordinateFiber: Korten's entropy lemma.
• Cslib.BitString.coordinateFiber_good_probability: most fibers have small deficit.
• Cslib.BitString.exists_uniformDeficit_fiber_le: pigeonhole for deficits.
• Cslib.BitString.uniformMass_le_rpow, Cslib.BitString.uniformDensity_le_rpow: a deficit bound bounds the uniform probability mass and density pointwise.
• Cslib.BitString.coordinateDensity_eq_expect: the density of a fiber is the probability that resampling the coordinates in s lands in the set.
• Cslib.BitString.projectionAverage_eq_coordinateMarginal, Cslib.BitString.expect_projectionAverage, Cslib.BitString.expect_resample: the two projections agree, and projecting or resampling preserves the mean.
• Cslib.BitString.expect_half_of_flip, Cslib.BitString.coordinateDensity_half_of_flip: a Boolean function that flips with a coordinate is true on half of the cube, and on half of every fiber that frees the coordinate.

References

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

Uniform distributions and min-entropy deficits

noncomputable def Cslib.BitString.uniformMass {α : Type u_1} [DecidableEq α] (X : Finset α) (x : α) : ℝ

Uniform probability mass on a nonempty finite set; zero off the set. The empty set gives the zero mass function.

noncomputable def Cslib.BitString.uniformDeficit {ι : Type u_1} [Fintype ι] (X : Finset (ι → Bool)) : ℝ

Min-entropy deficit of the uniform distribution on a nonempty Boolean cube subset. The real formula takes value card ι at the empty set because Real.logb 2 0 = 0; entropy interpretations require nonemptiness.

noncomputable def Cslib.BitString.uniformDensity {ι : Type u_1} [Fintype ι] (X : Finset (ι → Bool)) (x : ι → Bool) : ℝ

Density of uniform mass relative to the uniform Boolean cube. Its uniform cube expectation is one when X is nonempty.

theorem Cslib.BitString.uniformMass_nonneg {α : Type u_1} [DecidableEq α] (X : Finset α) (x : α) : 0 ≤ uniformMass X x

Uniform masses are nonnegative, including for the empty set.

theorem Cslib.BitString.sum_uniformMass {α : Type u_1} [Fintype α] [DecidableEq α] {X : Finset α} (hX : X.Nonempty) : ∑ x : α, uniformMass X x = 1

Uniform mass on a nonempty finite set sums to one.

theorem Cslib.BitString.sum_uniformMass_mul {α : Type u_1} [Fintype α] [DecidableEq α] (X : Finset α) (f : α → ℝ) : ∑ x : α, uniformMass X x * f x = X.expect fun (x : α) => f x

Summing against uniform mass agrees with the finite-set expectation.

theorem Cslib.BitString.uniformDensity_nonneg {ι : Type u_1} [Fintype ι] (X : Finset (ι → Bool)) (x : ι → Bool) : 0 ≤ uniformDensity X x

Uniform densities are nonnegative, including for the empty set.

theorem Cslib.BitString.uniformDeficit_nonneg {ι : Type u_1} [Fintype ι] (X : Finset (ι → Bool)) : 0 ≤ uniformDeficit X

Uniform deficits are nonnegative. For the empty set this follows from the documented real-logarithm convention.

theorem Cslib.BitString.card_eq_rpow_sub_uniformDeficit {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) : ↑X.card = 2 ^ (↑(Fintype.card ι) - uniformDeficit X)

A nonempty subset has cardinality 2^(dimension - deficit).

theorem Cslib.BitString.uniformDeficit_le_iff {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) {k : ℝ} : uniformDeficit X ≤ k ↔ 2 ^ (↑(Fintype.card ι) - k) ≤ ↑X.card

A deficit bound is equivalent to the corresponding density lower bound when the subset is nonempty.

theorem Cslib.BitString.uniformMass_le_rpow {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) {k : ℝ} (hdef : uniformDeficit X ≤ k) (x : ι → Bool) : uniformMass X x ≤ 2 ^ (k - ↑(Fintype.card ι))

A uniform deficit bound implies the light-patterns lemma's pointwise probability-mass hypothesis.

theorem Cslib.BitString.uniformDensity_le_rpow {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) {k : ℝ} (hk : uniformDeficit X ≤ k) (x : ι → Bool) : uniformDensity X x ≤ 2 ^ k

Entropy deficit bounds the normalized density pointwise.

theorem Cslib.BitString.uniformDensity_eq_deficit {ι : Type u_1} [Fintype ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) (z : ι → Bool) : uniformDensity X z = 2 ^ uniformDeficit X * if z ∈ X then 1 else 0

The density is 2^deficit on the nonempty set and zero elsewhere.

theorem Cslib.BitString.expect_uniformDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Finset (ι → Bool)} (hX : X.Nonempty) : (Finset.univ.expect fun (x : ι → Bool) => uniformDensity X x) = 1

Normalization of the density of a nonempty finite cube subset.

theorem Cslib.BitString.exists_uniformDeficit_fiber_le {ι : Type u_1} {M : Type u_2} [Fintype ι] [Fintype M] [DecidableEq M] (X : Finset (ι → Bool)) (hX : X.Nonempty) (send : (ι → Bool) → M) {m : ℝ} (hm : ↑(Fintype.card M) ≤ 2 ^ m) : ∃ (a : M), {x ∈ X | send x = a}.Nonempty ∧ uniformDeficit ({x ∈ X | send x = a}) ≤ uniformDeficit X + m

Pigeonhole for deficits: some fiber of a map from a nonempty set X to a type of at most 2 ^ m elements is nonempty, of deficit at most the deficit of X plus m.

Gluing points along a set of coordinates

def Cslib.BitString.completePattern {ι : Type u_1} (s x : ι → Bool) (z : { i : ι // s i = true } → Bool) : ι → Bool

Insert a pattern on selected coordinates, retaining x elsewhere.

def Cslib.BitString.resample {ι : Type u_1} (s x y : ι → Bool) : ι → Bool

Replace selected coordinates of x by those of y.

def Cslib.BitString.coordinateFiber {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : Finset ({ i : ι // s i = true } → Bool)

The fiber of X over the bits of x outside s, represented on the selected-coordinate cube. This is Korten's X_{x,S} inside its own subcube.

noncomputable def Cslib.BitString.coordinateDensity {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : ℝ

Fraction of the free-coordinate cube over x that belongs to X.

noncomputable def Cslib.BitString.projectionAverage {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected x : ι → Bool) : ℝ

The average of f over the coordinates outside selected, keeping the selected coordinates of x. It depends only on the selected coordinates of x.

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

The marginal of f on the patterns on the selected coordinates: the average of f over the completions of a pattern. For a density f relative to the uniform distribution, it is the density of the projection to the selected coordinates.

@[simp]

theorem Cslib.BitString.resample_false {ι : Type u_1} (x y : ι → Bool) : resample (fun (x : ι) => false) x y = x

Resampling no coordinates leaves the point unchanged.

@[simp]

theorem Cslib.BitString.resample_true {ι : Type u_1} (x y : ι → Bool) : resample (fun (x : ι) => true) x y = y

Resampling all coordinates gives the source point.

theorem Cslib.BitString.resample_eq_piecewise {ι : Type u_1} (s x y : ι → Bool) : resample s x y = {i : ι | s i = true}.piecewise y x

Resampling is Set.piecewise on the selected coordinates.

theorem Cslib.BitString.resample_eq_completePattern {ι : Type u_1} (s x y : ι → Bool) : resample s x y = completePattern s x fun (i : { i : ι // s i = true }) => y ↑i

Resampling completes the restriction of the sampled point.

theorem Cslib.BitString.resample_not {ι : Type u_1} (s x y : ι → Bool) : resample (fun (i : ι) => !s i) x y = resample s y x

Resampling the coordinates outside s of x from y is resampling the coordinates in s of y from x.

theorem Cslib.BitString.card_coordinateFiber {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : (coordinateFiber X s x).card = {y ∈ X | (fun (i : { i : ι // s i ≠ true }) => y ↑i) = fun (i : { i : ι // s i ≠ true }) => x ↑i}.card

The free-coordinate fiber counts exactly the full assignments in X whose unselected coordinates agree with x.

theorem Cslib.BitString.coordinateFiber_nonempty {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X : Finset (ι → Bool)} (s : ι → Bool) {x : ι → Bool} (hx : x ∈ X) : (coordinateFiber X s x).Nonempty

Conditioning at a point of X leaves a nonempty fiber.

theorem Cslib.BitString.coordinateDensity_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : 0 ≤ coordinateDensity X s x

Fiber densities are nonnegative, including for empty fibers.

theorem Cslib.BitString.coordinateDensity_eq_expect {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : coordinateDensity X s x = Finset.univ.expect fun (y : ι → Bool) => if resample s x y ∈ X then 1 else 0

The fraction of a fiber is the probability that coordinate resampling lands in the set.

theorem Cslib.BitString.coordinateDensity_resample_union {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (P Q x y : ι → Bool) : coordinateDensity X Q (resample P x y) = coordinateDensity X Q (resample (fun (i : ι) => P i || Q i) x y)

Resampling x on P ∪ Q instead of P does not change the density of its fiber over the coordinates outside Q.

Projections to a set of coordinates

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

An equivalence of coordinate types commutes with projections.

theorem Cslib.BitString.projectionAverage_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (selected x : ι → Bool) : 0 ≤ projectionAverage f selected x

Projections of nonnegative functions are nonnegative.

theorem Cslib.BitString.projectionAverage_const_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] (a : ℝ) (f : (ι → Bool) → ℝ) (s x : ι → Bool) : projectionAverage (fun (y : ι → Bool) => a * f y) s x = a * projectionAverage f s x

Projection commutes with multiplication by a constant.

theorem Cslib.BitString.coordinateMarginal_eq_expect_completePattern {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (s : ι → Bool) (z : { i : ι // s i = true } → Bool) : coordinateMarginal f s z = Finset.univ.expect fun (x : ι → Bool) => f (completePattern s x z)

The marginal of f at a pattern is the average of f at the completions of the pattern by a uniform point.

theorem Cslib.BitString.projectionAverage_eq_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected x : ι → Bool) : projectionAverage f selected x = coordinateMarginal f selected fun (i : { i : ι // selected i = true }) => x ↑i

The projection of f at x is its marginal at the selected coordinates of x.

theorem Cslib.BitString.expect_coordinateMarginal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (selected : ι → Bool) : (Finset.univ.expect fun (z : { i : ι // selected i = true } → Bool) => coordinateMarginal f selected z) = Finset.univ.expect fun (x : ι → Bool) => f x

Marginalization preserves the uniform mean, hence also density normalization.

theorem Cslib.BitString.expect_comp_projectionAverage {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (s : ι → Bool) (g : ℝ → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => g (projectionAverage f s x)) = Finset.univ.expect fun (z : { i : ι // s i = true } → Bool) => g (coordinateMarginal f s z)

The values of the projection of f at a uniform point are distributed as the values of its marginal at a uniform pattern.

theorem Cslib.BitString.expect_projectionAverage {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (s : ι → Bool) : (Finset.univ.expect fun (x : ι → Bool) => projectionAverage f s x) = Finset.univ.expect fun (x : ι → Bool) => f x

Projection preserves the uniform mean.

theorem Cslib.BitString.expect_resample {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (P : ι → Bool) : (Finset.univ.expect fun (x : ι → Bool) => Finset.univ.expect fun (y : ι → Bool) => f (resample P x y)) = Finset.univ.expect fun (z : ι → Bool) => f z

Resampling the coordinates in P of a uniform point gives a uniform point.

theorem Cslib.BitString.expect_resample_subset_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) {f : (ι → Bool) → ℝ} (hf : ∀ (x : ι → Bool), 0 ≤ f x) (P : ι → Bool) : (X.expect fun (x : ι → Bool) => Finset.univ.expect fun (y : ι → Bool) => f (resample P x y)) ≤ (∑ z : ι → Bool, f z) / ↑X.card

When the coordinates in P of a uniform point of X are resampled, each point of the cube has probability at most 1 / |X|, so the average of a nonnegative function is at most its sum divided by |X|.

theorem Cslib.BitString.coordinateDensity_eq_projectionAverage {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (s x : ι → Bool) : coordinateDensity X s x = projectionAverage (fun (y : ι → Bool) => if y ∈ X then 1 else 0) (fun (i : ι) => !s i) x

The density of the fiber of X over the coordinates of x outside s is the projection of the indicator of X to the coordinates outside s.

theorem Cslib.BitString.projectionAverage_comp_completePattern {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) (s x : ι → Bool) (R u : { i : ι // s i = true } → Bool) : projectionAverage (fun (z : { i : ι // s i = true } → Bool) => f (completePattern s x z)) R u = projectionAverage f (fun (i : ι) => if h : s i = true then R ⟨i, h⟩ else true) (completePattern s x u)

Projecting the restriction of f to the fiber over x, a function of the patterns on s, to the coordinates R is projecting f to R together with the coordinates outside s.

Korten's entropy lemma

theorem Cslib.BitString.expect_uniformDeficit_coordinateFiber {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (hX : X.Nonempty) (s : ι → Bool) : (X.expect fun (x : ι → Bool) => uniformDeficit (coordinateFiber X s x)) ≤ uniformDeficit X

Korten's entropy lemma (Lemma 4): conditioning on the unselected bits does not increase the average deficit in the selected-coordinate cube.

theorem Cslib.BitString.coordinateFiber_good_probability {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) (hX : X.Nonempty) (s : ι → Bool) {k : ℝ} (hk : 0 < k) (hdef : uniformDeficit X ≤ k) : 63 / 64 ≤ X.expect fun (x : ι → Bool) => if uniformDeficit (coordinateFiber X s x) ≤ 64 * k then 1 else 0

For every fixed set of free coordinates, a uniform point of X yields a fiber of deficit at most 64*k with probability at least 63/64.

Functions that flip with a coordinate

theorem Cslib.BitString.expect_half_of_flip {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) (hf : ∀ (x : ι → Bool), f (Function.update x i !x i) = !f x) (b : Bool) : (Finset.univ.expect fun (x : ι → Bool) => if f x = b then 1 else 0) = 1 / 2

A Boolean function that flips with one coordinate is true on half of the cube.

theorem Cslib.BitString.coordinateDensity_half_of_flip {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) (hf : ∀ (x : ι → Bool), f (Function.update x i !x i) = !f x) (P x : ι → Bool) (hi : P i = true) (b : Bool) : coordinateDensity {z : ι → Bool | f z = b} P x = 1 / 2

A Boolean function that flips with the coordinate i is true on half of every fiber over a set of coordinates containing i.