Superquadratic sensitivity separation: separation arithmetic

Real arithmetic turning the seed bounds into ratio bounds. A nonconstant function with sensitivity at most 2 * (d + 2) * M ^ (d + 1) and block sensitivity at least M ^ 2 * (2 * M ^ 2 + 1) ^ d at the all-false input has bs / s ^ 2 at least 2 ^ d / (4 * (d + 2) ^ 2), a quantity tending to infinity with d. At depth nine this bound equals 128 / 121 > 1, giving the strict quadratic gap (22 * M ^ 10) ^ 2 < M ^ 2 * (2 * M ^ 2 + 1) ^ 9 used for amplification.

Main results

• quantitative_ratio_of_bounds: the seed bounds imply 2 ^ d / (4 * (d + 2) ^ 2) ≤ bs / s ^ 2 at the all-false input.
• depth_nine_seed_ratio: 128 / 121 ≤ M ^ 2 * (2 * M ^ 2 + 1) ^ 9 / (22 * M ^ 10) ^ 2.
• depth_nine_seed_gap: 1 < 22 * M ^ 10 and (22 * M ^ 10) ^ 2 < M ^ 2 * (2 * M ^ 2 + 1) ^ 9.
• quantitative_ratio_tendsto: 2 ^ d / (4 * (d + 2) ^ 2) tends to infinity as d → ∞.

References

• Adapted from OpenAI's formalization [OAI26b] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Combinatorics/Sensitivity/SeparationArithmetic.lean), via the complexitylib port [Sch26e] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

theorem Cslib.QueryComplexity.SensitivitySeparation.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) ≤ ↑(blockSensitivityAt f fun (x : I) => false) / ↑(sensitivity f) ^ 2

If f is nonconstant, 0 < M, sensitivity f ≤ 2 * (d + 2) * M ^ (d + 1) and M ^ 2 * (2 * M ^ 2 + 1) ^ d ≤ blockSensitivityAt f (fun _ => false), then 2 ^ d / (4 * (d + 2) ^ 2) ≤ blockSensitivityAt f (fun _ => false) / sensitivity f ^ 2.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.depth_nine_seed_ratio {M : ℝ} (hM : 0 < M) : 128 / 121 ≤ M ^ 2 * (2 * M ^ 2 + 1) ^ 9 / (22 * M ^ 10) ^ 2

For 0 < M, 128 / 121 ≤ M ^ 2 * (2 * M ^ 2 + 1) ^ 9 / (22 * M ^ 10) ^ 2.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.depth_nine_seed_gap (M : ℕ) (hM : 0 < M) : 1 < 22 * M ^ 10 ∧ (22 * M ^ 10) ^ 2 < M ^ 2 * (2 * M ^ 2 + 1) ^ 9

For 0 < M, in ℕ, 1 < 22 * M ^ 10 and (22 * M ^ 10) ^ 2 < M ^ 2 * (2 * M ^ 2 + 1) ^ 9.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.quantitative_ratio_tendsto : Filter.Tendsto (fun (d : ℕ) => 2 ^ d / (4 * (↑d + 2) ^ 2)) Filter.atTop Filter.atTop

The ratio bound 2 ^ d / (4 * (d + 2) ^ 2) tends to infinity as d → ∞.