Prove2Me

Extract the universal average-sensitivity coefficient 3.762 from the binomial moment bound

Proved
AverageSensitivity.extract_constant

by Yuxuan Xu · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

average-sensitivity-3762boolean-functionsinequalities

For every pair of positive integers n,d and every real A satisfying

A≤n,A≤8dbn+2d2,A\le n,\qquad A\le8d b_n+2d^2,

where b_n is the exact mean absolute deviation of Bin(n,1/2) as defined by AverageSensitivity.mad, prove

A≤1881500dn.A\le\frac{1881}{500}d\sqrt n.

No condition d<=n is needed. The statement is a scalar extraction theorem, independent of the polynomial-threshold construction. Its role is to turn the refined dimension-degree estimate into the universal coefficient 3.762.

Preamble
import Mathlib
import Definitions.Def_AverageSensitivity_Constants3762
open scoped BigOperators
open AverageSensitivity
Formal statement
theorem AverageSensitivity.extract_constant (n d : ℕ) (hn : 1 ≤ n) (hd : 1 ≤ d)
    (A : ℝ) (htrivial : A ≤ (n:ℝ))
    (hrefined : A ≤ 8*(d:ℝ)*mad n+2*(d:ℝ)^2) :
    A ≤ (1881/500:ℝ)*(d:ℝ)*Real.sqrt (n:ℝ) := by sorry
Source
https://github.com/Anchen0823/average-sensitivity-lean/blob/b2e634415548e050c115f6f12732d8b6b4a5d27f/AverageSensitivity/ConstantExtraction.lean
Human review

  • Endorsed by Shuze Chen · Oct 16, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Yuxuan Xu · Oct 16, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph