Analysis of Boolean Functions in Lean

5.4. Degree-1 weight🔗

Lemma5.4.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 3
Statement dependency previews
Preview
Definition 1.4.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-4supportfidelity-generalized-zero-codimension

Exercise 5.29 (Fourier weight of a subcube). Let J\subseteq[n] have cardinality k\ge1, fix values a_i\in\mathbb F_2 for i\in J, and let A=\{x\in\mathbb F_2^n:x_i=a_i\text{ for every }i\in J\}. If f=1_A, then |\widehat f(S)| = \begin{cases} 2^{-k},&S\subseteq J,\\ 0,&S\not\subseteq J. \end{cases} In particular, \widehat f(\varnothing)=2^{-k}, \qquad \sum_{i=1}^n\widehat f(\{i\})^2=k2^{-2k}. Thus \mathbb E[f]=2^{-k} and \mathbf W^1[f]=k2^{-2k}.

Lean code for Lemma5.4.1●3 theorems
  • theoremdefined in FABL/Chapter05/DegreeOneWeight.lean
    complete
    theorem FABL.abs_vectorFourierCoeff_setIndicator_coordinateSubcube {n : ℕ}
  (coordinates : Finset (Fin n)) (basePoint γ : FABL.F₂Cube n) :
  |FABL.vectorFourierCoeff
        (FABL.setIndicator
          (FABL.F₂DecisionTree.coordinateSubcube coordinates basePoint))
        γ| =
    if FABL.f₂Support γ ⊆ coordinates then (2 ^ coordinates.card)⁻¹
    else 0
    theorem FABL.abs_vectorFourierCoeff_setIndicator_coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n))
  (basePoint γ : FABL.F₂Cube n) :
  |FABL.vectorFourierCoeff
        (FABL.setIndicator
          (FABL.F₂DecisionTree.coordinateSubcube
            coordinates basePoint))
        γ| =
    if FABL.f₂Support γ ⊆ coordinates then
      (2 ^ coordinates.card)⁻¹
    else 0
    Exercise 5.29: the Fourier coefficients of a coordinate-subcube indicator have magnitude
`2⁻ᵏ` exactly on frequencies supported inside its `k` fixed coordinates.
  • theoremdefined in FABL/Chapter05/DegreeOneWeight.lean
    complete
    theorem FABL.expect_setIndicator_coordinateSubcube {n : ℕ}
  (coordinates : Finset (Fin n)) (basePoint : FABL.F₂Cube n) :
  (Finset.univ.expect fun x =>
      FABL.setIndicator
        (FABL.F₂DecisionTree.coordinateSubcube coordinates basePoint)
        x) =
    (2 ^ coordinates.card)⁻¹
    theorem FABL.expect_setIndicator_coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n))
  (basePoint : FABL.F₂Cube n) :
  (Finset.univ.expect fun x =>
      FABL.setIndicator
        (FABL.F₂DecisionTree.coordinateSubcube
          coordinates basePoint)
        x) =
    (2 ^ coordinates.card)⁻¹
    Exercise 5.29: a coordinate subcube of codimension `k` has uniform expectation `2⁻ᵏ`.
  • theoremdefined in FABL/Chapter05/DegreeOneWeight.lean
    complete
    theorem FABL.sum_sq_vectorFourierCoeff_support_card_one_setIndicator_coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n)) (basePoint : FABL.F₂Cube n) :
  ∑ γ with (FABL.f₂Support γ).card = 1,
      FABL.vectorFourierCoeff
          (FABL.setIndicator
            (FABL.F₂DecisionTree.coordinateSubcube coordinates
              basePoint))
          γ ^
        2 =
    ↑coordinates.card * (2 ^ coordinates.card)⁻¹ ^ 2
    theorem FABL.sum_sq_vectorFourierCoeff_support_card_one_setIndicator_coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n))
  (basePoint : FABL.F₂Cube n) :
  ∑ γ with (FABL.f₂Support γ).card = 1,
      FABL.vectorFourierCoeff
          (FABL.setIndicator
            (FABL.F₂DecisionTree.coordinateSubcube
              coordinates basePoint))
          γ ^
        2 =
    ↑coordinates.card *
      (2 ^ coordinates.card)⁻¹ ^ 2
    Exercise 5.29: the level-one Fourier weight of a coordinate-subcube indicator is
`k 2⁻²ᵏ`, written directly in vector-indexed Fourier notation.
Proposition5.4.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.
uses 1used by 0✓L∃∀N
Tagssection-5-4fidelity-exact

Proposition 5.24. Let f:\mathbb F_2^n\to\{0,1\} be the indicator of a subcube of codimension k\ge1, for example the \operatorname{AND}_k function. Then \mathbb E[f]=2^{-k}, \qquad \mathbf W^1[f]=k2^{-2k}.

Lean code for Proposition5.4.2●1 theorem
  • theoremdefined in FABL/Chapter05/DegreeOneWeight.lean
    complete
    theorem FABL.expectation_and_degreeOneWeight_setIndicator_coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n)) (basePoint : FABL.F₂Cube n)
  (_hcoordinates : coordinates.Nonempty) :
  (Finset.univ.expect fun x =>
        FABL.setIndicator
          (FABL.F₂DecisionTree.coordinateSubcube coordinates basePoint)
          x) =
      (2 ^ coordinates.card)⁻¹ ∧
    ∑ γ with (FABL.f₂Support γ).card = 1,
        FABL.vectorFourierCoeff
            (FABL.setIndicator
              (FABL.F₂DecisionTree.coordinateSubcube coordinates
                basePoint))
            γ ^
          2 =
      ↑coordinates.card * (2 ^ coordinates.card)⁻¹ ^ 2
    theorem FABL.expectation_and_degreeOneWeight_setIndicator_coordinateSubcube
  {n : ℕ} (coordinates : Finset (Fin n))
  (basePoint : FABL.F₂Cube n)
  (_hcoordinates : coordinates.Nonempty) :
  (Finset.univ.expect fun x =>
        FABL.setIndicator
          (FABL.F₂DecisionTree.coordinateSubcube
            coordinates basePoint)
          x) =
      (2 ^ coordinates.card)⁻¹ ∧
    ∑ γ with (FABL.f₂Support γ).card = 1,
        FABL.vectorFourierCoeff
            (FABL.setIndicator
              (FABL.F₂DecisionTree.coordinateSubcube
                coordinates basePoint))
            γ ^
          2 =
      ↑coordinates.card *
        (2 ^ coordinates.card)⁻¹ ^ 2
    Proposition 5.24: a nontrivial coordinate-subcube indicator has expectation `2⁻ᵏ` and
degree-one Fourier weight `k 2⁻²ᵏ`.
Lemma5.4.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.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-4supportfidelity-exact

Exercise 5.30 (the Hamming-ball limit). Fix t\in\mathbb R, and for uniform x\in\{-1,1\}^n write S_n(x)=\frac1{\sqrt n}\sum_{i=1}^n x_i, \qquad f_n(x)=1\{S_n(x)>t\}. The symmetry of f_n gives, for every i\in[n], \widehat f_n(\{i\}) =\frac1{\sqrt n}\mathbb E[f_nS_n], \qquad \mathbf W^1[f_n]=\bigl(\mathbb E[f_nS_n]\bigr)^2. The Central Limit Theorem and uniform integrability imply, for Z\sim N(0,1), \mathbb E[f_n]\longrightarrow\Pr[Z>t]=\bar\Phi(t), \qquad \mathbb E[f_nS_n]\longrightarrow \mathbb E[Z1\{Z>t\}]=\phi(t). Consequently \mathbf W^1[f_n]\to\phi(t)^2.

Lean code for Lemma5.4.3●8 declarations
  • defdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    def FABL.normalizedRademacherSum (n : ℕ) (x : FABL.SignCube n) : ℝ
    def FABL.normalizedRademacherSum (n : ℕ)
  (x : FABL.SignCube n) : ℝ
    The normalized sum of the coordinates of a sign-cube input.
  • defdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    def FABL.hammingUpperTailIndicator (t : ℝ) (n : ℕ) (x : FABL.SignCube n) : ℝ
    def FABL.hammingUpperTailIndicator (t : ℝ)
  (n : ℕ) (x : FABL.SignCube n) : ℝ
    The real indicator of the strict upper level set of the normalized
