Sensitivity separation: power amplification #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Sensitivity/PowerAmplification.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.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