Superquadratic sensitivity separation: power amplification

Amplification by iterated composition. If a Boolean function f vanishing at the all-false input has sensitivity f ≤ A and block sensitivity at least B there, where 1 < A and A ^ 2 < B, then its iterates iterateFin f m satisfy s ^ α ≤ bs for the fixed exponent α = Real.log B / Real.log A > 2, their ratio bs / s ^ 2 is at least (B / A ^ 2) ^ m, and their block sensitivity tends to infinity.

Main results

• log_exponent_gt_two: 2 < Real.log B / Real.log A when 1 < A and A ^ 2 < B.
• rpow_log_exponent: A ^ (Real.log B / Real.log A) = B for 1 < A and 0 < B.
• power_amplification: the iterates of a seed with a strict quadratic gap give a separation with a fixed exponent α > 2.

References

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

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.log_exponent_gt_two {A B : ℝ} (hA : 1 < A) (hB : A ^ 2 < B) : 2 < Real.log B / Real.log A

If 1 < A and A ^ 2 < B, then 2 < Real.log B / Real.log A.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.rpow_log_exponent {A B : ℝ} (hA : 1 < A) (hB : 0 < B) : A ^ (Real.log B / Real.log A) = B

If 1 < A and 0 < B, then A ^ (Real.log B / Real.log A) = B.

theorem Cslib.QueryComplexity.SensitivitySeparation.Internal.power_amplification {I : Type} [Fintype I] (f : (I → Bool) → Bool) (hf : (f fun (x : I) => false) = false) (A B : ℕ) (hs : sensitivity f ≤ A) (hb : B ≤ blockSensitivityAt f fun (x : I) => false) (hA : 1 < A) (hB : A ^ 2 < B) : have α := Real.log ↑B / Real.log ↑A; 2 < α ∧ (∀ (m : ℕ), 0 < Fintype.card I ^ m ∧ (iterateFin f m fun (x : Fin (Fintype.card I ^ m)) => false) = false ∧ (∃ (x : Fin (Fintype.card I ^ m) → Bool) (y : Fin (Fintype.card I ^ m) → Bool), iterateFin f m x ≠ iterateFin f m y) ∧ ↑(sensitivity (iterateFin f m)) ^ α ≤ ↑(blockSensitivityAt (iterateFin f m) fun (x : Fin (Fintype.card I ^ m)) => false) ∧ (↑B / ↑A ^ 2) ^ m ≤ ↑(blockSensitivity (iterateFin f m)) / ↑(sensitivity (iterateFin f m)) ^ 2) ∧ Filter.Tendsto (fun (m : ℕ) => ↑(blockSensitivityAt (iterateFin f m) fun (x : Fin (Fintype.card I ^ m)) => false)) Filter.atTop Filter.atTop

Let f (fun _ => false) = false, sensitivity f ≤ A and B ≤ blockSensitivityAt f (fun _ => false) with 1 < A and A ^ 2 < B, and let α = Real.log B / Real.log A. Then 2 < α; for every m, the iterate g = iterateFin f m has Fintype.card I ^ m > 0 variables, vanishes at the all-false input, is nonconstant, and satisfies sensitivity g ^ α ≤ blockSensitivityAt g (fun _ => false) and (B / A ^ 2) ^ m ≤ blockSensitivity g / sensitivity g ^ 2; and the block sensitivity of the iterates at the all-false input tends to infinity.