Analysis of Boolean Functions in Lean

5.3. The Fourier coefficients of Majority🔗

Lemma5.3.1
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Lemma 2.1.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 5.3.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-3supportfidelity-exact

Symmetric Fourier coefficients (from Exercise 1.30). Let f:\{-1,1\}^n\to\mathbb R be symmetric. If S,T\subseteq[n] satisfy |S|=|T|, then \widehat f(S)=\widehat f(T). Thus the Fourier coefficient of a symmetric function at a set S depends only on |S|.

Lean code for Lemma5.3.1●1 theorem
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_eq_of_card_eq_of_isSymmetric {n : ℕ}
  {f : FABL.SignCube n → ℝ} (hf : FABL.IsSymmetric f)
  {S T : Finset (Fin n)} (hcard : S.card = T.card) :
  FABL.fourierCoeff f S = FABL.fourierCoeff f T
    theorem FABL.fourierCoeff_eq_of_card_eq_of_isSymmetric
  {n : ℕ} {f : FABL.SignCube n → ℝ}
  (hf : FABL.IsSymmetric f)
  {S T : Finset (Fin n)}
  (hcard : S.card = T.card) :
  FABL.fourierCoeff f S =
    FABL.fourierCoeff f T
    Exercise 1.30: Fourier coefficients of a symmetric function depend only on
the cardinality of their index set.
Lemma5.3.2
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Theorem 1.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact-used-part

Exercise 1.8(c), odd-function consequence. If f:\{-1,1\}^n\to\mathbb R is odd, so that f(-x)=-f(x) for every x, then every even-cardinality Fourier coefficient vanishes: |S|\text{ even}\quad\Longrightarrow\quad\widehat f(S)=0. This is the exact part of Exercise 1.8 used by Theorem 5.19.

Lean code for Lemma5.3.2●1 theorem
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_eq_zero_of_odd_of_even_card {n : ℕ}
  {f : FABL.SignCube n → ℝ} (hf : Function.Odd f) (S : Finset (Fin n))
  (hS : Even S.card) : FABL.fourierCoeff f S = 0
    theorem FABL.fourierCoeff_eq_zero_of_odd_of_even_card
  {n : ℕ} {f : FABL.SignCube n → ℝ}
  (hf : Function.Odd f)
  (S : Finset (Fin n))
  (hS : Even S.card) :
  FABL.fourierCoeff f S = 0
    Exercise 1.8(c): an odd function has zero Fourier coefficient on every
even-cardinality set.
Lemma5.3.3
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

Exercise 5.18 (the power series for arcsine).

(a) The generalized Binomial Theorem gives, for |z|<1, (1-z^2)^{-1/2} =\sum_{j=0}^{\infty}\binom{2j}{j}\frac{z^{2j}}{2^{2j}}.

(b) Integrating term by term gives, for |z|<1, \arcsin z =\sum_{j=0}^{\infty} \frac1{2j+1}\binom{2j}{j}\frac{z^{2j+1}}{2^{2j}} =\sum_{\substack{k\ge1\\k\ \mathrm{odd}}} \frac{2}{k2^k}\binom{k-1}{(k-1)/2}z^k. \tag{5.9}

(c) The arcsine series in (b) also holds for z=\pm1; it converges there to \arcsin(1)=\pi/2 and \arcsin(-1)=-\pi/2.

Lean code for Lemma5.3.3●6 declarations
  • defdefined in FABL/Chapter05/MajorityLimits.lean
    complete
    def FABL.arcsinSeriesCoefficient (j : ℕ) : ℝ
    def FABL.arcsinSeriesCoefficient (j : ℕ) : ℝ
    The coefficient of `z^(2j + 1)` in the central-binomial series for `Real.arcsin`.
  • defdefined in FABL/Chapter05/MajorityLimits.lean
    complete
    def FABL.arcsinOddPowerCoefficient (k : ℕ) : ℝ
    def FABL.arcsinOddPowerCoefficient (k : ℕ) : ℝ
    The coefficient of `z^k` in the odd-power presentation of the arcsine series.
  • theoremdefined in FABL/Chapter05/MajorityLimits.lean
    complete
    theorem FABL.arcsinOddPowerCoefficient_two_mul_add_one (j : ℕ) :
  FABL.arcsinOddPowerCoefficient (2 * j + 1) =
    FABL.arcsinSeriesCoefficient j
    theorem FABL.arcsinOddPowerCoefficient_two_mul_add_one
  (j : ℕ) :
  FABL.arcsinOddPowerCoefficient
      (2 * j + 1) =
    FABL.arcsinSeriesCoefficient j
  • theoremdefined in FABL/Chapter05/MajorityLimits.lean
    complete
    theorem FABL.exercise5_18a {z : ℝ} (hz : |z| < 1) :
  HasSum (fun j => ↑((2 * j).choose j) * z ^ (2 * j) / 2 ^ (2 * j))
    ((1 - z ^ 2) ^ (-1 / 2))
    theorem FABL.exercise5_18a {z : ℝ}
  (hz : |z| < 1) :
  HasSum
    (fun j =>
      ↑((2 * j).choose j) * z ^ (2 * j) /
        2 ^ (2 * j))
    ((1 - z ^ 2) ^ (-1 / 2))
    O'Donnell, Exercise 5.18(a): the generalized-binomial expansion of
`(1 - z²)⁻¹ᐟ²` on the open unit interval.
  • theoremdefined in FABL/Chapter05/MajorityLimits.lean
    complete
    theorem FABL.exercise5_18_arcsinSeries (z : ℝ) (hz : z ∈ Set.Icc (-1) 1) :
  HasSum (fun j => FABL.arcsinSeriesCoefficient j * z ^ (2 * j + 1))
      (Real.arcsin z) ∧
    HasSum (fun k => FABL.arcsinOddPowerCoefficient k * z ^ k)
      (Real.arcsin z)
    theorem FABL.exercise5_18_arcsinSeries (z : ℝ)
  (hz : z ∈ Set.Icc (-1) 1) :
  HasSum
      (fun j =>
        FABL.arcsinSeriesCoefficient j *
          z ^ (2 * j + 1))
      (Real.arcsin z) ∧
    HasSum
      (fun k =>
        FABL.arcsinOddPowerCoefficient k *
          z ^ k)
      (Real.arcsin z)
    O'Donnell, Exercise 5.18(b)--(c): both odd-power presentations of the
arcsine series converge on the closed unit interval, including its endpoints.
  • theoremdefined in FABL/Chapter05/MajorityLimits.lean
    complete
    theorem FABL.exercise5_18 :
  (∀ (z : ℝ),
      |z| < 1 →
        HasSum
          (fun j => ↑((2 * j).choose j) * z ^ (2 * j) / 2 ^ (2 * j))
          ((1 - z ^ 2) ^ (-1 / 2))) ∧
    (∀ z ∈ Set.Icc (-1) 1,
        HasSum
            (fun j => FABL.arcsinSeriesCoefficient j * z ^ (2 * j + 1))
            (Real.arcsin z) ∧
          HasSum (fun k => FABL.arcsinOddPowerCoefficient k * z ^ k)
            (Real.arcsin z)) ∧
      (HasSum
            (fun j => FABL.arcsinSeriesCoefficient j * 1 ^ (2 * j + 1))
            (Real.pi / 2) ∧
          HasSum (fun k => FABL.arcsinOddPowerCoefficient k * 1 ^ k)
            (Real.pi / 2)) ∧
        HasSum
            (fun j =>
              FABL.arcsinSeriesCoefficient j * (-1) ^ (2 * j + 1))
            (-(Real.pi / 2)) ∧
          HasSum (fun k => FABL.arcsinOddPowerCoefficient k * (-1) ^ k)
            (-(Real.pi / 2))
    theorem FABL.exercise5_18 :
  (∀ (z : ℝ),
      |z| < 1 →
        HasSum
          (fun j =>
            ↑((2 * j).choose j) *
                z ^ (2 * j) /
              2 ^ (2 * j))
          ((1 - z ^ 2) ^ (-1 / 2))) ∧
    (∀ z ∈ Set.Icc (-1) 1,
        HasSum
            (fun j =>
              FABL.arcsinSeriesCoefficient
                  j *
                z ^ (2 * j + 1))
            (Real.arcsin z) ∧
          HasSum
            (fun k =>
              FABL.arcsinOddPowerCoefficient
                  k *
                z ^ k)
            (Real.arcsin z)) ∧
      (HasSum
            (fun j =>
              FABL.arcsinSeriesCoefficient
                  j *
                1 ^ (2 * j + 1))
            (Real.pi / 2) ∧
          HasSum
            (fun k =>
              FABL.arcsinOddPowerCoefficient
                  k *
                1 ^ k)
            (Real.pi / 2)) ∧
        HasSum
            (fun j =>
              FABL.arcsinSeriesCoefficient
                  j *
                (-1) ^ (2 * j + 1))
            (-(Real.pi / 2)) ∧
          HasSum
            (fun k =>
              FABL.arcsinOddPowerCoefficient
                  k *
                (-1) ^ k)
            (-(Real.pi / 2))
    O'Donnell, Exercise 5.18: the derivative series on `(-1, 1)`, both
