Unrestricted depth-three lower bound: entropy bits

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/DepthThree/EntropyBits.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical proofs are retained.

def Complexity.DepthThreeLowerBound.trueCount {N : ℕ} (z : Fin N → Bool) : ℕ

Count the true bits of a binary string.

Equations

• Complexity.DepthThreeLowerBound.trueCount z = {i : Fin N | z i = true}.card

theorem Complexity.DepthThreeLowerBound.trueCount_le {N : ℕ} (z : Fin N → Bool) : trueCount z ≤ N

theorem Complexity.DepthThreeLowerBound.trueCount_cast {N : ℕ} (z : Fin N → Bool) : ↑(trueCount z) = ∑ i : Fin N, if z i = true then 1 else 0