Rademacher sum.
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.hammingUpperTailIndicator_isSymmetric (t : ℝ) (n : ℕ) :
  FABL.IsSymmetric (FABL.hammingUpperTailIndicator t n)
    theorem FABL.hammingUpperTailIndicator_isSymmetric
  (t : ℝ) (n : ℕ) :
  FABL.IsSymmetric
    (FABL.hammingUpperTailIndicator t n)
    The Hamming upper-tail indicator is invariant under coordinate
permutations.
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.fourierCoeff_hammingUpperTailIndicator_singleton (t : ℝ) (m : ℕ)
  (i : Fin (m + 1)) :
  FABL.fourierCoeff (FABL.hammingUpperTailIndicator t (m + 1)) {i} =
    (Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t (m + 1) x *
          FABL.normalizedRademacherSum (m + 1) x) /
      √↑(m + 1)
    theorem FABL.fourierCoeff_hammingUpperTailIndicator_singleton
  (t : ℝ) (m : ℕ) (i : Fin (m + 1)) :
  FABL.fourierCoeff
      (FABL.hammingUpperTailIndicator t
        (m + 1))
      {i} =
    (Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t
            (m + 1) x *
          FABL.normalizedRademacherSum
            (m + 1) x) /
      √↑(m + 1)
    Exercise 5.30: every singleton Fourier coefficient of the Hamming
upper-tail indicator is the normalized truncated first moment.
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_hammingUpperTailIndicator (t : ℝ)
  (m : ℕ) :
  FABL.fourierWeightAtLevel 1
      (FABL.hammingUpperTailIndicator t (m + 1)) =
    (Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t (m + 1) x *
          FABL.normalizedRademacherSum (m + 1) x) ^
      2
    theorem FABL.fourierWeightAtLevel_one_hammingUpperTailIndicator
  (t : ℝ) (m : ℕ) :
  FABL.fourierWeightAtLevel 1
      (FABL.hammingUpperTailIndicator t
        (m + 1)) =
    (Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t
            (m + 1) x *
          FABL.normalizedRademacherSum
            (m + 1) x) ^
      2
    Exercise 5.30: the level-one Fourier weight of the Hamming upper-tail
indicator is the square of its truncated first moment.
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.abs_expect_hammingUpperTailIndicator_sub_standardGaussianUpperTail_le
  (t : ℝ) (m : ℕ) :
  |(Finset.univ.expect fun x =>
          FABL.hammingUpperTailIndicator t (m + 1) x) -
        FABL.standardGaussianUpperTail t| ≤
    2 * ProbabilityTheory.thirdMomentBerryEsseenConstant * (√↑(m + 1))⁻¹
    theorem FABL.abs_expect_hammingUpperTailIndicator_sub_standardGaussianUpperTail_le
  (t : ℝ) (m : ℕ) :
  |(Finset.univ.expect fun x =>
          FABL.hammingUpperTailIndicator t
            (m + 1) x) -
        FABL.standardGaussianUpperTail
          t| ≤
    2 *
        ProbabilityTheory.thirdMomentBerryEsseenConstant *
      (√↑(m + 1))⁻¹
    The uniform Berry--Esseen bound for the upper level set of a normalized
equal-weight Rademacher sum.
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.tendsto_expect_hammingUpperTailIndicator (t : ℝ) :
  Filter.Tendsto
    (fun m =>
      Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t (m + 1) x)
    Filter.atTop (nhds (FABL.standardGaussianUpperTail t))
    theorem FABL.tendsto_expect_hammingUpperTailIndicator
  (t : ℝ) :
  Filter.Tendsto
    (fun m =>
      Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t
          (m + 1) x)
    Filter.atTop
    (nhds
      (FABL.standardGaussianUpperTail t))
    Exercise 5.30: the expectations of the Hamming upper-tail indicators
converge to the corresponding standard Gaussian upper tail.
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.tendsto_expect_hammingUpperTailIndicator_mul_normalizedRademacherSum
  (t : ℝ) :
  Filter.Tendsto
    (fun m =>
      Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t (m + 1) x *
          FABL.normalizedRademacherSum (m + 1) x)
    Filter.atTop (nhds (ProbabilityTheory.gaussianPDFReal 0 1 t))
    theorem FABL.tendsto_expect_hammingUpperTailIndicator_mul_normalizedRademacherSum
  (t : ℝ) :
  Filter.Tendsto
    (fun m =>
      Finset.univ.expect fun x =>
        FABL.hammingUpperTailIndicator t
            (m + 1) x *
          FABL.normalizedRademacherSum
            (m + 1) x)
    Filter.atTop
    (nhds
      (ProbabilityTheory.gaussianPDFReal 0
        1 t))
    Exercise 5.30: the truncated first moment of the normalized Rademacher
sum converges to the standard Gaussian density at the threshold.
Proposition5.4.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.
uses 1
Used by 3
Reverse dependency previews
Preview
Lemma 5.6.17
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-4fidelity-exact

Proposition 5.25. Fix t\in\mathbb R. For each n, define the linear threshold function f_n:\{-1,1\}^n\to\{0,1\} by f_n(x)=1 \quad\Longleftrightarrow\quad \frac1{\sqrt n}\sum_{i=1}^n x_i>t. Equivalently, f_n is the indicator of the Hamming ball \left\{ x:\Delta(x,(1,\ldots,1))<\frac n2-\frac{t\sqrt n}{2} \right\}. Then \lim_{n\to\infty}\mathbb E[f_n]=\bar\Phi(t), \qquad \lim_{n\to\infty}\mathbf W^1[f_n]=\phi(t)^2.

Lean code for Proposition5.4.4●1 theorem
  • theoremdefined in FABL/Chapter05/HammingBallLimit.lean
    complete
    theorem FABL.proposition5_25 (t : ℝ) :
  Filter.Tendsto
      (fun m =>
        Finset.univ.expect fun x =>
          FABL.hammingUpperTailIndicator t (m + 1) x)
      Filter.atTop (nhds (FABL.standardGaussianUpperTail t)) ∧
    Filter.Tendsto
      (fun m =>
        FABL.fourierWeightAtLevel 1
          (FABL.hammingUpperTailIndicator t (m + 1)))
      Filter.atTop (nhds (ProbabilityTheory.gaussianPDFReal 0 1 t ^ 2))
    theorem FABL.proposition5_25 (t : ℝ) :
  Filter.Tendsto
      (fun m =>
        Finset.univ.expect fun x =>
          FABL.hammingUpperTailIndicator t
            (m + 1) x)
      Filter.atTop
      (nhds
        (FABL.standardGaussianUpperTail
          t)) ∧
    Filter.Tendsto
      (fun m =>
        FABL.fourierWeightAtLevel 1
          (FABL.hammingUpperTailIndicator
            t (m + 1)))
      Filter.atTop
      (nhds
        (ProbabilityTheory.gaussianPDFReal
            0 1 t ^
          2))
    O'Donnell, Proposition 5.25: Hamming upper-tail indicators converge in
expectation to the Gaussian upper tail, and their level-one Fourier weights
converge to the squared Gaussian density.
Definition5.4.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.
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 5.4.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-4fidelity-exact

Definition 5.26. The Gaussian isoperimetric function U:[0,1]\longrightarrow \left[0,\frac1{\sqrt{2\pi}}\right] is defined on 0<\alpha<1 by U(\alpha) =\phi\bigl(\bar\Phi^{-1}(\alpha)\bigr), and by U(0)=U(1)=0. Thus U=\phi\circ\bar\Phi^{-1}. The symmetry \bar\Phi(t)=\Phi(-t) and \phi(t)=\phi(-t) also give U=\phi\circ\Phi^{-1}, \qquad U(\alpha)=U(1-\alpha).

Lean code for Definition5.4.5●24 declarations
  • defdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    def FABL.standardGaussianUpperTail (t : ℝ) : ℝ
    def FABL.standardGaussianUpperTail (t : ℝ) : ℝ
    The standard Gaussian upper-tail probability