integrated odd-power series on `[-1, 1]`, and their exact endpoint sums.
Definition5.3.4
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.4.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 5.3.13
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-3supportfidelity-exact

Limiting majority Fourier weights. For k\in\mathbb N, write \mathbf W^k(\operatorname{Maj}) :=[\rho^k]\left(\frac2\pi\arcsin\rho\right) = \begin{cases} \displaystyle \frac{4}{\pi k2^k}\binom{k-1}{(k-1)/2}, & k\text{ odd},\\[6pt] 0,& k\text{ even}. \end{cases} \tag{5.10} Here [\rho^k]F(\rho) denotes the coefficient of \rho^k in the power series F. Also write \mathbf W^{>k}(\operatorname{Maj}) =\sum_{j>k}\mathbf W^j(\operatorname{Maj}).

Lean code for Definition5.3.4●5 declarations
  • defdefined in FABL/Chapter05/LimitingMajorityWeights.lean
    complete
    def FABL.limitingMajorityFourierWeight (k : ℕ) : ℝ
    def FABL.limitingMajorityFourierWeight
  (k : ℕ) : ℝ
    O'Donnell, Equation (5.10): the degree-`k` coefficient of
`(2 / π) * arcsin ρ`.
  • theoremdefined in FABL/Chapter05/LimitingMajorityWeights.lean
    complete
    theorem FABL.limitingMajorityFourierWeight_eq (k : ℕ) :
  FABL.limitingMajorityFourierWeight k =
    if Odd k then
      4 / (Real.pi * ↑k * 2 ^ k) * ↑((k - 1).choose ((k - 1) / 2))
    else 0
    theorem FABL.limitingMajorityFourierWeight_eq
  (k : ℕ) :
  FABL.limitingMajorityFourierWeight k =
    if Odd k then
      4 / (Real.pi * ↑k * 2 ^ k) *
        ↑((k - 1).choose ((k - 1) / 2))
    else 0
    The explicit odd/even formula in O'Donnell, Equation (5.10).
  • theoremdefined in FABL/Chapter05/LimitingMajorityWeights.lean
    complete
    theorem FABL.limitingMajorityFourierWeight_hasSum_one :
  HasSum FABL.limitingMajorityFourierWeight 1
    theorem FABL.limitingMajorityFourierWeight_hasSum_one :
  HasSum
    FABL.limitingMajorityFourierWeight 1
    The limiting majority Fourier weights sum to `1`.
  • defdefined in FABL/Chapter05/LimitingMajorityWeights.lean
    complete
    def FABL.limitingMajorityFourierWeightAbove (k : ℕ) : ℝ
    def FABL.limitingMajorityFourierWeightAbove
  (k : ℕ) : ℝ
    O'Donnell's `𝐖^{>k}(Maj)`, expressed as the convergent sum over degrees
strictly greater than `k`.
  • theoremdefined in FABL/Chapter05/LimitingMajorityWeights.lean
    complete
    theorem FABL.limitingMajorityFourierWeightAbove_summable (k : ℕ) :
  Summable fun j => FABL.limitingMajorityFourierWeight ↑j
    theorem FABL.limitingMajorityFourierWeightAbove_summable
  (k : ℕ) :
  Summable fun j =>
    FABL.limitingMajorityFourierWeight ↑j
    The series defining `limitingMajorityFourierWeightAbove` is summable.
Lemma5.3.5
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 6
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

The middle-layer calculation, Equations (5.12)--(5.14). For m\in\mathbb N, let \operatorname{Half}_{2m}:\{-1,1\}^{2m}\to\{0,1\} be the indicator of the strings having exactly m coordinates equal to -1. Identifying a derivative that ignores its last coordinate with a function on the remaining coordinates, D_{2m+1}\operatorname{Maj}_{2m+1}=\operatorname{Half}_{2m}. For every 0\le j\le m and every T\subseteq[2m] with |T|=2j, \widehat{\operatorname{Half}_{2m}}(T) =(-1)^j \frac{\binom mj}{\binom{2m}{2j}} \frac1{2^{2m}}\binom{2m}{m}. \tag{5.12} For every \rho\in[-1,1], \begin{aligned} T_\rho\operatorname{Half}_{2m}(1,\ldots,1) &=\binom{2m}{m} \left(\frac12+\frac\rho2\right)^m \left(\frac12-\frac\rho2\right)^m\\ &=\frac1{2^{2m}}\binom{2m}{m}(1-\rho^2)^m, \end{aligned} \tag{5.13} whereas symmetry and the Fourier formula for T_\rho give T_\rho\operatorname{Half}_{2m}(1,\ldots,1) =\sum_{U\subseteq[2m]} \widehat{\operatorname{Half}_{2m}}(U)\rho^{|U|} =\sum_{i=0}^{2m}\binom{2m}{i} \widehat{\operatorname{Half}_{2m}}(T_i)\rho^i, \tag{5.14} where T_i is any i-element subset of [2m]. Comparing coefficients in (5.13) and (5.14) yields (5.12).

Lean code for Lemma5.3.5●9 declarations
  • defdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    def FABL.middleLayerIndicator (m : ℕ) (x : FABL.SignCube (2 * m)) : ℝ
    def FABL.middleLayerIndicator (m : ℕ)
  (x : FABL.SignCube (2 * m)) : ℝ
    The real-valued indicator of the middle Hamming layer in the even-dimensional sign cube.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.middleLayerIndicator_eq_one_iff_negative_count (m : ℕ)
  (x : FABL.SignCube (2 * m)) :
  FABL.middleLayerIndicator m x = 1 ↔ {i | x i = -1}.card = m
    theorem FABL.middleLayerIndicator_eq_one_iff_negative_count
  (m : ℕ) (x : FABL.SignCube (2 * m)) :
  FABL.middleLayerIndicator m x = 1 ↔
    {i | x i = -1}.card = m
    On a `2m`-dimensional sign cube, the chosen positive-coordinate representation
is exactly the book's indicator of strings with `m` negative coordinates.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.discreteDerivative_majority_odd_last_eq_middleLayerIndicator
  (m : ℕ) (x : FABL.SignCube (2 * m)) :
  (FABL.discreteDerivative (Fin.last (2 * m)))
      (FABL.majority (2 * m + 1)).toReal (Fin.snoc x 1) =
    FABL.middleLayerIndicator m x
    theorem FABL.discreteDerivative_majority_odd_last_eq_middleLayerIndicator
  (m : ℕ) (x : FABL.SignCube (2 * m)) :
  (FABL.discreteDerivative
        (Fin.last (2 * m)))
      (FABL.majority (2 * m + 1)).toReal
      (Fin.snoc x 1) =
    FABL.middleLayerIndicator m x
    The first identity in O'Donnell's middle-layer calculation: the last discrete derivative
