Unrestricted depth-three lower bound: cylinder probability

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

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

theorem Complexity.DepthThreeLowerBound.finiteAvg_eq_pattern {V : Type uDepth1} [Fintype V] (U : Finset V) (σ : Cube V) : (finiteAvg fun (x : Cube V) => if ∀ v ∈ U, x v = σ v then 1 else 0) = (2 ^ U.card)⁻¹

theorem Complexity.DepthThreeLowerBound.finiteAvg_indicator_eq_pattern {V : Type uDepth1} [Fintype V] (U : Finset V) (σ : Cube V) : (finiteAvg fun (x : Cube V) => indicator (decide (∀ v ∈ U, x v = σ v))) = (2 ^ U.card)⁻¹