`\bar Φ(t) = Pr[Z > t]`.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTail_eq_measureReal_Ioi (t : ℝ) :
  FABL.standardGaussianUpperTail t =
    (ProbabilityTheory.gaussianReal 0 1).real (Set.Ioi t)
    theorem FABL.standardGaussianUpperTail_eq_measureReal_Ioi
  (t : ℝ) :
  FABL.standardGaussianUpperTail t =
    (ProbabilityTheory.gaussianReal 0
          1).real
      (Set.Ioi t)
    The CDF complement is the real mass of the strict upper ray.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTail_pos (t : ℝ) :
  0 < FABL.standardGaussianUpperTail t
    theorem FABL.standardGaussianUpperTail_pos
  (t : ℝ) :
  0 < FABL.standardGaussianUpperTail t
    Every finite threshold has positive standard Gaussian upper tail.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTail_lt_one (t : ℝ) :
  FABL.standardGaussianUpperTail t < 1
    theorem FABL.standardGaussianUpperTail_lt_one
  (t : ℝ) :
  FABL.standardGaussianUpperTail t < 1
    Every finite threshold has standard Gaussian upper tail strictly below one.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTail_strictAnti :
  StrictAnti FABL.standardGaussianUpperTail
    theorem FABL.standardGaussianUpperTail_strictAnti :
  StrictAnti
    FABL.standardGaussianUpperTail
    The standard Gaussian upper tail is strictly decreasing.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.continuous_standardGaussianUpperTail :
  Continuous FABL.standardGaussianUpperTail
    theorem FABL.continuous_standardGaussianUpperTail :
  Continuous
    FABL.standardGaussianUpperTail
    The standard Gaussian upper tail is continuous.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.tendsto_standardGaussianUpperTail_atTop :
  Filter.Tendsto FABL.standardGaussianUpperTail Filter.atTop (nhds 0)
    theorem FABL.tendsto_standardGaussianUpperTail_atTop :
  Filter.Tendsto
    FABL.standardGaussianUpperTail
    Filter.atTop (nhds 0)
    The standard Gaussian upper tail tends to zero at positive infinity.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.tendsto_standardGaussianUpperTail_atBot :
  Filter.Tendsto FABL.standardGaussianUpperTail Filter.atBot (nhds 1)
    theorem FABL.tendsto_standardGaussianUpperTail_atBot :
  Filter.Tendsto
    FABL.standardGaussianUpperTail
    Filter.atBot (nhds 1)
    The standard Gaussian upper tail tends to one at negative infinity.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTail_neg (t : ℝ) :
  FABL.standardGaussianUpperTail (-t) =
    1 - FABL.standardGaussianUpperTail t
    theorem FABL.standardGaussianUpperTail_neg
  (t : ℝ) :
  FABL.standardGaussianUpperTail (-t) =
    1 - FABL.standardGaussianUpperTail t
    Gaussian reflection exchanges an upper tail with its complement.
  • defdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    def FABL.standardGaussianUpperTailOpen (t : ℝᵒᵈ) : ↑(Set.Ioo 0 1)
    def FABL.standardGaussianUpperTailOpen
  (t : ℝᵒᵈ) : ↑(Set.Ioo 0 1)
    The standard Gaussian upper tail, restricted to its exact open-unit range.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.strictMono_standardGaussianUpperTailOpen :
  StrictMono FABL.standardGaussianUpperTailOpen
    theorem FABL.strictMono_standardGaussianUpperTailOpen :
  StrictMono
    FABL.standardGaussianUpperTailOpen
    Reverse-ordered thresholds map strictly increasingly to upper-tail probabilities.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.surjective_standardGaussianUpperTailOpen :
  Function.Surjective FABL.standardGaussianUpperTailOpen
    theorem FABL.surjective_standardGaussianUpperTailOpen :
  Function.Surjective
    FABL.standardGaussianUpperTailOpen
    Every probability strictly between zero and one is a standard Gaussian upper tail.
  • defdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    def FABL.standardGaussianUpperTailOrderIso : ℝᵒᵈ ≃o ↑(Set.Ioo 0 1)
    def FABL.standardGaussianUpperTailOrderIso :
  ℝᵒᵈ ≃o ↑(Set.Ioo 0 1)
    The order isomorphism from reverse-ordered thresholds to Gaussian
upper-tail probabilities in `(0,1)`.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTailOrderIso_apply (t : ℝᵒᵈ) :
  ↑(FABL.standardGaussianUpperTailOrderIso t) =
    FABL.standardGaussianUpperTail t
    theorem FABL.standardGaussianUpperTailOrderIso_apply
  (t : ℝᵒᵈ) :
  ↑(FABL.standardGaussianUpperTailOrderIso
        t) =
    FABL.standardGaussianUpperTail t
    The Gaussian upper-tail order isomorphism has the expected underlying function.
  • defdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    def FABL.standardGaussianUpperQuantile (α : ↑(Set.Ioo 0 1)) : ℝ
    def FABL.standardGaussianUpperQuantile
  (α : ↑(Set.Ioo 0 1)) : ℝ
    The unique threshold whose standard Gaussian upper tail is `α`.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperTail_quantile (α : ↑(Set.Ioo 0 1)) :
  FABL.standardGaussianUpperTail
      (FABL.standardGaussianUpperQuantile α) =
    ↑α
    theorem FABL.standardGaussianUpperTail_quantile
  (α : ↑(Set.Ioo 0 1)) :
  FABL.standardGaussianUpperTail
      (FABL.standardGaussianUpperQuantile
        α) =
    ↑α
    Taking the upper tail of its quantile returns the original probability.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperQuantile_upperTail (t : ℝ) :
  FABL.standardGaussianUpperQuantile
      ⟨FABL.standardGaussianUpperTail t, ⋯⟩ =
    t
    theorem FABL.standardGaussianUpperQuantile_upperTail
  (t : ℝ) :
  FABL.standardGaussianUpperQuantile
      ⟨FABL.standardGaussianUpperTail t,
        ⋯⟩ =
    t
    Taking the quantile of a finite threshold's upper tail returns the threshold.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.standardGaussianUpperQuantile_one_sub (α : ↑(Set.Ioo 0 1)) :
  FABL.standardGaussianUpperQuantile ⟨1 - ↑α, ⋯⟩ =
    -FABL.standardGaussianUpperQuantile α
    theorem FABL.standardGaussianUpperQuantile_one_sub
  (α : ↑(Set.Ioo 0 1)) :
  FABL.standardGaussianUpperQuantile
      ⟨1 - ↑α, ⋯⟩ =
    -FABL.standardGaussianUpperQuantile α
    Complementary upper-tail probabilities have opposite quantiles.
  • defdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    def FABL.gaussianIsoperimetric (α : ↑unitInterval) : ℝ
    def FABL.gaussianIsoperimetric
  (α : ↑unitInterval) : ℝ
    Definition 5.26: the Gaussian isoperimetric function on `[0,1]`,
extended by zero at both endpoints.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.gaussianIsoperimetric_zero : FABL.gaussianIsoperimetric 0 = 0
    theorem FABL.gaussianIsoperimetric_zero :
  FABL.gaussianIsoperimetric 0 = 0
    The Gaussian isoperimetric function vanishes at zero.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.gaussianIsoperimetric_one : FABL.gaussianIsoperimetric 1 = 0
    theorem FABL.gaussianIsoperimetric_one :
  FABL.gaussianIsoperimetric 1 = 0
    The Gaussian isoperimetric function vanishes at one.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.gaussianIsoperimetric_apply_of_mem_Ioo (α : ↑unitInterval)
  (hα : ↑α ∈ Set.Ioo 0 1) :
  FABL.gaussianIsoperimetric α =
    ProbabilityTheory.gaussianPDFReal 0 1
      (FABL.standardGaussianUpperQuantile ⟨↑α, hα⟩)
    theorem FABL.gaussianIsoperimetric_apply_of_mem_Ioo
  (α : ↑unitInterval)
  (hα : ↑α ∈ Set.Ioo 0 1) :
  FABL.gaussianIsoperimetric α =
    ProbabilityTheory.gaussianPDFReal 0 1
      (FABL.standardGaussianUpperQuantile
        ⟨↑α, hα⟩)
    In the open unit interval, `U` is the density evaluated at the upper quantile.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.gaussianIsoperimetric_mem_Icc (α : ↑unitInterval) :
  FABL.gaussianIsoperimetric α ∈ Set.Icc 0 (√(2 * Real.pi))⁻¹
    theorem FABL.gaussianIsoperimetric_mem_Icc
  (α : ↑unitInterval) :
  FABL.gaussianIsoperimetric α ∈
    Set.Icc 0 (√(2 * Real.pi))⁻¹
    The Gaussian isoperimetric function takes values in
