Sensitivity separation: scalar bounds

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/ScalarBounds.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.geometric_error_le {d n : ℕ} (hn : n ≤ d) {ε L : ℝ} (hε : 0 ≤ ε) (hL : 0 ≤ L) (hbudget : ε * 3 ^ (d + 1) ≤ 2) : 3 / 2 * ε * L * (3 ^ n - 1) ≤ L

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.coupled_profiles_bound (d : ℕ) (u v : ℕ → ℝ) (ε L : ℝ) (hε : 0 ≤ ε) (hL : 0 ≤ L) (hbudget : ε * 3 ^ (d + 1) ≤ 2) (hu0 : u 0 ≤ L) (hv0 : v 0 ≤ 0) (hu : ∀ n < d, u (n + 1) ≤ (1 + ε) * u n + 3 * v n) (hv : ∀ n < d, v (n + 1) ≤ ε * u n + 3 * v n) (n : ℕ) : n ≤ d → u n ≤ 2 * L ∧ v n ≤ ε * L * (3 ^ n - 1)