of odd-arity majority is the indicator of the middle layer on the remaining coordinates.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.middleLayerIndicator_isSymmetric (m : ℕ) :
  FABL.IsSymmetric (FABL.middleLayerIndicator m)
    theorem FABL.middleLayerIndicator_isSymmetric
  (m : ℕ) :
  FABL.IsSymmetric
    (FABL.middleLayerIndicator m)
    The middle-layer indicator is invariant under every coordinate permutation.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq_product (m : ℕ)
  (ρ : ℝ) (hρ : ρ ∈ Set.Icc (-1) 1) :
  ((FABL.noiseOperator ρ) (FABL.middleLayerIndicator m) fun x => 1) =
    ↑((2 * m).choose m) * ((1 + ρ) / 2) ^ m * ((1 - ρ) / 2) ^ m
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq_product
  (m : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) :
  ((FABL.noiseOperator ρ)
      (FABL.middleLayerIndicator m)
      fun x => 1) =
    ↑((2 * m).choose m) *
        ((1 + ρ) / 2) ^ m *
      ((1 - ρ) / 2) ^ m
    Equation (5.13), first line: the noise operator at the all-ones input is the
middle-layer probability under independent coordinate noise.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq (m : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) :
  ((FABL.noiseOperator ρ) (FABL.middleLayerIndicator m) fun x => 1) =
    ↑((2 * m).choose m) / 2 ^ (2 * m) * (1 - ρ ^ 2) ^ m
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq
  (m : ℕ) (ρ : ℝ)
  (hρ : ρ ∈ Set.Icc (-1) 1) :
  ((FABL.noiseOperator ρ)
      (FABL.middleLayerIndicator m)
      fun x => 1) =
    ↑((2 * m).choose m) / 2 ^ (2 * m) *
      (1 - ρ ^ 2) ^ m
    Equation (5.13), second line: the middle-layer noise probability in its
polynomial form.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq_fourierSum (m : ℕ)
  (ρ : ℝ) :
  ((FABL.noiseOperator ρ) (FABL.middleLayerIndicator m) fun x => 1) =
    ∑ U, FABL.fourierCoeff (FABL.middleLayerIndicator m) U * ρ ^ U.card
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq_fourierSum
  (m : ℕ) (ρ : ℝ) :
  ((FABL.noiseOperator ρ)
      (FABL.middleLayerIndicator m)
      fun x => 1) =
    ∑ U,
      FABL.fourierCoeff
          (FABL.middleLayerIndicator m)
          U *
        ρ ^ U.card
    Equation (5.14), first equality: evaluation at the all-ones input turns every
Walsh character into one.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq_groupedFourierSum
  (m : ℕ) (ρ : ℝ) (T : ℕ → Finset (Fin (2 * m)))
  (hT : ∀ i ≤ 2 * m, (T i).card = i) :
  ((FABL.noiseOperator ρ) (FABL.middleLayerIndicator m) fun x => 1) =
    ∑ i ∈ Finset.range (2 * m + 1),
      ↑((2 * m).choose i) *
          FABL.fourierCoeff (FABL.middleLayerIndicator m) (T i) *
        ρ ^ i
    theorem FABL.noiseOperator_middleLayerIndicator_allOne_eq_groupedFourierSum
  (m : ℕ) (ρ : ℝ)
  (T : ℕ → Finset (Fin (2 * m)))
  (hT : ∀ i ≤ 2 * m, (T i).card = i) :
  ((FABL.noiseOperator ρ)
      (FABL.middleLayerIndicator m)
      fun x => 1) =
    ∑ i ∈ Finset.range (2 * m + 1),
      ↑((2 * m).choose i) *
          FABL.fourierCoeff
            (FABL.middleLayerIndicator m)
            (T i) *
        ρ ^ i
    Equation (5.14), grouped by cardinality: any representative of each Fourier
level may be used because the middle-layer indicator is symmetric.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_middleLayerIndicator (m j : ℕ) (hj : j ≤ m)
  (T : Finset (Fin (2 * m))) (hT : T.card = 2 * j) :
  FABL.fourierCoeff (FABL.middleLayerIndicator m) T =
    (-1) ^ j * ↑(m.choose j) / ↑((2 * m).choose (2 * j)) *
        (1 / 2 ^ (2 * m)) *
      ↑((2 * m).choose m)
    theorem FABL.fourierCoeff_middleLayerIndicator
  (m j : ℕ) (hj : j ≤ m)
  (T : Finset (Fin (2 * m)))
  (hT : T.card = 2 * j) :
  FABL.fourierCoeff
      (FABL.middleLayerIndicator m) T =
    (-1) ^ j * ↑(m.choose j) /
          ↑((2 * m).choose (2 * j)) *
        (1 / 2 ^ (2 * m)) *
      ↑((2 * m).choose m)
    Equation (5.12): the exact Fourier coefficient of the middle Hamming layer
on an even-dimensional sign cube.
Theorem5.3.6
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Lemma 5.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 5
Reverse dependency previews
Preview
Lemma 5.3.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-3fidelity-exact

Theorem 5.19. Let n be odd and let S\subseteq[n]. If |S| is even, then \widehat{\operatorname{Maj}_n}(S)=0. If |S|=k is odd, then \widehat{\operatorname{Maj}_n}(S) =(-1)^{(k-1)/2} \frac{\binom{(n-1)/2}{(k-1)/2}}{\binom{n-1}{k-1}} \frac2{2^n}\binom{n-1}{(n-1)/2}. Equivalently, when n=2m+1 and k=2j+1, \widehat{\operatorname{Maj}_{2m+1}}(S) =(-1)^j \frac{\binom mj}{\binom{2m}{2j}} \frac1{2^{2m}}\binom{2m}{m}.

Lean code for Theorem5.3.6●4 theorems
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_majority_odd_insert_last (m : ℕ)
  (T : Finset (Fin (2 * m))) :
  FABL.fourierCoeff (FABL.majority (2 * m + 1)).toReal
      (insert (Fin.last (2 * m)) (Finset.map Fin.castSuccEmb T)) =
    FABL.fourierCoeff (FABL.middleLayerIndicator m) T
    theorem FABL.fourierCoeff_majority_odd_insert_last
  (m : ℕ) (T : Finset (Fin (2 * m))) :
  FABL.fourierCoeff
      (FABL.majority (2 * m + 1)).toReal
      (insert (Fin.last (2 * m))
        (Finset.map Fin.castSuccEmb T)) =
    FABL.fourierCoeff
      (FABL.middleLayerIndicator m) T
    The derivative step in Theorem 5.19: adjoining the last coordinate to a
Fourier set of the middle layer gives the corresponding majority coefficient.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_majority_eq_zero_of_odd_arity_of_even_card {n : ℕ}
  (hn : Odd n) (S : Finset (Fin n)) (hS : Even S.card) :
  FABL.fourierCoeff (FABL.majority n).toReal S = 0
    theorem FABL.fourierCoeff_majority_eq_zero_of_odd_arity_of_even_card
  {n : ℕ} (hn : Odd n)
  (S : Finset (Fin n))
  (hS : Even S.card) :
  FABL.fourierCoeff
      (FABL.majority n).toReal S =
    0
    Theorem 5.19, even-cardinality case.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_majority_two_mul_add_one (m j : ℕ)
  (S : Finset (Fin (2 * m + 1))) (hS : S.card = 2 * j + 1) :
  FABL.fourierCoeff (FABL.majority (2 * m + 1)).toReal S =
    (-1) ^ j * ↑(m.choose j) / ↑((2 * m).choose (2 * j)) *
        (1 / 2 ^ (2 * m)) *
      ↑((2 * m).choose m)
    theorem FABL.fourierCoeff_majority_two_mul_add_one
  (m j : ℕ) (S : Finset (Fin (2 * m + 1)))
  (hS : S.card = 2 * j + 1) :
  FABL.fourierCoeff
      (FABL.majority (2 * m + 1)).toReal
      S =
    (-1) ^ j * ↑(m.choose j) /
          ↑((2 * m).choose (2 * j)) *
        (1 / 2 ^ (2 * m)) *
      ↑((2 * m).choose m)
    Theorem 5.19 in the equivalent parametrization `n = 2m+1`,