`[0, 1 / sqrt (2π)]`.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetric.lean
    complete
    theorem FABL.gaussianIsoperimetric_symm (α : ↑unitInterval) :
  FABL.gaussianIsoperimetric (unitInterval.symm α) =
    FABL.gaussianIsoperimetric α
    theorem FABL.gaussianIsoperimetric_symm
  (α : ↑unitInterval) :
  FABL.gaussianIsoperimetric
      (unitInterval.symm α) =
    FABL.gaussianIsoperimetric α
    The Gaussian isoperimetric function is symmetric about `1/2`.
Lemma5.4.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.
uses 1
Used by 2
Reverse dependency previews
Preview
Proposition 5.4.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-4supportfidelity-exact

Standard Gaussian Mills ratio. For every t>0, \frac{t}{1+t^2}\phi(t) \le\bar\Phi(t) \le\frac{\phi(t)}{t}. Consequently, \bar\Phi(t)\sim\frac{\phi(t)}{t} \qquad\text{as }t\to+\infty.

Lean code for Lemma5.4.6●5 theorems
  • theoremdefined in FABL/Chapter05/GaussianMillsRatio.lean
    complete
    theorem FABL.standardGaussianUpperTail_eq_integral_density (t : ℝ) :
  FABL.standardGaussianUpperTail t =
    ∫ (x : ℝ) in Set.Ioi t, ProbabilityTheory.gaussianPDFReal 0 1 x
    theorem FABL.standardGaussianUpperTail_eq_integral_density
  (t : ℝ) :
  FABL.standardGaussianUpperTail t =
    ∫ (x : ℝ) in Set.Ioi t,
      ProbabilityTheory.gaussianPDFReal 0
        1 x
    The standard Gaussian upper tail is the integral of its density over the
corresponding upper half-line.
  • theoremdefined in FABL/Chapter05/GaussianMillsRatio.lean
    complete
    theorem FABL.standardGaussianUpperTail_le_density_div {t : ℝ} (ht : 0 < t) :
  FABL.standardGaussianUpperTail t ≤
    ProbabilityTheory.gaussianPDFReal 0 1 t / t
    theorem FABL.standardGaussianUpperTail_le_density_div
  {t : ℝ} (ht : 0 < t) :
  FABL.standardGaussianUpperTail t ≤
    ProbabilityTheory.gaussianPDFReal 0 1
        t /
      t
    The elementary upper half of the standard Gaussian Mills-ratio estimate.
  • theoremdefined in FABL/Chapter05/GaussianMillsRatio.lean
    complete
    theorem FABL.density_mul_t_div_one_add_sq_le_standardGaussianUpperTail {t : ℝ}
  (ht : 0 < t) :
  t / (1 + t ^ 2) * ProbabilityTheory.gaussianPDFReal 0 1 t ≤
    FABL.standardGaussianUpperTail t
    theorem FABL.density_mul_t_div_one_add_sq_le_standardGaussianUpperTail
  {t : ℝ} (ht : 0 < t) :
  t / (1 + t ^ 2) *
      ProbabilityTheory.gaussianPDFReal 0
        1 t ≤
    FABL.standardGaussianUpperTail t
    The elementary lower half of the standard Gaussian Mills-ratio estimate.
  • theoremdefined in FABL/Chapter05/GaussianMillsRatio.lean
    complete
    theorem FABL.tendsto_standardGaussianUpperTail_div_density_div :
  Filter.Tendsto
    (fun t =>
      FABL.standardGaussianUpperTail t /
        (ProbabilityTheory.gaussianPDFReal 0 1 t / t))
    Filter.atTop (nhds 1)
    theorem FABL.tendsto_standardGaussianUpperTail_div_density_div :
  Filter.Tendsto
    (fun t =>
      FABL.standardGaussianUpperTail t /
        (ProbabilityTheory.gaussianPDFReal
            0 1 t /
          t))
    Filter.atTop (nhds 1)
    The standard Gaussian Mills ratio tends to one at positive infinity.
  • theoremdefined in FABL/Chapter05/GaussianMillsRatio.lean
    complete
    theorem FABL.standardGaussianUpperTail_isEquivalent_density_div :
  Asymptotics.IsEquivalent Filter.atTop FABL.standardGaussianUpperTail
    fun t => ProbabilityTheory.gaussianPDFReal 0 1 t / t
    theorem FABL.standardGaussianUpperTail_isEquivalent_density_div :
  Asymptotics.IsEquivalent Filter.atTop
    FABL.standardGaussianUpperTail
    fun t =>
    ProbabilityTheory.gaussianPDFReal 0 1
        t /
      t
    The standard Gaussian upper tail is asymptotic to its density divided by
the threshold.
Proposition5.4.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.
Statement uses 2
Statement dependency previews
Preview
Definition 5.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-4fidelity-exact

Proposition 5.27. As \alpha\to0^+, the Gaussian isoperimetric function satisfies U(\alpha) \sim \alpha\sqrt{2\ln(1/\alpha)}. Here \ln denotes the natural logarithm.

Lean code for Proposition5.4.7●6 theorems
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetricAsymptotics.lean
    complete
    theorem FABL.tendsto_standardGaussianUpperQuantile_atBot :
  Filter.Tendsto FABL.standardGaussianUpperQuantile Filter.atBot
    Filter.atTop
    theorem FABL.tendsto_standardGaussianUpperQuantile_atBot :
  Filter.Tendsto
    FABL.standardGaussianUpperQuantile
    Filter.atBot Filter.atTop
    The standard Gaussian upper quantile tends to positive infinity as its
open-unit probability tends to zero.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetricAsymptotics.lean
    complete
    theorem FABL.log_inv_standardGaussianUpperTail_isEquivalent_sq :
  Asymptotics.IsEquivalent Filter.atTop
    (fun t => Real.log (1 / FABL.standardGaussianUpperTail t)) fun t =>
    t ^ 2 / 2
    theorem FABL.log_inv_standardGaussianUpperTail_isEquivalent_sq :
  Asymptotics.IsEquivalent Filter.atTop
    (fun t =>
      Real.log
        (1 /
          FABL.standardGaussianUpperTail
            t))
    fun t => t ^ 2 / 2
    On the Gaussian upper-tail scale,
`log (1 / barPhi(t))` is asymptotic to `t² / 2`.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetricAsymptotics.lean
    complete
    theorem FABL.tendsto_sqrt_two_mul_log_inv_standardGaussianUpperTail_div :
  Filter.Tendsto
    (fun t =>
      √(2 * Real.log (1 / FABL.standardGaussianUpperTail t)) / t)
    Filter.atTop (nhds 1)
    theorem FABL.tendsto_sqrt_two_mul_log_inv_standardGaussianUpperTail_div :
  Filter.Tendsto
    (fun t =>
      √(2 *
            Real.log
              (1 /
                FABL.standardGaussianUpperTail
                  t)) /
        t)
    Filter.atTop (nhds 1)
    The logarithmic upper-tail scale recovers the Gaussian threshold:
`sqrt (2 log (1 / barPhi(t))) / t` tends to one.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetricAsymptotics.lean
    complete
    theorem FABL.standardGaussianUpperQuantile_isEquivalent_sqrt_log_inv :
  Asymptotics.IsEquivalent Filter.atBot
    FABL.standardGaussianUpperQuantile fun α => √(2 * Real.log (1 / ↑α))
    theorem FABL.standardGaussianUpperQuantile_isEquivalent_sqrt_log_inv :
  Asymptotics.IsEquivalent Filter.atBot
    FABL.standardGaussianUpperQuantile
    fun α => √(2 * Real.log (1 / ↑α))
    On the open probability interval, the upper quantile is asymptotic to
