Sensitivity separation: parameter bounds

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/ParameterBounds.lean

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

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.parameter_ge_eighty_one {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : 81 ≤ M

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ceil_sqrt_max_le_two_sqrt {M : ℕ} (hM : 81 ≤ M) : ↑(max ⌈√↑M⌉₊ 16) ≤ 2 * √↑M

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.parameter_sqrt_lower {d M : ℕ} (hM : 9 ^ (d + 1) ≤ M) : 3 ^ (d + 1) ≤ √↑M

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.parameter_epsilon_budget {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ↑(max ⌈√↑M⌉₊ 16) / ↑M * 3 ^ (d + 1) ≤ 2

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.parameter_epsilon_le {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ↑(max ⌈√↑M⌉₊ 16) / ↑M ≤ 2 / 3 ^ (d + 1)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.parameter_epsilon_sqrt {d M : ℕ} (hd : 1 ≤ d) (hM : 9 ^ (d + 1) ≤ M) : ↑(max ⌈√↑M⌉₊ 16) / ↑M ≤ 2 / √↑M ∧ 2 / √↑M ≤ 2 / 3 ^ (d + 1)