`|S| = 2j+1`.
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.fourierCoeff_majority_of_odd_arity_of_card_eq_odd {n k : ℕ}
  (hn : Odd n) (hk : Odd k) (S : Finset (Fin n)) (hS : S.card = k) :
  FABL.fourierCoeff (FABL.majority n).toReal S =
    (-1) ^ ((k - 1) / 2) * ↑(((n - 1) / 2).choose ((k - 1) / 2)) /
          ↑((n - 1).choose (k - 1)) *
        (2 / 2 ^ n) *
      ↑((n - 1).choose ((n - 1) / 2))
    theorem FABL.fourierCoeff_majority_of_odd_arity_of_card_eq_odd
  {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (S : Finset (Fin n)) (hS : S.card = k) :
  FABL.fourierCoeff
      (FABL.majority n).toReal S =
    (-1) ^ ((k - 1) / 2) *
            ↑(((n - 1) / 2).choose
                ((k - 1) / 2)) /
          ↑((n - 1).choose (k - 1)) *
        (2 / 2 ^ n) *
      ↑((n - 1).choose ((n - 1) / 2))
    Theorem 5.19, odd-cardinality case, in the book's `n,k` notation.
Lemma5.3.7
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

Exercise 5.20. Prove that for odd n and S,T\subseteq[n] satisfying |S|+|T|=n+1, \widehat{\operatorname{Maj}_n}(S) =(-1)^{(n-1)/2}\widehat{\operatorname{Maj}_n}(T), and deduce that, for 1\le k\le n, \mathbf W^{n-k+1}[\operatorname{Maj}_n] =\frac{k}{n-k+1}\mathbf W^k[\operatorname{Maj}_n].

Lean code for Lemma5.3.7●1 theorem
  • theoremdefined in FABL/Chapter05/MajorityComplementaryWeights.lean
    complete
    theorem FABL.fourierCoeff_majority_complementary {n : ℕ} (hn : Odd n)
  (S T : Finset (Fin n)) (hcard : S.card + T.card = n + 1) :
  FABL.fourierCoeff (FABL.majority n).toReal S =
    (-1) ^ ((n - 1) / 2) * FABL.fourierCoeff (FABL.majority n).toReal T
    theorem FABL.fourierCoeff_majority_complementary
  {n : ℕ} (hn : Odd n)
  (S T : Finset (Fin n))
  (hcard : S.card + T.card = n + 1) :
  FABL.fourierCoeff
      (FABL.majority n).toReal S =
    (-1) ^ ((n - 1) / 2) *
      FABL.fourierCoeff
        (FABL.majority n).toReal T
    Exercise 5.20 and Corollary 5.20: Fourier coefficients of odd-arity majority
at complementary cardinalities agree up to the middle-level sign.
Corollary5.3.8
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.3.14
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-3fidelity-exact

Corollary 5.20. Let n be odd. Whenever S,T\subseteq[n] satisfy |S|+|T|=n+1, \widehat{\operatorname{Maj}_n}(S) =(-1)^{(n-1)/2}\widehat{\operatorname{Maj}_n}(T). Hence, for every 1\le k\le n, \mathbf W^{n-k+1}[\operatorname{Maj}_n] =\frac{k}{n-k+1}\mathbf W^k[\operatorname{Maj}_n].

Lean code for Corollary5.3.8●1 theorem
  • theoremdefined in FABL/Chapter05/MajorityComplementaryWeights.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_complementary {n : ℕ} (hn : Odd n)
  (k : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) :
  FABL.fourierWeightAtLevel (n - k + 1) (FABL.majority n).toReal =
    ↑k / ↑(n - k + 1) *
      FABL.fourierWeightAtLevel k (FABL.majority n).toReal
    theorem FABL.fourierWeightAtLevel_majority_complementary
  {n : ℕ} (hn : Odd n) (k : ℕ)
  (hk : 1 ≤ k) (hkn : k ≤ n) :
  FABL.fourierWeightAtLevel (n - k + 1)
      (FABL.majority n).toReal =
    ↑k / ↑(n - k + 1) *
      FABL.fourierWeightAtLevel k
        (FABL.majority n).toReal
    Exercise 5.20 and Corollary 5.20: complementary Fourier levels of odd-arity
majority differ by the ratio of their cardinalities.
Lemma5.3.9
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

Exercise 5.22. Fix an odd positive integer k. Prove that \mathbf W^k[\operatorname{Maj}_n] is a strictly decreasing function of n as n ranges through the odd integers with n\ge k.

Lean code for Lemma5.3.9●4 theorems
  • theoremdefined in FABL/Chapter05/MajorityWeightMonotonicity.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_eq_choose_mul (n k : ℕ)
  (S : Finset (Fin n)) (hS : S.card = k) :
  FABL.fourierWeightAtLevel k (FABL.majority n).toReal =
    ↑(n.choose k) * FABL.fourierWeight (FABL.majority n).toReal S
    theorem FABL.fourierWeightAtLevel_majority_eq_choose_mul
  (n k : ℕ) (S : Finset (Fin n))
  (hS : S.card = k) :
  FABL.fourierWeightAtLevel k
      (FABL.majority n).toReal =
    ↑(n.choose k) *
      FABL.fourierWeight
        (FABL.majority n).toReal S
    A symmetric level of majority consists of `n.choose k` equal Fourier weights.
  • theoremdefined in FABL/Chapter05/MajorityWeightMonotonicity.lean
    complete
    theorem FABL.fourierCoeff_majority_next_odd_eq (m j : ℕ) (hj : j ≤ m)
  (S : Finset (Fin (2 * m + 1))) (hS : S.card = 2 * j + 1)
  (T : Finset (Fin (2 * (m + 1) + 1))) (hT : T.card = 2 * j + 1) :
  FABL.fourierCoeff (FABL.majority (2 * (m + 1) + 1)).toReal T =
    ↑(2 * (m - j) + 1) / ↑(2 * (m + 1)) *
      FABL.fourierCoeff (FABL.majority (2 * m + 1)).toReal S
    theorem FABL.fourierCoeff_majority_next_odd_eq
  (m j : ℕ) (hj : j ≤ m)
  (S : Finset (Fin (2 * m + 1)))
  (hS : S.card = 2 * j + 1)
  (T : Finset (Fin (2 * (m + 1) + 1)))
  (hT : T.card = 2 * j + 1) :
  FABL.fourierCoeff
      (FABL.majority
          (2 * (m + 1) + 1)).toReal
      T =
    ↑(2 * (m - j) + 1) / ↑(2 * (m + 1)) *
      FABL.fourierCoeff
        (FABL.majority (2 * m + 1)).toReal
        S
    Theorem 5.19 implies an exact ratio between corresponding fixed-level
coefficients in two consecutive odd dimensions.
  • theoremdefined in FABL/Chapter05/MajorityWeightMonotonicity.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_next_odd_eq (m j : ℕ) (hj : j ≤ m) :
  FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * (m + 1) + 1)).toReal =
    ↑(2 * m + 3) * ↑(2 * (m - j) + 1) /
        (↑(2 * m + 2) * ↑(2 * (m - j) + 2)) *
      FABL.fourierWeightAtLevel (2 * j + 1)
        (FABL.majority (2 * m + 1)).toReal
    theorem FABL.fourierWeightAtLevel_majority_next_odd_eq
  (m j : ℕ) (hj : j ≤ m) :
  FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority
          (2 * (m + 1) + 1)).toReal =
    ↑(2 * m + 3) * ↑(2 * (m - j) + 1) /
        (↑(2 * m + 2) *
          ↑(2 * (m - j) + 2)) *
      FABL.fourierWeightAtLevel
        (2 * j + 1)
        (FABL.majority (2 * m + 1)).toReal
    Exercise 5.22, exact adjacent-step identity for a fixed positive odd level.
  • theoremdefined in FABL/Chapter05/MajorityWeightMonotonicity.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_next_odd_lt (m j : ℕ) (hj : j ≤ m) :
  FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * (m + 1) + 1)).toReal <
    FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * m + 1)).toReal
    theorem FABL.fourierWeightAtLevel_majority_next_odd_lt
  (m j : ℕ) (hj : j ≤ m) :
  FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority
          (2 * (m + 1) + 1)).toReal <
    FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * m + 1)).toReal
    Exercise 5.22: increasing odd arity by two strictly decreases every
available fixed positive odd Fourier level.
Corollary5.3.10
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 5.3.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-3fidelity-exact

Corollary 5.21. For every fixed odd positive integer k, \mathbf W^k[\operatorname{Maj}_n] is a strictly decreasing function of n as n ranges through the odd integers with n\ge k.