`sqrt (2 log (1 / α))` as `α` tends to zero.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetricAsymptotics.lean
    complete
    theorem FABL.gaussianIsoperimetric_isEquivalent_probability_mul_quantile :
  Asymptotics.IsEquivalent Filter.atBot
    (fun α => FABL.gaussianIsoperimetric ⟨↑α, ⋯⟩) fun α =>
    ↑α * FABL.standardGaussianUpperQuantile α
    theorem FABL.gaussianIsoperimetric_isEquivalent_probability_mul_quantile :
  Asymptotics.IsEquivalent Filter.atBot
    (fun α =>
      FABL.gaussianIsoperimetric ⟨↑α, ⋯⟩)
    fun α =>
    ↑α *
      FABL.standardGaussianUpperQuantile α
    Mills' ratio gives the first factorization in Proposition 5.27:
`U(α)` is asymptotic to `α` times its upper quantile.
  • theoremdefined in FABL/Chapter05/GaussianIsoperimetricAsymptotics.lean
    complete
    theorem FABL.gaussianIsoperimetric_isEquivalent_atBot :
  Asymptotics.IsEquivalent Filter.atBot
    (fun α => FABL.gaussianIsoperimetric ⟨↑α, ⋯⟩) fun α =>
    ↑α * √(2 * Real.log (1 / ↑α))
    theorem FABL.gaussianIsoperimetric_isEquivalent_atBot :
  Asymptotics.IsEquivalent Filter.atBot
    (fun α =>
      FABL.gaussianIsoperimetric ⟨↑α, ⋯⟩)
    fun α => ↑α * √(2 * Real.log (1 / ↑α))
    Proposition 5.27: on the natural open probability domain, where `atBot`
means `α → 0⁺`, the Gaussian isoperimetric function satisfies
`U(α) ~ α sqrt (2 log (1 / α))`.
Lemma5.4.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 1used by 1✓L∃∀N
Tagssection-5-4fidelity-exact

Lemma 5.31. Let \ell(x)=a_1x_1+\cdots+a_nx_n, \qquad \sum_{i=1}^n a_i^2=1. For every s\ge1, \mathbb E\!\left[ 1\{|\ell(x)|>s\}\,|\ell(x)| \right] \le (2s+2)\exp(-s^2/2).

Lean code for Lemma5.4.8●1 theorem
  • theoremdefined in FABL/Chapter05/LevelOneInequality.lean
    complete
    theorem FABL.expect_abs_linearForm_indicator_gt_le {n : ℕ} (a : Fin n → ℝ)
  (hnormalized : ∑ i, a i ^ 2 = 1) {s : ℝ} (hs : 1 ≤ s) :
  (Finset.univ.expect fun x =>
      if s < |FABL.linearForm a x| then |FABL.linearForm a x| else 0) ≤
    (2 * s + 2) * Real.exp (-s ^ 2 / 2)
    theorem FABL.expect_abs_linearForm_indicator_gt_le
  {n : ℕ} (a : Fin n → ℝ)
  (hnormalized : ∑ i, a i ^ 2 = 1) {s : ℝ}
  (hs : 1 ≤ s) :
  (Finset.univ.expect fun x =>
      if s < |FABL.linearForm a x| then
        |FABL.linearForm a x|
      else 0) ≤
    (2 * s + 2) * Real.exp (-s ^ 2 / 2)
    O'Donnell, Lemma 5.31: the absolute first moment of the part of a normalized
Rademacher linear form above `s ≥ 1` has the stated subgaussian bound.
Theorem5.4.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.
Statement uses 3
Statement dependency previews
Preview
Theorem 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 5.4.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-4fidelity-exact

Level-1 Inequality. There is a universal constant C such that if f:\{-1,1\}^n\to\{0,1\} has \mathbb E[f]=\alpha, \qquad 0<\alpha\le\frac12, then \mathbf W^1[f] \le C\alpha^2\log_2(1/\alpha). If \alpha=0, then \mathbf W^1[f]=0; for \alpha\ge1/2, the corresponding small-set estimate is obtained by replacing f with 1-f.

Lean code for Theorem5.4.9●2 theorems
  • theoremdefined in FABL/Chapter05/LevelOneInequality.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_eq_zero_of_zero_one_mean_eq_zero {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (hvalues : ∀ (x : FABL.SignCube n), f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = 0) : FABL.fourierWeightAtLevel 1 f = 0
    theorem FABL.fourierWeightAtLevel_one_eq_zero_of_zero_one_mean_eq_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x = 0 ∨ f x = 1)
  (hmean : FABL.mean f = 0) :
  FABL.fourierWeightAtLevel 1 f = 0
    The zero-density case of the Level-1 Inequality: a `{0,1}`-valued
function of uniform mean zero has no level-one Fourier weight.
  • theoremdefined in FABL/Chapter05/LevelOneInequality.lean
    complete
    theorem FABL.exists_levelOneInequality_constant :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (f : FABL.SignCube n → ℝ) {α : ℝ},
        (∀ (x : FABL.SignCube n), f x = 0 ∨ f x = 1) →
          FABL.mean f = α →
            0 < α →
              α ≤ 1 / 2 →
                FABL.fourierWeightAtLevel 1 f ≤
                  C * α ^ 2 * Real.logb 2 (1 / α)
    theorem FABL.exists_levelOneInequality_constant :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (f : FABL.SignCube n → ℝ)
        {α : ℝ},
        (∀ (x : FABL.SignCube n),
            f x = 0 ∨ f x = 1) →
          FABL.mean f = α →
            0 < α →
              α ≤ 1 / 2 →
                FABL.fourierWeightAtLevel
                    1 f ≤
                  C * α ^ 2 *
                    Real.logb 2 (1 / α)
    O'Donnell's Level-1 Inequality: the level-one Fourier weight of a
`{0,1}`-valued function of density `0 < α ≤ 1/2` is at most a universal
constant times `α² log₂(1/α)`.
Lemma5.4.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 1used by 1✓L∃∀N
Tagssection-5-4erratumfidelity-corrected-false-printed-codomain

Remark 5.28 (sharp Level-1 Inequality). The Level-1 bound has the sharp form \mathbf W^1[f]\le2\alpha^2\ln(1/\alpha). More generally, this holds for every f:\{-1,1\}^n\to[0,1] with \alpha=\mathbb E[f], \qquad 0<\alpha\le\frac12. For \alpha=0 the conclusion is \mathbf W^1[f]=0. In particular, Hamming balls are asymptotic maximizers of degree-1 Fourier weight among sets whose volume \alpha tends to 0. Here \ln is the natural logarithm.

The printed signed generalization is false. Already for f(x_1,x_2)=(x_1+x_2)/2, one has \mathbb E[|f|]=1/2 and \mathbf W^1[f]=1/2, whereas the displayed right-hand side is (\ln 2)/2<1/2.

