Unrestricted depth-three lower bound: asymptotic bounds

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

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

theorem Complexity.DepthThreeLowerBound.exists_factorial_tail_width (Q : ℝ) (hQ : 0 ≤ Q) : ∃ (b : ℕ), 1 ≤ b ∧ ∀ (k : ℕ), ∑ ℓ ∈ Finset.Ico (b + 1) (k + 1), Q ^ ℓ / ↑ℓ.factorial ≤ 1 / 2

theorem Complexity.DepthThreeLowerBound.div_five_ge (D n : ℕ) (h : 5 * D ≤ n) : D ≤ n / 5

theorem Complexity.DepthThreeLowerBound.input_div_five_scale (n : ℕ) (hn : 5 ≤ n) : 0 < n / 5 ∧ n ≤ 9 * (n / 5)

theorem Complexity.DepthThreeLowerBound.sqrt_input_div_five_le (n : ℕ) (hn : 5 ≤ n) : √↑n ≤ 3 * √↑(n / 5)

theorem Complexity.DepthThreeLowerBound.circuit_size_scale (A : ℝ) (hA : 0 ≤ A) (n : ℕ) (hn : 5 ≤ n) : 2 ^ (A * √↑n) ≤ 2 ^ (3 * A * √↑(n / 5))

theorem Complexity.DepthThreeLowerBound.final_error_exponents (s d S : ℝ) (hS0 : 0 ≤ S) (hS : S ≤ 2 ^ (s * √d)) (k : ℕ) (hk : 3 * (s + 1) * √d ≤ ↑k) : 6 * S * 2 ^ (-(64 * (s + 1) * √d) / 16) + S ^ 2 * 2 ^ (-↑k) ≤ 6 * 2 ^ (-((3 * s + 4) * √d)) + 2 ^ (-((s + 3) * √d))

theorem Complexity.DepthThreeLowerBound.final_error_le (s d S : ℝ) (hs : 0 ≤ s) (hd : 4 ≤ d) (hS0 : 0 ≤ S) (hS : S ≤ 2 ^ (s * √d)) (k : ℕ) (hk : 3 * (s + 1) * √d ≤ ↑k) : 6 * S * 2 ^ (-(64 * (s + 1) * √d) / 16) + S ^ 2 * 2 ^ (-↑k) ≤ 5 / 128

theorem Complexity.DepthThreeLowerBound.correlation_error_le (s d : ℝ) (hs : 0 ≤ s) (hd : 1 ≤ d) : 6 * 2 ^ (-(4 * (s + 1) * √d)) ≤ 3 / 8