Documentation

Complexitylib.BooleanAnalysis.Sensitivity.Internal.SeparationArithmetic

Sensitivity separation: separation arithmetic #

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

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

source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.seed_ratio_identity (d : ℕ) {L M k : ℝ} (hL : L ≠ 0) (hM : M ≠ 0) :
M ^ 2 * k ^ d / (2 * L * M ^ (d + 1)) ^ 2 = (k / M ^ 2) ^ d / (4 * L ^ 2)
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.seed_ratio_lower (d : ℕ) {M : ℝ} (hM : 0 < M) :
2 ^ d / (4 * (↑d + 2) ^ 2) ≤ M ^ 2 * (2 * M ^ 2 + 1) ^ d / (2 * (↑d + 2) * M ^ (d + 1)) ^ 2
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.ratio_of_bounds {I : Type} [Fintype I] (f : (I → Bool) → Bool) (s b : ℝ) (hpos : 0 < ↑(sensitivity f)) (hs : ↑(sensitivity f) ≤ s) (hb : b ≤ ↑(blockSensitivityAt f fun (x : I) => false)) (hb0 : 0 ≤ b) :
b / s ^ 2 ≤ ↑(blockSensitivity f) / ↑(sensitivity f) ^ 2
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.quantitative_ratio_of_bounds {I : Type} [Fintype I] (f : (I → Bool) → Bool) (d M : ℕ) (hM : 0 < M) (hnc : ∃ (x : I → Bool) (y : I → Bool), f x ≠ f y) (hs : sensitivity f ≤ 2 * (d + 2) * M ^ (d + 1)) (hb : M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt f fun (x : I) => false) :
2 ^ d / (4 * (↑d + 2) ^ 2) ≤ ↑(blockSensitivity f) / ↑(sensitivity f) ^ 2
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.depth_nine_ratio :
2 ^ 9 / (4 * (9 + 2) ^ 2) = 128 / 121
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.depth_nine_ratio_gt_one :
1 < 128 / 121
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.depth_nine_seed_ratio {M : ℝ} (hM : 0 < M) :
128 / 121 ≤ M ^ 2 * (2 * M ^ 2 + 1) ^ 9 / (22 * M ^ 10) ^ 2
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.depth_nine_seed_gap (M : ℕ) (hM : 0 < M) :
1 < 22 * M ^ 10 ∧ (22 * M ^ 10) ^ 2 < M ^ 2 * (2 * M ^ 2 + 1) ^ 9
source
theorem Complexity.BooleanAnalysis.Sensitivity.Internal.quantitative_ratio_tendsto :
Filter.Tendsto (fun (d : ℕ) => 2 ^ d / (4 * (↑d + 2) ^ 2)) Filter.atTop Filter.atTop