Lean code for Lemma5.4.10●7 declarations
  • theoremdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    theorem FABL.sharpLevelOneInequality_eq_zero {n : ℕ} (f : FABL.SignCube n → ℝ)
  (hvalues : ∀ (x : FABL.SignCube n), f x ∈ Set.Icc 0 1)
  (hmean : FABL.mean f = 0) : FABL.fourierWeightAtLevel 1 f = 0
    theorem FABL.sharpLevelOneInequality_eq_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x ∈ Set.Icc 0 1)
  (hmean : FABL.mean f = 0) :
  FABL.fourierWeightAtLevel 1 f = 0
    The zero-density case of the sharp Level-1 inequality.
  • theoremdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    theorem FABL.sharpLevelOneInequality {n : ℕ} (f : FABL.SignCube n → ℝ) {α : ℝ}
  (hvalues : ∀ (x : FABL.SignCube n), f x ∈ Set.Icc 0 1)
  (hmean : FABL.mean f = α) (hα : 0 < α) (_hαhalf : α ≤ 1 / 2) :
  FABL.fourierWeightAtLevel 1 f ≤ 2 * α ^ 2 * Real.log (1 / α)
    theorem FABL.sharpLevelOneInequality {n : ℕ}
  (f : FABL.SignCube n → ℝ) {α : ℝ}
  (hvalues :
    ∀ (x : FABL.SignCube n),
      f x ∈ Set.Icc 0 1)
  (hmean : FABL.mean f = α) (hα : 0 < α)
  (_hαhalf : α ≤ 1 / 2) :
  FABL.fourierWeightAtLevel 1 f ≤
    2 * α ^ 2 * Real.log (1 / α)
    The intended sharp form of Remark 5.28 for a `[0,1]`-valued function.
  • defdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    def FABL.sharpLevelOneSignedCounterexample : FABL.SignCube 2 → ℝ
    def FABL.sharpLevelOneSignedCounterexample :
  FABL.SignCube 2 → ℝ
    The two-dimensional signed function witnessing the erratum in Remark 5.28.
  • theoremdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    theorem FABL.sharpLevelOneSignedCounterexample_mem_Icc (x : FABL.SignCube 2) :
  FABL.sharpLevelOneSignedCounterexample x ∈ Set.Icc (-1) 1
    theorem FABL.sharpLevelOneSignedCounterexample_mem_Icc
  (x : FABL.SignCube 2) :
  FABL.sharpLevelOneSignedCounterexample
      x ∈
    Set.Icc (-1) 1
  • theoremdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    theorem FABL.mean_abs_sharpLevelOneSignedCounterexample :
  (FABL.mean fun x => |FABL.sharpLevelOneSignedCounterexample x|) =
    1 / 2
    theorem FABL.mean_abs_sharpLevelOneSignedCounterexample :
  (FABL.mean fun x =>
      |FABL.sharpLevelOneSignedCounterexample
          x|) =
    1 / 2
  • theoremdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_sharpLevelOneSignedCounterexample :
  FABL.fourierWeightAtLevel 1 FABL.sharpLevelOneSignedCounterexample =
    1 / 2
    theorem FABL.fourierWeightAtLevel_one_sharpLevelOneSignedCounterexample :
  FABL.fourierWeightAtLevel 1
      FABL.sharpLevelOneSignedCounterexample =
    1 / 2
  • theoremdefined in FABL/Chapter05/SharpLevelOneInequality.lean
    complete
    theorem FABL.not_sharpLevelOneInequality_signed :
  ¬∀ {n : ℕ} (f : FABL.SignCube n → ℝ) {α : ℝ},
      (∀ (x : FABL.SignCube n), |f x| ≤ 1) →
        (FABL.mean fun x => |f x|) = α →
          0 < α →
            α ≤ 1 / 2 →
              FABL.fourierWeightAtLevel 1 f ≤
                2 * α ^ 2 * Real.log (1 / α)
    theorem FABL.not_sharpLevelOneInequality_signed :
  ¬∀ {n : ℕ} (f : FABL.SignCube n → ℝ)
      {α : ℝ},
      (∀ (x : FABL.SignCube n),
          |f x| ≤ 1) →
        (FABL.mean fun x => |f x|) = α →
          0 < α →
            α ≤ 1 / 2 →
              FABL.fourierWeightAtLevel 1
                  f ≤
                2 * α ^ 2 *
                  Real.log (1 / α)
    The signed generalization printed in Remark 5.28 is false.
Lemma5.4.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.
uses 0used by 0XL∃∀N
Tagssection-5-4nondependencybibliographic

Remark 5.29. The name “Level-1 Inequality” is not standard. In additive combinatorics the result is called Chang's Inequality. The terminology used here anticipates the Level-k Inequalities of Chapter 9.5.

Theorem5.4.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.
Statement uses 6
Statement dependency previews
Preview
Theorem 1.4.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-5-4fidelity-exact

The 2/\pi Theorem. There is a universal constant C such that the following holds. Let 0<\epsilon\le1 and let f:\{-1,1\}^n\to\{-1,1\} satisfy |\widehat f(\{i\})|\le\epsilon \qquad\text{for every }i\in[n]. Then \mathbf W^1[f]\le\frac2\pi+C\epsilon. \tag{5.16} Furthermore, if \mathbf W^1[f]\ge\frac2\pi-\epsilon, then \Pr_x\!\left[ f(x)\ne\operatorname{sgn}\bigl(f^{=1}(x)\bigr) \right] \le C\sqrt\epsilon, where f^{=1}(x)=\sum_{i=1}^n\widehat f(\{i\})x_i. Thus a near-extremizer is O(\sqrt\epsilon)-close to the linear threshold function \operatorname{sgn}(f^{=1}).

Lean code for Theorem5.4.12●1 theorem
  • theoremdefined in FABL/Chapter05/TwoDivPi.lean
    complete
    theorem FABL.exists_two_div_pi_constant :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ} (f : FABL.BooleanFunction n) {ε : ℝ},
        0 < ε →
          ε ≤ 1 →
            (∀ (i : Fin n), |FABL.fourierCoeff f.toReal {i}| ≤ ε) →
              FABL.fourierWeightAtLevel 1 f.toReal ≤
                  2 / Real.pi + C * ε ∧
                (2 / Real.pi - ε ≤
                    FABL.fourierWeightAtLevel 1 f.toReal →
                  (FABL.relativeHammingDist f fun x =>
                      FABL.thresholdSign
                        (FABL.degreePart 1 f.toReal x)) ≤
                    C * √ε)
    theorem FABL.exists_two_div_pi_constant :
  ∃ C,
    0 < C ∧
      ∀ {n : ℕ}
        (f : FABL.BooleanFunction n)
        {ε : ℝ},
        0 < ε →
          ε ≤ 1 →
            (∀ (i : Fin n),
                |FABL.fourierCoeff
                      f.toReal {i}| ≤
                  ε) →
              FABL.fourierWeightAtLevel 1
                    f.toReal ≤
                  2 / Real.pi + C * ε ∧
                (2 / Real.pi - ε ≤
                    FABL.fourierWeightAtLevel
                      1 f.toReal →
                  (FABL.relativeHammingDist
                      f fun x =>
                      FABL.thresholdSign
                        (FABL.degreePart 1
                          f.toReal x)) ≤
                    C * √ε)
    O'Donnell's 2/pi Theorem: regular Boolean functions have level-one weight at most
`2/pi + O(ε)`, and every near-extremizer is `O(sqrt ε)`-close to the sign of its
degree-one Fourier projection.
Lemma5.4.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.
uses 0used by 0XL∃∀N
Tagssection-5-4nondependencyexplanatory

Remark 5.30. For an unbiased Boolean function, \operatorname{Stab}_\rho[f] =\rho\mathbf W^1[f]+O(\rho^2), \qquad \frac2\pi\arcsin\rho =\frac2\pi\rho+O(\rho^3) as \rho\to0^+. Hence the 2/\pi Theorem is the \rho\to0^+ limiting case of the Majority Is Stablest Theorem.

Lemma5.4.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 2
Statement dependency previews
Preview
Definition 1.4.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-4supportfidelity-exact

Exercise 5.37 (nearly constant functions). Let f:\{-1,1\}^n\to\{-1,1\} satisfy |\mathbb E[f]|\ge1-\delta\ge0. Choose the sign so that g=\frac{1\mp f}{2} has mean \alpha\le\delta/2. Then \mathbf W^1[f]=4\mathbf W^1[g]. Applying the sharp Level-1 Inequality and converting the natural logarithm to the book's base-2 logarithm gives \mathbf W^1[f] \le4\delta^2\log_2(2/\delta). The case \delta=0 is interpreted by the conclusion \mathbf W^1[f]=0.

Lean code for Lemma5.4.14●7 declarations
  • defdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    def FABL.nearlyConstantMinorityIndicator {n : ℕ}
  (f : FABL.BooleanFunction n) : FABL.SignCube n → ℝ
    def FABL.nearlyConstantMinorityIndicator
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.SignCube n → ℝ
    The indicator of the minority output value, with the nearer constant sign