Lean code for Corollary5.3.10●2 theorems
  • theoremdefined in FABL/Chapter05/MajorityWeightMonotonicity.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_odd_sequence_strictAnti (j : ℕ) :
  StrictAnti fun r =>
    FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * (j + r) + 1)).toReal
    theorem FABL.fourierWeightAtLevel_majority_odd_sequence_strictAnti
  (j : ℕ) :
  StrictAnti fun r =>
    FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority
          (2 * (j + r) + 1)).toReal
    Corollary 5.21 in its canonical sequence form: for fixed level `2j+1`,
the Fourier weight is strictly decreasing along all odd arities at least `2j+1`.
  • theoremdefined in FABL/Chapter05/MajorityWeightMonotonicity.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_strict_decreasing {k n₁ n₂ : ℕ}
  (hkPos : 0 < k) (hkOdd : Odd k) (hn₁Odd : Odd n₁) (hn₂Odd : Odd n₂)
  (hkn₁ : k ≤ n₁) (hn₁n₂ : n₁ < n₂) :
  FABL.fourierWeightAtLevel k (FABL.majority n₂).toReal <
    FABL.fourierWeightAtLevel k (FABL.majority n₁).toReal
    theorem FABL.fourierWeightAtLevel_majority_strict_decreasing
  {k n₁ n₂ : ℕ} (hkPos : 0 < k)
  (hkOdd : Odd k) (hn₁Odd : Odd n₁)
  (hn₂Odd : Odd n₂) (hkn₁ : k ≤ n₁)
  (hn₁n₂ : n₁ < n₂) :
  FABL.fourierWeightAtLevel k
      (FABL.majority n₂).toReal <
    FABL.fourierWeightAtLevel k
      (FABL.majority n₁).toReal
    Corollary 5.21 in the book's `k,n` notation.
Lemma5.3.11
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 2.4.6
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

Exercise 5.23. Prove Theorem 5.18: for every \rho\in[0,1), \operatorname{Stab}_\rho[\operatorname{Maj}_n] decreases as n ranges through the positive odd integers, and \frac2\pi\arcsin\rho \le \operatorname{Stab}_\rho[\operatorname{Maj}_n] \le \frac2\pi\arcsin\rho +O_\rho\left(\frac1{\sqrt{1-\rho^2}\sqrt n}\right). Use Corollary 5.21 for the monotonicity.

Lean code for Lemma5.3.11●6 theorems
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.noiseStability_majority_next_odd_le (m : ℕ) {ρ : ℝ}
  (hρ : ρ ∈ Set.Ico 0 1) :
  FABL.noiseStability ρ ⋯ (FABL.majority (2 * (m + 1) + 1)).toReal ≤
    FABL.noiseStability ρ ⋯ (FABL.majority (2 * m + 1)).toReal
    theorem FABL.noiseStability_majority_next_odd_le
  (m : ℕ) {ρ : ℝ} (hρ : ρ ∈ Set.Ico 0 1) :
  FABL.noiseStability ρ ⋯
      (FABL.majority
          (2 * (m + 1) + 1)).toReal ≤
    FABL.noiseStability ρ ⋯
      (FABL.majority (2 * m + 1)).toReal
    Exercise 5.23, adjacent-step form: odd-majority noise stability is nonincreasing
for every nonnegative correlation below one.
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.noiseStability_majority_next_odd_lt (m : ℕ) {ρ : ℝ}
  (hρ : ρ ∈ Set.Ioo 0 1) :
  FABL.noiseStability ρ ⋯ (FABL.majority (2 * (m + 1) + 1)).toReal <
    FABL.noiseStability ρ ⋯ (FABL.majority (2 * m + 1)).toReal
    theorem FABL.noiseStability_majority_next_odd_lt
  (m : ℕ) {ρ : ℝ} (hρ : ρ ∈ Set.Ioo 0 1) :
  FABL.noiseStability ρ ⋯
      (FABL.majority
          (2 * (m + 1) + 1)).toReal <
    FABL.noiseStability ρ ⋯
      (FABL.majority (2 * m + 1)).toReal
    Exercise 5.23, strict adjacent-step form: the decrease is strict when
the correlation is strictly between zero and one.
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.noiseStability_majority_odd_antitone (ρ : ℝ)
  (hρ : ρ ∈ Set.Ico 0 1) :
  Antitone fun m =>
    FABL.noiseStability ρ ⋯ (FABL.majority (2 * m + 1)).toReal
    theorem FABL.noiseStability_majority_odd_antitone
  (ρ : ℝ) (hρ : ρ ∈ Set.Ico 0 1) :
  Antitone fun m =>
    FABL.noiseStability ρ ⋯
      (FABL.majority (2 * m + 1)).toReal
    Exercise 5.23: at every `ρ ∈ [0,1)`, odd-majority noise stability is
antitone in the half-arity parameter. At `ρ = 0` every term is zero.
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.noiseStability_majority_odd_strictAnti (ρ : ℝ)
  (hρ : ρ ∈ Set.Ioo 0 1) :
  StrictAnti fun m =>
    FABL.noiseStability ρ ⋯ (FABL.majority (2 * m + 1)).toReal
    theorem FABL.noiseStability_majority_odd_strictAnti
  (ρ : ℝ) (hρ : ρ ∈ Set.Ioo 0 1) :
  StrictAnti fun m =>
    FABL.noiseStability ρ ⋯
      (FABL.majority (2 * m + 1)).toReal
    Exercise 5.23, strengthened away from the endpoint: at every
`ρ ∈ (0,1)`, odd-majority noise stability is strictly antitone.
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.two_div_pi_mul_arcsin_le_noiseStability_majority_odd (m : ℕ)
  {ρ : ℝ} (hρ : ρ ∈ Set.Ico 0 1) :
  2 / Real.pi * Real.arcsin ρ ≤
    FABL.noiseStability ρ ⋯ (FABL.majority (2 * m + 1)).toReal
    theorem FABL.two_div_pi_mul_arcsin_le_noiseStability_majority_odd
  (m : ℕ) {ρ : ℝ} (hρ : ρ ∈ Set.Ico 0 1) :
  2 / Real.pi * Real.arcsin ρ ≤
    FABL.noiseStability ρ ⋯
      (FABL.majority (2 * m + 1)).toReal
    The lower bound in Theorem 5.18: finite odd majority lies above its
Gaussian arcsine limit.
  • theoremdefined in FABL/Chapter05/MajorityNoiseStability.lean
    complete
    theorem FABL.exists_noiseStability_majority_odd_le_arcsine_add_inv_sqrt :
  ∃ C,
    0 < C ∧
      ∀ (m : ℕ) {ρ : ℝ} (hρ : ρ ∈ Set.Ico 0 1),
        FABL.noiseStability ρ ⋯ (FABL.majority (2 * m + 1)).toReal ≤
          2 / Real.pi * Real.arcsin ρ +
            C / (√(1 - ρ ^ 2) * √↑(2 * m + 1))
    theorem FABL.exists_noiseStability_majority_odd_le_arcsine_add_inv_sqrt :
  ∃ C,
    0 < C ∧
      ∀ (m : ℕ) {ρ : ℝ}
        (hρ : ρ ∈ Set.Ico 0 1),
        FABL.noiseStability ρ ⋯
            (FABL.majority
                (2 * m + 1)).toReal ≤
          2 / Real.pi * Real.arcsin ρ +
            C /
              (√(1 - ρ ^ 2) *
                √↑(2 * m + 1))
    The quantitative upper bound in Theorem 5.18, obtained by specializing
the regular homogeneous-threshold invariance bound to equal majority weights.
Lemma5.3.12
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

Exercise 5.24. For integers n,k satisfying 1\le k\le n/2, prove \left(1-\frac{k+1}{n}+\frac{k}{n^2}\right)^{-1/2} \le 1+\frac{2k}{n}.

Lean code for Lemma5.3.12●1 theorem
  • theoremdefined in FABL/Chapter05/FourierCoefficientsOfMajority.lean
    complete
    theorem FABL.exercise5_24 (k n : ℕ) (hk : 1 ≤ k) (hkn : 2 * k ≤ n) :
  (1 - ↑(k + 1) / ↑n + ↑k / ↑n ^ 2) ^ (-(1 / 2)) ≤ 1 + 2 * ↑k / ↑n
    theorem FABL.exercise5_24 (k n : ℕ) (hk : 1 ≤ k)
  (hkn : 2 * k ≤ n) :
  (1 - ↑(k + 1) / ↑n + ↑k / ↑n ^ 2) ^
      (-(1 / 2)) ≤
    1 + 2 * ↑k / ↑n
    Exercise 5.24: the elementary estimate used in the monotonicity of
