Sensitivity separation: separation

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/Separation.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.quantitative_separation (d : ℕ) (hd : 1 ≤ d) : ∃ (n : ℕ) (f : (Fin n → Bool) → Bool), 0 < n ∧ (f fun (x : Fin n) => false) = false ∧ (∃ (x : Fin n → Bool) (y : Fin n → Bool), f x ≠ f y) ∧ 2 ^ d / (4 * (↑d + 2) ^ 2) ≤ ↑(blockSensitivity f) / ↑(sensitivity f) ^ 2

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.unbounded_quadratic_separation (C : ℝ) (hC : 0 < C) : ∃ (n : ℕ) (f : (Fin n → Bool) → Bool), 0 < n ∧ (f fun (x : Fin n) => false) = false ∧ (∃ (x : Fin n → Bool) (y : Fin n → Bool), f x ≠ f y) ∧ C * ↑(sensitivity f) ^ 2 < ↑(blockSensitivity f)

theorem Complexity.BooleanAnalysis.Sensitivity.Internal.fixed_power_separation : ∃ (α : ℝ), 2 < α ∧ ∃ (n : ℕ → ℕ) (F : (m : ℕ) → (Fin (n m) → Bool) → Bool), (∀ (m : ℕ), 1 ≤ m → 0 < n m ∧ (F m fun (x : Fin (n m)) => false) = false ∧ (∃ (x : Fin (n m) → Bool) (y : Fin (n m) → Bool), F m x ≠ F m y) ∧ ↑(sensitivity (F m)) ^ α ≤ ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false)) ∧ Filter.Tendsto (fun (m : ℕ) => ↑(blockSensitivityAt (F m) fun (x : Fin (n m)) => false)) Filter.atTop Filter.atTop