Korten's conditional-fiber entropy lemma

Lemma 4 of Oliver Korten, Top-Down Lower Bounds for All Depths, ECCC TR26-221 (2026), https://eccc.weizmann.ac.il/report/2026/221/.

For a nonempty cube subset X, conditioning on the coordinates outside s does not increase its average uniform min-entropy deficit. The fiber is represented on the selected-coordinate cube, and card_coordinateFiber identifies it with the full-cube set of points agreeing outside s.

coordinateFiber_good_probability is the 63/64 consequence used in the mirror-set argument. The uniform-mass API connects a deficit bound to the pointwise probability bound required by the light-patterns lemma.

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

Uniform masses are nonnegative, including for the empty set.

theorem Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.uniformDeficit_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X : Finset (ι → Bool)) : 0 ≤ uniformDeficit X

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

theorem Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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.

theorem Complexity.BooleanAnalysis.expect_restrict_coordinates {ι : Type u_1} [Fintype ι] [DecidableEq ι] (s : ι → Bool) (f : ({ i : ι // s i = true } → Bool) → ℝ) : (Finset.univ.expect fun (x : ι → Bool) => f fun (i : { i : ι // s i = true }) => x ↑i) = Finset.univ.expect fun (x : { i : ι // s i = true } → Bool) => f x

Uniform resampling on the whole cube restricts to uniform sampling on any fixed selected-coordinate subtype.

theorem Complexity.BooleanAnalysis.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

Whole-cube resampling completes the restriction of the sampled point.

theorem Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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 Complexity.BooleanAnalysis.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.