Documentation

Complexitylib.BooleanAnalysis.PolynomialThreshold.Internal.BinomialMoments

Gotsman--Linial: BinomialMoments #

Adapted from OpenAI's formalization of Average Sensitivity of Polynomial Threshold Functions (25 September 2026), at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/GotsmanLinial/BinomialMoments.lean

The original Boolean-cube representation is used internally in this proof development; Complexitylib.BooleanAnalysis.PolynomialThreshold transports the result to the library's Fourier and influence API. Changes here adapt module visibility, namespace names, formatting, and redundant simp attributes to complexitylib.

Exact finite moments of the symmetric binomial weights. These identities provide the grading multiplicities and the variance used in the finite coupling estimate. No probabilistic assumptions or measures enter the statements.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialDenominator_pos (n : ℕ) :
0 < 2 ^ n

The normalizing denominator is positive, also when n = 0.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialDenominator_ne_zero (n : ℕ) :
2 ^ n ≠ 0
source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_range (n : ℕ) :
∑ k ∈ Finset.range (n + 1), ↑(n.choose k) = 2 ^ n

The real sum of one row of Pascal's triangle.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_succ (n : ℕ) (f : ℕ → ℝ) :
∑ k ∈ Finset.range (n + 2), ↑((n + 1).choose k) * f k = ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * f k + ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * f (k + 1)

Pascal recursion for an arbitrary real function of the binomial index.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_mul_index_range (n : ℕ) :
∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ↑k = ↑n * 2 ^ n / 2

The first raw binomial moment, with a formula valid at n = 0.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_mul_index_sq_range (n : ℕ) :
∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ↑k ^ 2 = ↑n * (↑n + 1) * 2 ^ n / 4

The second raw binomial moment, with a formula valid at n = 0.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_centered_sq_range (n : ℕ) :
∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * (↑k - ↑n / 2) ^ 2 = ↑n * 2 ^ n / 4

Exact centered second moment before dividing by 2^n.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose (n : ℕ) :
∑ k : Fin (n + 1), ↑(n.choose ↑k) = 2 ^ n

The same total mass on the grading-index type.

source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_mul_index (n : ℕ) :
∑ k : Fin (n + 1), ↑(n.choose ↑k) * ↑↑k = ↑n * 2 ^ n / 2
source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_mul_index_sq (n : ℕ) :
∑ k : Fin (n + 1), ↑(n.choose ↑k) * ↑↑k ^ 2 = ↑n * (↑n + 1) * 2 ^ n / 4
source
theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_choose_centered_sq (n : ℕ) :
∑ k : Fin (n + 1), ↑(n.choose ↑k) * (↑↑k - ↑n / 2) ^ 2 = ↑n * 2 ^ n / 4
source
noncomputable def Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialWeight (n : ℕ) (k : Fin (n + 1)) :
ℝ

The symmetric binomial probability weights, presented as a finite real function.

Equations
Instances For
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialWeight_nonneg (n : ℕ) (k : Fin (n + 1)) :
    0 ≤ binomialWeight n k
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.sum_binomialWeight (n : ℕ) :
    ∑ k : Fin (n + 1), binomialWeight n k = 1
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialWeight_mean (n : ℕ) :
    ∑ k : Fin (n + 1), binomialWeight n k * ↑↑k = ↑n / 2
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialWeight_variance (n : ℕ) :
    ∑ k : Fin (n + 1), binomialWeight n k * (↑↑k - ↑n / 2) ^ 2 = ↑n / 4
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.choose_reflect (n : ℕ) (k : Fin (n + 1)) :
    n.choose (n - ↑k) = n.choose ↑k

    The binomial coefficients are invariant under reflection about n/2.

    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.choose_rev (n : ℕ) (k : Fin (n + 1)) :
    n.choose ↑k.rev = n.choose ↑k
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialWeight_rev (n : ℕ) (k : Fin (n + 1)) :
    binomialWeight n k.rev = binomialWeight n k
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.index_rev_real (n : ℕ) (k : Fin (n + 1)) :
    ↑↑k.rev = ↑n - ↑↑k
    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialWeight_reflect (n : ℕ) (φ : ℝ → ℝ) :
    ∑ k : Fin (n + 1), binomialWeight n k * φ (↑n - ↑↑k) = ∑ k : Fin (n + 1), binomialWeight n k * φ ↑↑k

    Reflecting a binomial index preserves every real finite expectation.

    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialSigma_sq (n : ℕ) :
    (√↑n / 2) ^ 2 = ↑n / 4

    Standard deviation corresponding to the preceding finite variance identity.

    source
    theorem Complexity.BooleanAnalysis.PolynomialThreshold.Internal.binomialSigma_nonneg (n : ℕ) :
    0 ≤ √↑n / 2