Unrestricted depth-three lower bound: entropy

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

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

theorem Complexity.DepthThreeLowerBound.finite_card_le_of_uniform_weight_lower_bound {α : Type uDepth1} [Fintype α] (A : Finset α) (w : α → ℝ) {δ : ℝ} (hδ : 0 < δ) (hw : ∀ (a : α), 0 ≤ w a) (hsum : ∑ a : α, w a ≤ 1) (hlower : ∀ a ∈ A, δ ≤ w a) : ↑A.card ≤ 1 / δ

def Complexity.DepthThreeLowerBound.bernoulliStringWeight {N : ℕ} (x : ℝ) (z : Fin N → Bool) : ℝ

The product Bernoulli weight of a finite binary string.

Equations

• Complexity.DepthThreeLowerBound.bernoulliStringWeight x z = ∏ i : Fin N, if z i = true then x else 1 - x

theorem Complexity.DepthThreeLowerBound.bernoulliStringWeight_pos {N : ℕ} {x : ℝ} (hx : 0 < x) (hx1 : x < 1) (z : Fin N → Bool) : 0 < bernoulliStringWeight x z

theorem Complexity.DepthThreeLowerBound.sum_bernoulliStringWeight (N : ℕ) (x : ℝ) : ∑ z : Fin N → Bool, bernoulliStringWeight x z = 1

theorem Complexity.DepthThreeLowerBound.log_bernoulliStringWeight {N : ℕ} {x : ℝ} (hx : 0 < x) (hx1 : x < 1) (z : Fin N → Bool) : Real.log (bernoulliStringWeight x z) = ↑N * Real.log (1 - x) + ↑(trueCount z) * (Real.log x - Real.log (1 - x))

theorem Complexity.DepthThreeLowerBound.bernoulliStringWeight_lower_bound {N : ℕ} {x : ℝ} (hx : 0 < x) (hxhalf : x ≤ 1 / 2) (z : Fin N → Bool) (hz : ↑(trueCount z) ≤ ↑N * x) : Real.exp (-(↑N * binaryEntropy x * Real.log 2)) ≤ bernoulliStringWeight x z

noncomputable def Complexity.DepthThreeLowerBound.sparseBinaryStrings (N : ℕ) (x : ℝ) : Finset (Fin N → Bool)

Binary strings satisfying the specified upper bound on true bits.

Equations

• Complexity.DepthThreeLowerBound.sparseBinaryStrings N x = {z : Fin N → Bool | ↑(Complexity.DepthThreeLowerBound.trueCount z) ≤ ↑N * x}

theorem Complexity.DepthThreeLowerBound.card_sparse_binary_strings_le (N : ℕ) {x : ℝ} (hx : 0 < x) (hxhalf : x ≤ 1 / 2) : ↑(sparseBinaryStrings N x).card ≤ 2 ^ (↑N * binaryEntropy x)