Counting events that fix selected independent coordinates #
Forcing k distinct Boolean coordinates leaves at most a 2⁻ᵏ fraction of the
cube. The proof injects the event into the unused coordinate assignments.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Entropy.pow_card_mul_card_le_of_forces_coordinates
{I : Type u_1}
{V : Type u_2}
[Fintype I]
[Fintype V]
[DecidableEq I]
[DecidableEq V]
(e : I ↪ V)
(bits : I → Bool)
(P : (V → Bool) → Prop)
[DecidablePred P]
(forced : ∀ (x : V → Bool), P x → x ∘ ⇑e = bits)
:
An event fixing every selected coordinate occupies at most one corresponding cube fibre.