Density and coordinate-resampling identities

Uniform cube densities normalize probability masses. Completing a selected pattern identifies the fraction of a fiber with its resampling probability. These identities connect Korten's entropy and light-patterns lemmas.

theorem Complexity.BooleanAnalysis.expect_restrict_coordinates_internal {ι : 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

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

theorem Complexity.BooleanAnalysis.coordinateDensity_eq_expect_internal {ι : 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

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

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

theorem Complexity.BooleanAnalysis.uniformDensity_eq_deficit_internal {ι : 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