Unrestricted depth-three lower bound: sparse tail bounds

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

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

theorem Complexity.DepthThreeLowerBound.nat_pow_eq_two_rpow (x : ℝ) (hx : 0 < x) (n : ℕ) : x ^ n = 2 ^ (↑n * (Real.log x / Real.log 2))

theorem Complexity.DepthThreeLowerBound.sparse_count_le_two_rpow (m b L : ℕ) : ((2 * ↑m + 1) ^ b + 1) ^ L ≤ 2 ^ (↑L * (1 + ↑b * (Real.log (2 * ↑m + 1) / Real.log 2)))

theorem Complexity.DepthThreeLowerBound.sparseTestCode_card_le_two_rpow {V : Type uDepth1} [Fintype V] (b L : ℕ) : ↑(Fintype.card (SparseTestCode V b L)) ≤ 2 ^ (↑L * (1 + ↑b * (Real.log (2 * ↑(Fintype.card V) + 1) / Real.log 2)))

theorem Complexity.DepthThreeLowerBound.sparse_moment_union_le {V : Type uDepth2} [Fintype V] (b M t : ℕ) (hm : 0 < Fintype.card V) (ht : 0 < t) (hcond : ↑M * (1 + ↑b * (Real.log (2 * ↑(Fintype.card V) + 1) / Real.log 2)) / ↑t + Real.log ↑t / Real.log 2 / ↑(Fintype.card V) ≤ 1 / 8) : ↑(Fintype.card (SparseTestCode V b (M * Fintype.card V))) * ↑t ^ t * 2 ^ (-(↑(Fintype.card V) * ↑t) / 4) ≤ 2 ^ (-(↑(Fintype.card V) * ↑t) / 8)