chosen from the sign of the mean.
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.nearlyConstantMinorityIndicator_mem_Icc {n : ℕ}
  (f : FABL.BooleanFunction n) (x : FABL.SignCube n) :
  FABL.nearlyConstantMinorityIndicator f x ∈ Set.Icc 0 1
    theorem FABL.nearlyConstantMinorityIndicator_mem_Icc
  {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) :
  FABL.nearlyConstantMinorityIndicator f
      x ∈
    Set.Icc 0 1
    The minority-value indicator is `[0,1]`-valued.
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.mean_nearlyConstantMinorityIndicator {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.mean (FABL.nearlyConstantMinorityIndicator f) =
    (1 - |FABL.mean f.toReal|) / 2
    theorem FABL.mean_nearlyConstantMinorityIndicator
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.mean
      (FABL.nearlyConstantMinorityIndicator
        f) =
    (1 - |FABL.mean f.toReal|) / 2
    The chosen indicator has mean `(1 - |𝔼[f]|) / 2`.
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.mean_nearlyConstantMinorityIndicator_nonneg {n : ℕ}
  (f : FABL.BooleanFunction n) :
  0 ≤ FABL.mean (FABL.nearlyConstantMinorityIndicator f)
    theorem FABL.mean_nearlyConstantMinorityIndicator_nonneg
  {n : ℕ} (f : FABL.BooleanFunction n) :
  0 ≤
    FABL.mean
      (FABL.nearlyConstantMinorityIndicator
        f)
    The chosen minority-value indicator has nonnegative mean.
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.mean_nearlyConstantMinorityIndicator_le {n : ℕ}
  (f : FABL.BooleanFunction n) {δ : ℝ}
  (hmean : 1 - δ ≤ |FABL.mean f.toReal|) :
  FABL.mean (FABL.nearlyConstantMinorityIndicator f) ≤ δ / 2
    theorem FABL.mean_nearlyConstantMinorityIndicator_le
  {n : ℕ} (f : FABL.BooleanFunction n)
  {δ : ℝ}
  (hmean : 1 - δ ≤ |FABL.mean f.toReal|) :
  FABL.mean
      (FABL.nearlyConstantMinorityIndicator
        f) ≤
    δ / 2
    Under the nearly constant hypothesis, the minority-value indicator has
mean at most `δ / 2`.
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.fourierCoeff_nearlyConstantMinorityIndicator_singleton {n : ℕ}
  (f : FABL.BooleanFunction n) (i : Fin n) :
  FABL.fourierCoeff (FABL.nearlyConstantMinorityIndicator f) {i} =
    if 0 ≤ FABL.mean f.toReal then -FABL.fourierCoeff f.toReal {i} / 2
    else FABL.fourierCoeff f.toReal {i} / 2
    theorem FABL.fourierCoeff_nearlyConstantMinorityIndicator_singleton
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  FABL.fourierCoeff
      (FABL.nearlyConstantMinorityIndicator
        f)
      {i} =
    if 0 ≤ FABL.mean f.toReal then
      -FABL.fourierCoeff f.toReal {i} / 2
    else
      FABL.fourierCoeff f.toReal {i} / 2
    Singleton Fourier coefficients of the minority indicator are the
corresponding coefficients of `f`, scaled by one half and possibly negated.
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_eq_four_mul_nearlyConstantMinorityIndicator
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.fourierWeightAtLevel 1 f.toReal =
    4 *
      FABL.fourierWeightAtLevel 1
        (FABL.nearlyConstantMinorityIndicator f)
    theorem FABL.fourierWeightAtLevel_one_eq_four_mul_nearlyConstantMinorityIndicator
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.fourierWeightAtLevel 1 f.toReal =
    4 *
      FABL.fourierWeightAtLevel 1
        (FABL.nearlyConstantMinorityIndicator
          f)
    Passing to the minority indicator divides Level-1 Fourier weight by four.
Corollary5.4.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 1✓L∃∀N
Tagssection-5-4fidelity-exact

Corollary 5.32. Let f:\{-1,1\}^n\to\{-1,1\} satisfy |\mathbb E[f]|\ge1-\delta\ge0. Then \mathbf W^1[f]\le4\delta^2\log_2(2/\delta). For \delta=0, the right-hand side is understood as 0.

Lean code for Corollary5.4.15●1 theorem
  • theoremdefined in FABL/Chapter05/NearlyConstantLevelOne.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_le_of_abs_mean_ge {n : ℕ}
  (f : FABL.BooleanFunction n) {δ : ℝ}
  (hmean : 1 - δ ≤ |FABL.mean f.toReal|) (hδ : 0 ≤ 1 - δ) :
  FABL.fourierWeightAtLevel 1 f.toReal ≤ 4 * δ ^ 2 * Real.logb 2 (2 / δ)
    theorem FABL.fourierWeightAtLevel_one_le_of_abs_mean_ge
  {n : ℕ} (f : FABL.BooleanFunction n)
  {δ : ℝ}
  (hmean : 1 - δ ≤ |FABL.mean f.toReal|)
  (hδ : 0 ≤ 1 - δ) :
  FABL.fourierWeightAtLevel 1 f.toReal ≤
    4 * δ ^ 2 * Real.logb 2 (2 / δ)
    Corollary 5.32: a Boolean function whose mean is within `δ` of a
constant has Level-1 weight at most `4 δ² log₂(2 / δ)`.
Lemma5.4.16
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 1✓L∃∀N
Tagssection-5-4supportfidelity-exact

Exercise 2.49 (balanced lift for FKN). Suppose f:\{-1,1\}^n\to\{-1,1\} satisfies \mathbf W^{\le1}[f]\ge1-\delta. Define g:\{-1,1\}^{n+1}\to\{-1,1\} by g(x_0,x)=x_0f(x_0x), where x_0x=(x_0x_1,\ldots,x_0x_n). Then \mathbb E[g]=0, \qquad \mathbf W^1[g]=\mathbf W^{\le1}[f]. Applying the balanced FKN Theorem to g and translating its dictator or negated-dictator conclusion back to f shows that f is O(\delta)-close to a 1-junta. The same construction preserves the chosen FKN closeness constant.

Lean code for Lemma5.4.16●6 declarations
  • defdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    def FABL.balancedFKNLift {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.BooleanFunction (n + 1)
    def FABL.balancedFKNLift {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.BooleanFunction (n + 1)
    O'Donnell, Exercise 2.49: the balanced lift
`g(x₀, x) = x₀ f(x₀ x)` of a Boolean function.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.balancedFKNLift_fin_cons_one {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) : FABL.balancedFKNLift f (Fin.cons 1 x) = f x
    theorem FABL.balancedFKNLift_fin_cons_one {n : ℕ}
  (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) :
  FABL.balancedFKNLift f (Fin.cons 1 x) =
    f x
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.balancedFKNLift_fin_cons_neg_one {n : ℕ}
  (f : FABL.BooleanFunction n) (x : FABL.SignCube n) :
  FABL.balancedFKNLift f (Fin.cons (-1) x) = -f (-x)
    theorem FABL.balancedFKNLift_fin_cons_neg_one
  {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) :
  FABL.balancedFKNLift f
      (Fin.cons (-1) x) =
    -f (-x)
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.mean_balancedFKNLift {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.mean (FABL.balancedFKNLift f).toReal = 0
    theorem FABL.mean_balancedFKNLift {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.mean
      (FABL.balancedFKNLift f).toReal =
    0
    Exercise 2.49: the balanced lift has mean zero.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_balancedFKNLift {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.fourierWeightAtLevel 1 (FABL.balancedFKNLift f).toReal =
    FABL.fourierWeightAtMost 1 f.toReal
    theorem FABL.fourierWeightAtLevel_one_balancedFKNLift
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.fourierWeightAtLevel 1
      (FABL.balancedFKNLift f).toReal =
    FABL.fourierWeightAtMost 1 f.toReal
    Exercise 2.49: the level-one Fourier weight of the balanced lift is the
degree-at-most-one Fourier weight of the original function.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.exists_isKJunta_one_relativeHammingDist_le_of_fourierWeightAtMost_one
  {n : ℕ} (f : FABL.BooleanFunction n) (δ : ℝ) (hδ₀ : 0 ≤ δ)
  (hδ : δ ≤ 1 / 1600)
  (hweight : 1 - δ ≤ FABL.fourierWeightAtMost 1 f.toReal) :
  ∃ g, FABL.IsKJunta g 1 ∧ FABL.relativeHammingDist f g ≤ 1601 * δ
    theorem FABL.exists_isKJunta_one_relativeHammingDist_le_of_fourierWeightAtMost_one
  {n : ℕ} (f : FABL.BooleanFunction n)
  (δ : ℝ) (hδ₀ : 0 ≤ δ)
  (hδ : δ ≤ 1 / 1600)
  (hweight :
    1 - δ ≤
      FABL.fourierWeightAtMost 1
        f.toReal) :
  ∃ g,
    FABL.IsKJunta g 1 ∧
      FABL.relativeHammingDist f g ≤
        1601 * δ
    Exercise 2.49: applying FKN to the balanced lift transfers its unchanged
`1601 · δ` closeness bound to a one-junta for the original function.
Lemma5.4.17
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-4supportfidelity-exact

Exercise 5.38 (numerical details for Theorem 5.33). Let C\ge1, \delta>0, and \eta =16C^2\delta^2 \max\!\left(\log_2\!\left(\frac1{C\delta}\right),1\right). Complete the two numerical steps in the proof:

(a) If \delta>1/(10C), then 1-\frac\delta2-2\eta<0.

(b) If 0<\delta\le1/(10C), then 1-\delta -16C^2\delta^2\log_2\!\left(\frac1{C\delta}\right) \ge \left(1-\frac\delta2-2\eta\right)^2. Consequently, any nonnegative number whose square is at least the left-hand side in (b) is at least 1-\delta/2-2\eta.

Lean code for Lemma5.4.17●5 declarations
  • defdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    def FABL.fknImprovementEta (C δ : ℝ) : ℝ
    def FABL.fknImprovementEta (C δ : ℝ) : ℝ
    The second-order error term in O'Donnell's improved FKN argument.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.exercise5_38a {C δ : ℝ} (hC : 1 ≤ C) (hδ : 0 < δ)
  (hlarge : 1 / (10 * C) < δ) :
  1 - δ / 2 - 2 * FABL.fknImprovementEta C δ < 0
    theorem FABL.exercise5_38a {C δ : ℝ} (hC : 1 ≤ C)
  (hδ : 0 < δ)
  (hlarge : 1 / (10 * C) < δ) :
  1 - δ / 2 -
      2 * FABL.fknImprovementEta C δ <
    0
    O'Donnell, Exercise 5.38(a): outside the small-error regime, the proposed
degree-one lower bound is already negative.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.exercise5_38b {C δ : ℝ} (hC : 1 ≤ C) (hδ : 0 < δ)
  (hsmall : δ ≤ 1 / (10 * C)) :
  1 - δ - 16 * C ^ 2 * δ ^ 2 * Real.logb 2 (1 / (C * δ)) ≥
    (1 - δ / 2 - 2 * FABL.fknImprovementEta C δ) ^ 2
    theorem FABL.exercise5_38b {C δ : ℝ} (hC : 1 ≤ C)
  (hδ : 0 < δ)
  (hsmall : δ ≤ 1 / (10 * C)) :
  1 - δ -
      16 * C ^ 2 * δ ^ 2 *
        Real.logb 2 (1 / (C * δ)) ≥
    (1 - δ / 2 -
        2 * FABL.fknImprovementEta C δ) ^
      2
    O'Donnell, Exercise 5.38(b): the numerical square comparison in the
small-error regime.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.exercise5_38_nonnegative_lower_bound {C δ z : ℝ} (hC : 1 ≤ C)
  (hδ : 0 < δ) (hsmall : δ ≤ 1 / (10 * C)) (hz : 0 ≤ z)
  (hzsq :
    1 - δ - 16 * C ^ 2 * δ ^ 2 * Real.logb 2 (1 / (C * δ)) ≤ z ^ 2) :
  1 - δ / 2 - 2 * FABL.fknImprovementEta C δ ≤ z
    theorem FABL.exercise5_38_nonnegative_lower_bound
  {C δ z : ℝ} (hC : 1 ≤ C) (hδ : 0 < δ)
  (hsmall : δ ≤ 1 / (10 * C)) (hz : 0 ≤ z)
  (hzsq :
    1 - δ -
        16 * C ^ 2 * δ ^ 2 *
          Real.logb 2 (1 / (C * δ)) ≤
      z ^ 2) :
  1 - δ / 2 -
      2 * FABL.fknImprovementEta C δ ≤
    z
    Exercise 5.38: a nonnegative quantity with square at least the numerical
left-hand side is at least the improved FKN target.
  • theoremdefined in FABL/Chapter05/FKNImprovement.lean
    complete
    theorem FABL.exercise5_38_sqrt_lower_bound {C δ A : ℝ} (hC : 1 ≤ C) (hδ : 0 < δ)
  (hsmall : δ ≤ 1 / (10 * C)) (hA : 0 ≤ A)
  (hbound :
    1 - δ - 16 * C ^ 2 * δ ^ 2 * Real.logb 2 (1 / (C * δ)) ≤ A) :
  1 - δ / 2 - 2 * FABL.fknImprovementEta C δ ≤ √A
    theorem FABL.exercise5_38_sqrt_lower_bound
  {C δ A : ℝ} (hC : 1 ≤ C) (hδ : 0 < δ)
  (hsmall : δ ≤ 1 / (10 * C)) (hA : 0 ≤ A)
  (hbound :
    1 - δ -
        16 * C ^ 2 * δ ^ 2 *
          Real.logb 2 (1 / (C * δ)) ≤
      A) :
  1 - δ / 2 -
      2 * FABL.fknImprovementEta C δ ≤
    √A
    Exercise 5.38: square-root form of the numerical lower bound used in
Theorem 5.33.
Theorem5.4.18
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
Theorem 2.5.13
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-5-4fidelity-explicit-positive-arity

Theorem 5.33. Let n\ge1. Suppose the FKN Theorem holds with closeness bound C\delta, where C\ge1 is a universal constant: whenever f:\{-1,1\}^n\to\{-1,1\} satisfies \mathbf W^1[f]\ge1-\delta\ge0, the function f is C\delta-close to a dictator or negated dictator. Then the same conclusion holds with the improved bound \frac\delta4+\eta, \qquad \eta =16C^2\delta^2 \max\!\left(\log_2\!\left(\frac1{C\delta}\right),1\right). At \delta=0, this expression is understood by continuity as 0. Thus FKN admits the essentially optimal closeness bound \delta/4+O(\delta^2\log(1/\delta)).

Lean code for Theorem5.4.18●1 theorem
  • theoremdefined in FABL/Chapter05/ImprovedFKN.lean
    complete
    theorem FABL.improvedFKN (C : ℝ) (hC : 1 ≤ C)
  (hFKN :
    ∀ {m : ℕ},
      0 < m →
        ∀ (g : FABL.BooleanFunction m) (ε : ℝ),
          0 ≤ ε →
            0 ≤ 1 - ε →
              1 - ε ≤ FABL.fourierWeightAtLevel 1 g.toReal →
                ∃ i negated,
                  FABL.relativeHammingDist g
                      (FABL.signedDictator i negated) ≤
                    C * ε)
  {n : ℕ} (hn : 0 < n) (f : FABL.BooleanFunction n) (δ : ℝ) (hδ : 0 ≤ δ)
  (hδone : 0 ≤ 1 - δ)
  (hweight : 1 - δ ≤ FABL.fourierWeightAtLevel 1 f.toReal) :
  ∃ i negated,
    FABL.relativeHammingDist f (FABL.signedDictator i negated) ≤
      δ / 4 + FABL.fknImprovementEta C δ
    theorem FABL.improvedFKN (C : ℝ) (hC : 1 ≤ C)
  (hFKN :
    ∀ {m : ℕ},
      0 < m →
        ∀ (g : FABL.BooleanFunction m)
          (ε : ℝ),
          0 ≤ ε →
            0 ≤ 1 - ε →
              1 - ε ≤
                  FABL.fourierWeightAtLevel
                    1 g.toReal →
                ∃ i negated,
                  FABL.relativeHammingDist
                      g
                      (FABL.signedDictator
                        i negated) ≤
                    C * ε)
  {n : ℕ} (hn : 0 < n)
  (f : FABL.BooleanFunction n) (δ : ℝ)
  (hδ : 0 ≤ δ) (hδone : 0 ≤ 1 - δ)
  (hweight :
    1 - δ ≤
      FABL.fourierWeightAtLevel 1
        f.toReal) :
  ∃ i negated,
    FABL.relativeHammingDist f
        (FABL.signedDictator i negated) ≤
      δ / 4 + FABL.fknImprovementEta C δ
    O'Donnell, Theorem 5.33: any positive-arity FKN bound with universal
constant `C ≥ 1` self-improves to `δ / 4` plus the explicit second-order
term from Exercise 5.38.