majority's fixed-level Fourier weights.
Theorem5.3.13
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 5
Statement dependency previews
Preview
Lemma 2.3.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-3fidelity-exact

Theorem 5.22. For each fixed odd positive integer k, \mathbf W^k[\operatorname{Maj}_n] \searrow [\rho^k]\left(\frac2\pi\arcsin\rho\right) =\frac{4}{\pi k2^k}\binom{k-1}{(k-1)/2} as n\ge k tends to infinity through the odd integers. Moreover, for every odd n and odd k with k<n/2, [\rho^k]\left(\frac2\pi\arcsin\rho\right) \le \mathbf W^k[\operatorname{Maj}_n] \le \left(1+\frac{2k}{n}\right) [\rho^k]\left(\frac2\pi\arcsin\rho\right). \tag{5.15} For k>n/2, Corollary 5.20 converts the estimate to the complementary Fourier level.

Lean code for Theorem5.3.13●7 theorems
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.limitingMajorityFourierWeight_pos_of_odd {k : ℕ} (hk : Odd k) :
  0 < FABL.limitingMajorityFourierWeight k
    theorem FABL.limitingMajorityFourierWeight_pos_of_odd
  {k : ℕ} (hk : Odd k) :
  0 < FABL.limitingMajorityFourierWeight k
    Every positive odd limiting majority weight is strictly positive.
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_two_mul_add_one_eq_limiting_mul
  (m j : ℕ) (hj : j ≤ m) :
  FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * m + 1)).toReal =
    FABL.limitingMajorityFourierWeight (2 * j + 1) *
      (Real.pi / 2 * ↑(2 * m + 1) * FABL.oddMajorityInfluence (m - j) *
        FABL.oddMajorityInfluence m)
    theorem FABL.fourierWeightAtLevel_majority_two_mul_add_one_eq_limiting_mul
  (m j : ℕ) (hj : j ≤ m) :
  FABL.fourierWeightAtLevel (2 * j + 1)
      (FABL.majority (2 * m + 1)).toReal =
    FABL.limitingMajorityFourierWeight
        (2 * j + 1) *
      (Real.pi / 2 * ↑(2 * m + 1) *
          FABL.oddMajorityInfluence
            (m - j) *
        FABL.oddMajorityInfluence m)
    The exact central-binomial factorization used in Theorem 5.22.
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.limitingMajorityFourierWeight_le_fourierWeightAtLevel_majority
  {n k : ℕ} (hn : Odd n) (hk : Odd k) (hkn : k ≤ n) :
  FABL.limitingMajorityFourierWeight k ≤
    FABL.fourierWeightAtLevel k (FABL.majority n).toReal
    theorem FABL.limitingMajorityFourierWeight_le_fourierWeightAtLevel_majority
  {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (hkn : k ≤ n) :
  FABL.limitingMajorityFourierWeight k ≤
    FABL.fourierWeightAtLevel k
      (FABL.majority n).toReal
    Theorem 5.22, lower half of (5.15).
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_le_limitingMajorityFourierWeight
  {n k : ℕ} (hn : Odd n) (hk : Odd k) (hkn : 2 * k < n) :
  FABL.fourierWeightAtLevel k (FABL.majority n).toReal ≤
    (1 + 2 * ↑k / ↑n) * FABL.limitingMajorityFourierWeight k
    theorem FABL.fourierWeightAtLevel_majority_le_limitingMajorityFourierWeight
  {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (hkn : 2 * k < n) :
  FABL.fourierWeightAtLevel k
      (FABL.majority n).toReal ≤
    (1 + 2 * ↑k / ↑n) *
      FABL.limitingMajorityFourierWeight k
    Theorem 5.22, upper half of (5.15).
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.majorityFourierWeight_bounds {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (hkn : 2 * k < n) :
  FABL.limitingMajorityFourierWeight k ≤
      FABL.fourierWeightAtLevel k (FABL.majority n).toReal ∧
    FABL.fourierWeightAtLevel k (FABL.majority n).toReal ≤
      (1 + 2 * ↑k / ↑n) * FABL.limitingMajorityFourierWeight k
    theorem FABL.majorityFourierWeight_bounds
  {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (hkn : 2 * k < n) :
  FABL.limitingMajorityFourierWeight k ≤
      FABL.fourierWeightAtLevel k
        (FABL.majority n).toReal ∧
    FABL.fourierWeightAtLevel k
        (FABL.majority n).toReal ≤
      (1 + 2 * ↑k / ↑n) *
        FABL.limitingMajorityFourierWeight
          k
    Theorem 5.22, the complete two-sided estimate (5.15).
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_odd_tendsto {k : ℕ} (hk : Odd k) :
  Filter.Tendsto
    (fun r =>
      FABL.fourierWeightAtLevel k (FABL.majority (k + 2 * r)).toReal)
    Filter.atTop (nhds (FABL.limitingMajorityFourierWeight k))
    theorem FABL.fourierWeightAtLevel_majority_odd_tendsto
  {k : ℕ} (hk : Odd k) :
  Filter.Tendsto
    (fun r =>
      FABL.fourierWeightAtLevel k
        (FABL.majority
            (k + 2 * r)).toReal)
    Filter.atTop
    (nhds
      (FABL.limitingMajorityFourierWeight
        k))
    Theorem 5.22: for fixed positive odd level `k`, the Fourier weight tends to its
arcsine-series coefficient as `n` ranges over all odd arities `n ≥ k`.
  • theoremdefined in FABL/Chapter05/MajorityFourierWeightLimits.lean
    complete
    theorem FABL.fourierWeightAtLevel_majority_odd_strictAnti_and_tendsto {k : ℕ}
  (hk : Odd k) :
  (StrictAnti fun r =>
      FABL.fourierWeightAtLevel k (FABL.majority (k + 2 * r)).toReal) ∧
    Filter.Tendsto
      (fun r =>
        FABL.fourierWeightAtLevel k (FABL.majority (k + 2 * r)).toReal)
      Filter.atTop (nhds (FABL.limitingMajorityFourierWeight k))
    theorem FABL.fourierWeightAtLevel_majority_odd_strictAnti_and_tendsto
  {k : ℕ} (hk : Odd k) :
  (StrictAnti fun r =>
      FABL.fourierWeightAtLevel k
        (FABL.majority
            (k + 2 * r)).toReal) ∧
    Filter.Tendsto
      (fun r =>
        FABL.fourierWeightAtLevel k
          (FABL.majority
              (k + 2 * r)).toReal)
      Filter.atTop
      (nhds
        (FABL.limitingMajorityFourierWeight
          k))
    Theorem 5.22 in the book's `searrow` form. The parameter `r` enumerates exactly all odd
arities `n ≥ k`, via `n = k + 2r`.
Lemma5.3.14
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 4
Statement dependency previews
Preview
Lemma 2.3.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-3supportfidelity-exact

Exercise 5.27.

(a) For every odd positive integer k, prove \left(\frac2\pi\right)^{3/2}k^{-3/2} \le [\rho^k]\left(\frac2\pi\arcsin\rho\right) \le \left(\frac2\pi\right)^{3/2}k^{-3/2} \left(1+O(1/k)\right).

(b) Let k tend to infinity through the odd positive integers, and let n=n(k) be odd with n\ge2k^2. Prove \mathbf W^k[\operatorname{Maj}_n] =\left(\frac2\pi\right)^{3/2}k^{-3/2} \left(1\pm O(1/k)\right), \mathbf W^{>k}[\operatorname{Maj}_n] =\left(\frac2\pi\right)^{3/2}k^{-1/2} \left(1\pm O(1/k)\right), using an integral comparison for the second estimate. Deduce that the Fourier spectrum of \operatorname{Maj}_n is \epsilon-concentrated up to degree \frac8{\pi^3}\epsilon^{-2}+O_\epsilon(1).

Lean code for Lemma5.3.14●20 declarations
  • defdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    def FABL.majorityFourierLevelMain (k : ℕ) : ℝ
    def FABL.majorityFourierLevelMain (k : ℕ) : ℝ
    The leading term in Exercise 5.27(a).
  • defdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    def FABL.majorityFourierTailMain (k : ℕ) : ℝ
    def FABL.majorityFourierTailMain (k : ℕ) : ℝ
    The leading term in Exercise 5.27(b) for Fourier weight above level `k`.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.majorityFourierLevelMain_pos {k : ℕ} (hk : 0 < k) :
  0 < FABL.majorityFourierLevelMain k
    theorem FABL.majorityFourierLevelMain_pos {k : ℕ}
  (hk : 0 < k) :
  0 < FABL.majorityFourierLevelMain k
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.majorityFourierTailMain_pos {k : ℕ} (hk : 0 < k) :
  0 < FABL.majorityFourierTailMain k
    theorem FABL.majorityFourierTailMain_pos {k : ℕ}
  (hk : 0 < k) :
  0 < FABL.majorityFourierTailMain k
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeight_two_mul_add_one_eq (j : ℕ) :
  FABL.limitingMajorityFourierWeight (2 * j + 1) =
    2 / (Real.pi * ↑(2 * j + 1)) * FABL.oddMajorityInfluence j
    theorem FABL.limitingMajorityFourierWeight_two_mul_add_one_eq
  (j : ℕ) :
  FABL.limitingMajorityFourierWeight
      (2 * j + 1) =
    2 / (Real.pi * ↑(2 * j + 1)) *
      FABL.oddMajorityInfluence j
    The arcsine coefficient at `2j+1` is the central-binomial probability from
Exercise 2.22 multiplied by `2 / (π(2j+1))`.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.majorityFourierLevelMain_two_mul_add_one_eq (j : ℕ) :
  FABL.majorityFourierLevelMain (2 * j + 1) =
    2 / (Real.pi * ↑(2 * j + 1)) * FABL.oddMajorityInfluenceMain j
    theorem FABL.majorityFourierLevelMain_two_mul_add_one_eq
  (j : ℕ) :
  FABL.majorityFourierLevelMain
      (2 * j + 1) =
    2 / (Real.pi * ↑(2 * j + 1)) *
      FABL.oddMajorityInfluenceMain j
    The central-binomial main term from Exercise 2.22 is exactly the leading
term in Exercise 5.27(a).
  • defdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    def FABL.limitingMajorityFourierWeightError (k : ℕ) : ℝ
    def FABL.limitingMajorityFourierWeightError
  (k : ℕ) : ℝ
    The nonnegative remainder in Exercise 5.27(a).
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeightError_mem_Icc {k : ℕ} (hk : Odd k) :
  FABL.limitingMajorityFourierWeightError k ∈
    Set.Icc 0 (FABL.majorityFourierLevelMain k / ↑k)
    theorem FABL.limitingMajorityFourierWeightError_mem_Icc
  {k : ℕ} (hk : Odd k) :
  FABL.limitingMajorityFourierWeightError
      k ∈
    Set.Icc 0
      (FABL.majorityFourierLevelMain k /
        ↑k)
    Exercise 5.27(a), with an explicit global remainder interval on positive odd levels.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.majorityFourierLevelMain_le_limitingMajorityFourierWeight {k : ℕ}
  (hk : Odd k) :
  FABL.majorityFourierLevelMain k ≤ FABL.limitingMajorityFourierWeight k
    theorem FABL.majorityFourierLevelMain_le_limitingMajorityFourierWeight
  {k : ℕ} (hk : Odd k) :
  FABL.majorityFourierLevelMain k ≤
    FABL.limitingMajorityFourierWeight k
    Exercise 5.27(a), lower estimate.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeight_le_levelMain_mul {k : ℕ}
  (hk : Odd k) :
  FABL.limitingMajorityFourierWeight k ≤
    FABL.majorityFourierLevelMain k * (1 + 1 / ↑k)
    theorem FABL.limitingMajorityFourierWeight_le_levelMain_mul
  {k : ℕ} (hk : Odd k) :
  FABL.limitingMajorityFourierWeight k ≤
    FABL.majorityFourierLevelMain k *
      (1 + 1 / ↑k)
    Exercise 5.27(a), upper estimate with the literal factor `1 + 1/k`.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeightError_isBigO :
  (fun k => FABL.limitingMajorityFourierWeightError ↑k) =O[Filter.atTop]
    fun k => FABL.majorityFourierLevelMain ↑k / ↑↑k
    theorem FABL.limitingMajorityFourierWeightError_isBigO :
  (fun k =>
      FABL.limitingMajorityFourierWeightError
        ↑k) =O[Filter.atTop]
    fun k =>
    FABL.majorityFourierLevelMain ↑k / ↑↑k
    Exercise 5.27(a) in literal Mathlib `O(1/k)` notation along the positive odd integers.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeightAbove_eq_tsum_odd {k : ℕ}
  (hk : Odd k) :
  FABL.limitingMajorityFourierWeightAbove k =
    ∑' (r : ℕ), FABL.limitingMajorityFourierWeight (k + 2 * (r + 1))
    theorem FABL.limitingMajorityFourierWeightAbove_eq_tsum_odd
  {k : ℕ} (hk : Odd k) :
  FABL.limitingMajorityFourierWeightAbove
      k =
    ∑' (r : ℕ),
      FABL.limitingMajorityFourierWeight
        (k + 2 * (r + 1))
    The limiting tail is exactly the sum over the subsequent odd levels.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeightAbove_mem_Icc {k : ℕ} (hk : Odd k) :
  FABL.limitingMajorityFourierWeightAbove k ∈
    Set.Icc (FABL.majorityFourierTailMain k * (1 - 1 / ↑k))
      (FABL.majorityFourierTailMain k * (1 + 1 / (3 * ↑k)))
    theorem FABL.limitingMajorityFourierWeightAbove_mem_Icc
  {k : ℕ} (hk : Odd k) :
  FABL.limitingMajorityFourierWeightAbove
      k ∈
    Set.Icc
      (FABL.majorityFourierTailMain k *
        (1 - 1 / ↑k))
      (FABL.majorityFourierTailMain k *
        (1 + 1 / (3 * ↑k)))
    Exercise 5.27(b), the limiting-tail estimate with explicit `1 ± O(1/k)`
constants before passage to a varying finite arity.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.abs_limitingMajorityFourierWeightAbove_div_tailMain_sub_one_le
  {k : ℕ} (hk : Odd k) :
  |FABL.limitingMajorityFourierWeightAbove k /
          FABL.majorityFourierTailMain k -
        1| ≤
    1 / ↑k
    theorem FABL.abs_limitingMajorityFourierWeightAbove_div_tailMain_sub_one_le
  {k : ℕ} (hk : Odd k) :
  |FABL.limitingMajorityFourierWeightAbove
            k /
          FABL.majorityFourierTailMain k -
        1| ≤
    1 / ↑k
    Exercise 5.27(b): the limiting Fourier tail has relative error at most `1/k`.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.limitingMajorityFourierWeightAbove_relativeError_isBigO :
  (fun k =>
      FABL.limitingMajorityFourierWeightAbove ↑k /
          FABL.majorityFourierTailMain ↑k -
        1) =O[Filter.atTop]
    fun k => 1 / ↑↑k
    theorem FABL.limitingMajorityFourierWeightAbove_relativeError_isBigO :
  (fun k =>
      FABL.limitingMajorityFourierWeightAbove
            ↑k /
          FABL.majorityFourierTailMain
            ↑k -
        1) =O[Filter.atTop]
    fun k => 1 / ↑↑k
    Exercise 5.27(b), limiting-tail form in literal Mathlib asymptotic notation.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.abs_fourierWeightAtLevel_majority_div_levelMain_sub_one_le
  {n k : ℕ} (hn : Odd n) (hk : Odd k) (hnk : 2 * k ^ 2 ≤ n) :
  |FABL.fourierWeightAtLevel k (FABL.majority n).toReal /
          FABL.majorityFourierLevelMain k -
        1| ≤
    3 / ↑k
    theorem FABL.abs_fourierWeightAtLevel_majority_div_levelMain_sub_one_le
  {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (hnk : 2 * k ^ 2 ≤ n) :
  |FABL.fourierWeightAtLevel k
            (FABL.majority n).toReal /
          FABL.majorityFourierLevelMain
            k -
        1| ≤
    3 / ↑k
    Corollary 5.23, the finite-dimensional level estimate with an explicit relative error.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.abs_fourierWeightAbove_majority_div_tailMain_sub_one_le {n k : ℕ}
  (hn : Odd n) (hk : Odd k) (hnk : 2 * k ^ 2 ≤ n) :
  |FABL.fourierWeightAbove k (FABL.majority n).toReal /
          FABL.majorityFourierTailMain k -
        1| ≤
    5 / ↑k
    theorem FABL.abs_fourierWeightAbove_majority_div_tailMain_sub_one_le
  {n k : ℕ} (hn : Odd n) (hk : Odd k)
  (hnk : 2 * k ^ 2 ≤ n) :
  |FABL.fourierWeightAbove k
            (FABL.majority n).toReal /
          FABL.majorityFourierTailMain k -
        1| ≤
    5 / ↑k
    Corollary 5.23, the finite-dimensional tail estimate with an explicit relative error.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.majorityFourierLevel_family_relativeError_isBigO
  (n : { k // Odd k } → ℕ) (hnOdd : ∀ (k : { k // Odd k }), Odd (n k))
  (hnQuadratic : ∀ (k : { k // Odd k }), 2 * ↑k ^ 2 ≤ n k) :
  (fun k =>
      FABL.fourierWeightAtLevel (↑k) (FABL.majority (n k)).toReal /
          FABL.majorityFourierLevelMain ↑k -
        1) =O[Filter.atTop]
    fun k => 1 / ↑↑k
    theorem FABL.majorityFourierLevel_family_relativeError_isBigO
  (n : { k // Odd k } → ℕ)
  (hnOdd :
    ∀ (k : { k // Odd k }), Odd (n k))
  (hnQuadratic :
    ∀ (k : { k // Odd k }),
      2 * ↑k ^ 2 ≤ n k) :
  (fun k =>
      FABL.fourierWeightAtLevel (↑k)
            (FABL.majority (n k)).toReal /
          FABL.majorityFourierLevelMain
            ↑k -
        1) =O[Filter.atTop]
    fun k => 1 / ↑↑k
    Corollary 5.23, the `W^k` estimate for every odd family `n(k) ≥ 2k²`, in
literal Mathlib asymptotic notation.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.majorityFourierTail_family_relativeError_isBigO
  (n : { k // Odd k } → ℕ) (hnOdd : ∀ (k : { k // Odd k }), Odd (n k))
  (hnQuadratic : ∀ (k : { k // Odd k }), 2 * ↑k ^ 2 ≤ n k) :
  (fun k =>
      FABL.fourierWeightAbove (↑k) (FABL.majority (n k)).toReal /
          FABL.majorityFourierTailMain ↑k -
        1) =O[Filter.atTop]
    fun k => 1 / ↑↑k
    theorem FABL.majorityFourierTail_family_relativeError_isBigO
  (n : { k // Odd k } → ℕ)
  (hnOdd :
    ∀ (k : { k // Odd k }), Odd (n k))
  (hnQuadratic :
    ∀ (k : { k // Odd k }),
      2 * ↑k ^ 2 ≤ n k) :
  (fun k =>
      FABL.fourierWeightAbove (↑k)
            (FABL.majority (n k)).toReal /
          FABL.majorityFourierTailMain
            ↑k -
        1) =O[Filter.atTop]
    fun k => 1 / ↑↑k
    Corollary 5.23, the `W^{>k}` estimate for every odd family `n(k) ≥ 2k²`,
in literal Mathlib asymptotic notation.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.tendsto_limitingMajorityFourierWeightAbove_odd_zero :
  Filter.Tendsto
    (fun q => FABL.limitingMajorityFourierWeightAbove (2 * q + 1))
    Filter.atTop (nhds 0)
    theorem FABL.tendsto_limitingMajorityFourierWeightAbove_odd_zero :
  Filter.Tendsto
    (fun q =>
      FABL.limitingMajorityFourierWeightAbove
        (2 * q + 1))
    Filter.atTop (nhds 0)
    The limiting odd-level tail tends to zero.
Corollary5.3.15
Group: Chapter 5: Majority and threshold functions (107)
Group member previews
Preview
Lemma 5.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
Tagssection-5-3fidelity-exact

Corollary 5.23. Let k tend to infinity through the odd positive integers, and let n=n(k) be odd with n\ge2k^2. Then \mathbf W^k[\operatorname{Maj}_n] =\left(\frac2\pi\right)^{3/2}k^{-3/2} \left(1\pm O(1/k)\right), and \mathbf W^{>k}[\operatorname{Maj}_n] =\left(\frac2\pi\right)^{3/2}k^{-1/2} \left(1\pm O(1/k)\right). Consequently, the Fourier spectrum of \operatorname{Maj}_n is \epsilon-concentrated up to degree \frac8{\pi^3}\epsilon^{-2}+O_\epsilon(1).

Lean code for Corollary5.3.15●2 theorems
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.exists_majorityFourierConcentrationCutoff {ε : ℝ} (hε : 0 < ε) :
  ∃ B,
    0 ≤ B ∧
      ∃ k,
        Odd k ∧
          ↑k ≤ 8 / Real.pi ^ 3 * ε⁻¹ ^ 2 + B ∧
            ∀ (n : ℕ),
              Odd n →
                2 * k ^ 2 ≤ n →
                  FABL.IsFourierSpectrumConcentratedUpTo
                    (FABL.majority n).toReal ε ↑k
    theorem FABL.exists_majorityFourierConcentrationCutoff
  {ε : ℝ} (hε : 0 < ε) :
  ∃ B,
    0 ≤ B ∧
      ∃ k,
        Odd k ∧
          ↑k ≤
              8 / Real.pi ^ 3 * ε⁻¹ ^ 2 +
                B ∧
            ∀ (n : ℕ),
              Odd n →
                2 * k ^ 2 ≤ n →
                  FABL.IsFourierSpectrumConcentratedUpTo
                    (FABL.majority
                        n).toReal
                    ε ↑k
    Corollary 5.23, the book's `8/π³ ε⁻² + Oε(1)` cutoff with all
quantifiers explicit. The remainder depends only on `ε`, never on the arity.
  • theoremdefined in FABL/Chapter05/MajorityFourierTailAsymptotics.lean
    complete
    theorem FABL.corollary5_23 (n : { k // Odd k } → ℕ)
  (hnOdd : ∀ (k : { k // Odd k }), Odd (n k))
  (hnQuadratic : ∀ (k : { k // Odd k }), 2 * ↑k ^ 2 ≤ n k) :
  ((fun k =>
        FABL.fourierWeightAtLevel (↑k) (FABL.majority (n k)).toReal /
            FABL.majorityFourierLevelMain ↑k -
          1) =O[Filter.atTop]
      fun k => 1 / ↑↑k) ∧
    (fun k =>
        FABL.fourierWeightAbove (↑k) (FABL.majority (n k)).toReal /
            FABL.majorityFourierTailMain ↑k -
          1) =O[Filter.atTop]
      fun k => 1 / ↑↑k
    theorem FABL.corollary5_23
  (n : { k // Odd k } → ℕ)
  (hnOdd :
    ∀ (k : { k // Odd k }), Odd (n k))
  (hnQuadratic :
    ∀ (k : { k // Odd k }),
      2 * ↑k ^ 2 ≤ n k) :
  ((fun k =>
        FABL.fourierWeightAtLevel (↑k)
              (FABL.majority
                  (n k)).toReal /
            FABL.majorityFourierLevelMain
              ↑k -
          1) =O[Filter.atTop]
      fun k => 1 / ↑↑k) ∧
    (fun k =>
        FABL.fourierWeightAbove (↑k)
              (FABL.majority
                  (n k)).toReal /
            FABL.majorityFourierTailMain
              ↑k -
          1) =O[Filter.atTop]
      fun k => 1 / ↑↑k
    Corollary 5.23, collecting the two family asymptotics with their respective error terms.