Analysis of Boolean Functions in Lean

5.5. Highlight: Peres's Theorem and uniform noise stability🔗

Lemma5.5.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 2.2.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Lemma 5.5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-5supportfidelity-exact

Exercise 2.5 (unate functions). A Boolean function f:\{-1,1\}^n\to\{-1,1\} is unate in coordinate i if it is either monotone or antimonotone in that coordinate, and it is unate if this holds in every coordinate.

(a) For every i\in[n], |\widehat f(i)|\le\operatorname{Inf}_i[f], with equality if and only if f is unate in the ith direction.

(b) The total-influence conclusion of Theorem 2.33 extends from monotone to unate functions: every unate f satisfies \mathbf I[f]\le\mathbf I[\operatorname{Maj}_n].

Lean code for Lemma5.5.1●7 declarations
  • defdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    def FABL.IsMonotoneInCoordinate {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) : Prop
    def FABL.IsMonotoneInCoordinate {n : ℕ}
  (f : FABL.BooleanFunction n)
  (i : Fin n) : Prop
    A Boolean function is monotone in coordinate `i` when changing that coordinate from `-1`
to `1` cannot decrease its value.
  • defdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    def FABL.IsAntimonotoneInCoordinate {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) : Prop
    def FABL.IsAntimonotoneInCoordinate {n : ℕ}
  (f : FABL.BooleanFunction n)
  (i : Fin n) : Prop
    A Boolean function is antimonotone in coordinate `i` when changing that coordinate from `-1`
to `1` cannot increase its value.
  • defdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    def FABL.IsUnateInCoordinate {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) : Prop
    def FABL.IsUnateInCoordinate {n : ℕ}
  (f : FABL.BooleanFunction n)
  (i : Fin n) : Prop
    O'Donnell, Exercise 2.5: a Boolean function is unate in a coordinate when it is monotone or
antimonotone in that coordinate.
  • defdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    def FABL.IsUnate {n : ℕ} (f : FABL.BooleanFunction n) : Prop
    def FABL.IsUnate {n : ℕ}
  (f : FABL.BooleanFunction n) : Prop
    O'Donnell, Exercise 2.5: a Boolean function is unate when it is unate in every coordinate.
  • theoremdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    theorem FABL.abs_fourierCoeff_singleton_le_influence {n : ℕ}
  (f : FABL.BooleanFunction n) (i : Fin n) :
  |FABL.fourierCoeff f.toReal {i}| ≤ FABL.influence f.toReal i
    theorem FABL.abs_fourierCoeff_singleton_le_influence
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  |FABL.fourierCoeff f.toReal {i}| ≤
    FABL.influence f.toReal i
    O'Donnell, Exercise 2.5(a): a singleton Fourier coefficient is bounded in absolute value by
the corresponding coordinate influence.
  • theoremdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    theorem FABL.abs_fourierCoeff_singleton_eq_influence_iff_isUnateInCoordinate
  {n : ℕ} (f : FABL.BooleanFunction n) (i : Fin n) :
  |FABL.fourierCoeff f.toReal {i}| = FABL.influence f.toReal i ↔
    FABL.IsUnateInCoordinate f i
    theorem FABL.abs_fourierCoeff_singleton_eq_influence_iff_isUnateInCoordinate
  {n : ℕ} (f : FABL.BooleanFunction n)
  (i : Fin n) :
  |FABL.fourierCoeff f.toReal {i}| =
      FABL.influence f.toReal i ↔
    FABL.IsUnateInCoordinate f i
    Equality in the singleton-coefficient influence bound holds exactly in the unate
directions.
  • theoremdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    theorem FABL.totalInfluence_toReal_le_majority_of_unate {n : ℕ}
  (f : FABL.BooleanFunction n) (hf : FABL.IsUnate f) :
  FABL.totalInfluence f.toReal ≤
    FABL.totalInfluence (FABL.majority n).toReal
    theorem FABL.totalInfluence_toReal_le_majority_of_unate
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsUnate f) :
  FABL.totalInfluence f.toReal ≤
    FABL.totalInfluence
      (FABL.majority n).toReal
    O'Donnell, Exercise 2.5(b): every unate Boolean function has total influence at most
majority's total influence.
Lemma5.5.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
Definition 2.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.5.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-5supportfidelity-exact

Exercise 2.6. Every linear threshold function is unate.

Lean code for Lemma5.5.2●1 theorem
  • theoremdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    theorem FABL.isUnate_of_isLinearThreshold {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f) : FABL.IsUnate f
    theorem FABL.isUnate_of_isLinearThreshold {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f) :
  FABL.IsUnate f
    O'Donnell, Exercise 2.6: every Boolean linear threshold function is unate.
Lemma5.5.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 4
Statement dependency previews
Preview
Theorem 1.4.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-5-5supportfidelity-exact

Exercise 2.23. If f:\{-1,1\}^n\to\{-1,1\} is monotone, then \mathbf I[f]\le\sqrt n. The same estimate holds for every unate Boolean function. The proof uses only Cauchy--Schwarz and Parseval's Theorem.

Lean code for Lemma5.5.3●1 theorem
  • theoremdefined in FABL/Chapter05/UnateFunctions.lean
    complete
    theorem FABL.totalInfluence_toReal_le_sqrt_card_of_unate {n : ℕ}
  (f : FABL.BooleanFunction n) (hf : FABL.IsUnate f) :
  FABL.totalInfluence f.toReal ≤ √↑n
    theorem FABL.totalInfluence_toReal_le_sqrt_card_of_unate
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsUnate f) :
  FABL.totalInfluence f.toReal ≤ √↑n
    O'Donnell, Exercise 2.23: every unate Boolean function on `n` variables has total influence
at most `√n`.
Lemma5.5.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 3
Statement dependency previews
Preview
Definition 2.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 5.5.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-5supportfidelity-exact

Exercise 2.43(a) (average influence). For n\ge1, define the average influence of f:\{-1,1\}^n\to\mathbb R by \mathbf E[f]=\frac1n\mathbf I[f]. If f is Boolean-valued, then \mathbf E[f] =\Pr_{\substack{x\sim\{-1,1\}^n\\ i\sim[n]}} [f(x)\ne f(x^{\oplus i})], and \frac{1-e^{-2}}2\mathbf E[f] \le\operatorname{NS}_{1/n}[f] \le\mathbf E[f].

Lean code for Lemma5.5.4●5 declarations
  • defdefined in FABL/Chapter05/AverageInfluence.lean
    complete
    def FABL.averageInfluence {n : ℕ} (f : FABL.SignCube n → ℝ) : ℝ
    def FABL.averageInfluence {n : ℕ}
  (f : FABL.SignCube n → ℝ) : ℝ
    O'Donnell, Exercise 2.43(a): average influence is total influence divided by the
dimension.
  • defdefined in FABL/Chapter05/AverageInfluence.lean
    complete
    def FABL.averageCoordinateFlipProbability {n : ℕ}
  (f : FABL.BooleanFunction n) : ℝ
    def FABL.averageCoordinateFlipProbability
  {n : ℕ} (f : FABL.BooleanFunction n) : ℝ
    The probability of a Boolean function changing after independently choosing a uniform input
and a uniform coordinate and flipping that coordinate.
  • theoremdefined in FABL/Chapter05/AverageInfluence.lean
    complete
    theorem FABL.averageInfluence_toReal_eq_averageCoordinateFlipProbability {n : ℕ}
  (f : FABL.BooleanFunction n) (_hn : 0 < n) :
  FABL.averageInfluence f.toReal =
    FABL.averageCoordinateFlipProbability f
    theorem FABL.averageInfluence_toReal_eq_averageCoordinateFlipProbability
  {n : ℕ} (f : FABL.BooleanFunction n)
  (_hn : 0 < n) :
  FABL.averageInfluence f.toReal =
    FABL.averageCoordinateFlipProbability
      f
    For positive dimension, average influence is the random-coordinate flip probability.
  • theoremdefined in FABL/Chapter05/AverageInfluence.lean
    complete
    theorem FABL.averageInfluence_mul_one_sub_exp_neg_two_div_two_le_noiseSensitivity
  {n : ℕ} (f : FABL.BooleanFunction n) (hn : 0 < n) :
  (1 - Real.exp (-2)) / 2 * FABL.averageInfluence f.toReal ≤
    FABL.noiseSensitivity (1 / ↑n) ⋯ f
    theorem FABL.averageInfluence_mul_one_sub_exp_neg_two_div_two_le_noiseSensitivity
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) :
  (1 - Real.exp (-2)) / 2 *
      FABL.averageInfluence f.toReal ≤
    FABL.noiseSensitivity (1 / ↑n) ⋯ f
    O'Donnell, Exercise 2.43(a), lower comparison at inverse dimension.
  • theoremdefined in FABL/Chapter05/AverageInfluence.lean
    complete
    theorem FABL.noiseSensitivity_inverse_dimension_le_averageInfluence {n : ℕ}
  (f : FABL.BooleanFunction n) (hn : 0 < n) :
  FABL.noiseSensitivity (1 / ↑n) ⋯ f ≤ FABL.averageInfluence f.toReal
    theorem FABL.noiseSensitivity_inverse_dimension_le_averageInfluence
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) :
  FABL.noiseSensitivity (1 / ↑n) ⋯ f ≤
    FABL.averageInfluence f.toReal
    O'Donnell, Exercise 2.43(a), upper comparison at inverse dimension.
Theorem5.5.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 3
Statement dependency previews
Preview
Lemma 5.5.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Lemma 5.5.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-5fidelity-explicit-universal-constant

Peres's Theorem. Every linear threshold function f:\{-1,1\}^n\to\{-1,1\} satisfies \operatorname{NS}_\delta[f]\le O(\sqrt\delta) \qquad (0<\delta\le1/2), with a universal implied constant independent of n and f.

Lean code for Theorem5.5.5●1 theorem
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.peresNoiseSensitivityBound {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤ √(3 / 2) * √↑δ
    theorem FABL.peresNoiseSensitivityBound {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    √(3 / 2) * √↑δ
    Peres's Theorem with the explicit universal constant from Remark 5.36.
Definition5.5.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 3
Reverse dependency previews
Preview
Theorem 5.5.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-5fidelity-exact

Definition 5.34. Let \mathcal B be a class of Boolean-valued functions. The class \mathcal B is uniformly noise-stable if there is a function \epsilon:[0,1/2]\to[0,1] such that \epsilon(\delta)\to0 as \delta\to0^+ and \operatorname{NS}_\delta[f]\le\epsilon(\delta) for every f\in\mathcal B and every \delta\in[0,1/2].

Lean code for Definition5.5.6●4 definitions
  • abbrevdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    abbrev FABL.BooleanClass : Type
    abbrev FABL.BooleanClass : Type
    A Boolean class contains functions across all finite input dimensions.
  • abbrevdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    abbrev FABL.HalfNoiseParameter : Set ℝ
    abbrev FABL.HalfNoiseParameter : Set ℝ
    The closed interval of noise parameters used in Definition 5.34.
  • abbrevdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    abbrev FABL.UnitProbability : Set ℝ
    abbrev FABL.UnitProbability : Set ℝ
    The closed unit interval of probability bounds used in Definition 5.34.
  • defdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    def FABL.IsUniformlyNoiseStable (B : FABL.BooleanClass) : Prop
    def FABL.IsUniformlyNoiseStable
  (B : FABL.BooleanClass) : Prop
    O'Donnell, Definition 5.34: one modulus controls the noise sensitivity of every member
of a Boolean class, uniformly over its input dimension, and tends to zero from the right.
Theorem5.5.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 3
Statement dependency previews
Preview
Proposition 2.4.13
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 4
Reverse dependency previews
Preview
Theorem 5.5.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-5-5fidelity-exact

Theorem 5.35. Let \delta\in(0,1/2], let A:\mathbb N^+\to\mathbb R, and let \mathcal B be a class of Boolean-valued functions closed under negating and identifying input variables. Suppose every f\in\mathcal B with domain \{-1,1\}^r satisfies \mathbf I[f]\le A(r). Then every f\in\mathcal B satisfies \operatorname{NS}_\delta[f]\le\frac1m A(m), \qquad m=\left\lfloor\frac1\delta\right\rfloor.

Lean code for Theorem5.5.7●7 declarations
  • defdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    def FABL.negateInputVariables {n : ℕ} (z : FABL.SignCube n)
  (f : FABL.BooleanFunction n) : FABL.BooleanFunction n
    def FABL.negateInputVariables {n : ℕ}
  (z : FABL.SignCube n)
  (f : FABL.BooleanFunction n) :
  FABL.BooleanFunction n
    Negate the input variables selected by a sign vector.
  • defdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    def FABL.identifyInputVariables {n m : ℕ} (π : Fin n → Fin m)
  (f : FABL.BooleanFunction n) : FABL.BooleanFunction m
    def FABL.identifyInputVariables {n m : ℕ}
  (π : Fin n → Fin m)
  (f : FABL.BooleanFunction n) :
  FABL.BooleanFunction m
    Identify the input variables of `f` according to a map from its old coordinates to the
new coordinates.
  • defdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    def FABL.IsClosedUnderNegatingInputVariables (B : FABL.BooleanClass) : Prop
    def FABL.IsClosedUnderNegatingInputVariables
  (B : FABL.BooleanClass) : Prop
    A Boolean class is closed under arbitrary negations of input variables.
  • defdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    def FABL.IsClosedUnderIdentifyingInputVariables (B : FABL.BooleanClass) :
  Prop
    def FABL.IsClosedUnderIdentifyingInputVariables
  (B : FABL.BooleanClass) : Prop
    A Boolean class is closed under arbitrary identifications of input variables.
  • abbrevdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    abbrev FABL.PositiveHalfNoiseParameter : Set ℝ
    abbrev FABL.PositiveHalfNoiseParameter : Set ℝ
    The positive noise-parameter interval used in Theorem 5.35.
  • defdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    def FABL.inverseNoiseFloor (δ : ↑FABL.PositiveHalfNoiseParameter) : ℕ+
    def FABL.inverseNoiseFloor
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  ℕ+
    The integer `m = ⌊1 / δ⌋` used in the random-partition bound.
  • theoremdefined in FABL/Chapter05/UniformNoiseStability.lean
    complete
    theorem FABL.noiseSensitivity_le_inverseNoiseFloor_totalInfluenceBound
  (B : FABL.BooleanClass)
  (hneg : FABL.IsClosedUnderNegatingInputVariables B)
  (hidentify : FABL.IsClosedUnderIdentifyingInputVariables B)
  (A : ℕ+ → ℝ)
  (hA : ∀ (r : ℕ+), ∀ g ∈ B ↑r, FABL.totalInfluence g.toReal ≤ A r)
  {n : ℕ} (f : FABL.BooleanFunction n) (hf : f ∈ B n)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    A (FABL.inverseNoiseFloor δ) / ↑↑(FABL.inverseNoiseFloor δ)
    theorem FABL.noiseSensitivity_le_inverseNoiseFloor_totalInfluenceBound
  (B : FABL.BooleanClass)
  (hneg :
    FABL.IsClosedUnderNegatingInputVariables
      B)
  (hidentify :
    FABL.IsClosedUnderIdentifyingInputVariables
      B)
  (A : ℕ+ → ℝ)
  (hA :
    ∀ (r : ℕ+),
      ∀ g ∈ B ↑r,
        FABL.totalInfluence g.toReal ≤
          A r)
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : f ∈ B n)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    A (FABL.inverseNoiseFloor δ) /
      ↑↑(FABL.inverseNoiseFloor δ)
    O'Donnell, Theorem 5.35: a dimension-wise total-influence bound controls noise
sensitivity at every positive noise rate through `m = ⌊1 / δ⌋`.
Lemma5.5.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.
Statement uses 3
Statement dependency previews
Preview
Lemma 2.3.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-5-5fidelity-exact

Remark 5.36. The proof of Peres's Theorem gives the explicit bound \operatorname{NS}_\delta[f] \le\sqrt{\frac1{\lfloor1/\delta\rfloor}} \le\sqrt{\frac32}\,\sqrt\delta \qquad (0<\delta\le1/2), and its first expression is \sqrt\delta+O(\delta^{3/2}) as \delta\to0^+. Replacing Exercise 2.23 by the sharper unate bound from Theorem 2.33 yields \operatorname{NS}_\delta[f] \le\sqrt{\frac2\pi}\,\sqrt\delta+O(\delta^{3/2}).

Lean code for Lemma5.5.8●7 declarations
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.noiseSensitivity_le_sqrt_inverseNoiseFloor_of_isLinearThreshold
  {n : ℕ} (f : FABL.BooleanFunction n) (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤ √(1 / ↑↑(FABL.inverseNoiseFloor δ))
    theorem FABL.noiseSensitivity_le_sqrt_inverseNoiseFloor_of_isLinearThreshold
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    √(1 / ↑↑(FABL.inverseNoiseFloor δ))
    Peres's random-partition argument before estimating the floor: the noise sensitivity of a
linear threshold function is at most `sqrt (1 / floor (1 / δ))`.
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.sqrt_inverseNoiseFloor_le_sqrt_three_halves_mul_sqrt
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  √(1 / ↑↑(FABL.inverseNoiseFloor δ)) ≤ √(3 / 2) * √↑δ
    theorem FABL.sqrt_inverseNoiseFloor_le_sqrt_three_halves_mul_sqrt
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  √(1 / ↑↑(FABL.inverseNoiseFloor δ)) ≤
    √(3 / 2) * √↑δ
    The floor estimate in Remark 5.36.
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.sqrt_one_div_natFloor_one_div_sub_sqrt_isBigO :
  (fun δ => √(1 / ↑⌊1 / δ⌋₊) - √δ) =O[nhdsWithin 0 (Set.Ici 0)] fun δ =>
    δ ^ (3 / 2)
    theorem FABL.sqrt_one_div_natFloor_one_div_sub_sqrt_isBigO :
  (fun δ =>
      √(1 / ↑⌊1 / δ⌋₊) -
        √δ) =O[nhdsWithin 0 (Set.Ici 0)]
    fun δ => δ ^ (3 / 2)
    The floor in Remark 5.36 contributes exactly an `O(δ^(3/2))` square-root
remainder from the right at zero.
  • defdefined in FABL/Chapter05/Peres.lean
    complete
    def FABL.peresMajorityUpperBound (δ : ℝ) : ℝ
    def FABL.peresMajorityUpperBound (δ : ℝ) : ℝ
    The deterministic majority-based modulus in the asymptotic form of Remark 5.36.
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.noiseSensitivity_le_majorityInfluenceRatio_of_isLinearThreshold
  {n : ℕ} (f : FABL.BooleanFunction n) (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    FABL.totalInfluence
        (FABL.majority ↑(FABL.inverseNoiseFloor δ)).toReal /
      ↑↑(FABL.inverseNoiseFloor δ)
    theorem FABL.noiseSensitivity_le_majorityInfluenceRatio_of_isLinearThreshold
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    FABL.totalInfluence
        (FABL.majority
            ↑(FABL.inverseNoiseFloor
                δ)).toReal /
      ↑↑(FABL.inverseNoiseFloor δ)
    The random-partition proof bounds every linear threshold function by the total-influence
quotient of majority in dimension `⌊1/δ⌋`.
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.noiseSensitivity_le_peresMajorityUpperBound {n : ℕ}
  (f : FABL.BooleanFunction n) (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤ FABL.peresMajorityUpperBound ↑δ
    theorem FABL.noiseSensitivity_le_peresMajorityUpperBound
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.IsLinearThreshold f)
  (δ : ↑FABL.PositiveHalfNoiseParameter) :
  FABL.noiseSensitivity ↑δ ⋯ f ≤
    FABL.peresMajorityUpperBound ↑δ
    The majority-based upper bound in Remark 5.36 is uniform over the dimension and over all
linear threshold functions.
  • theoremdefined in FABL/Chapter05/Peres.lean
    complete
    theorem FABL.peresMajorityUpperBound_sub_main_isBigO :
  (fun δ =>
      FABL.peresMajorityUpperBound δ -
        √(2 / Real.pi) * √δ) =O[nhdsWithin 0 (Set.Ici 0)]
    fun δ => δ ^ (3 / 2)
    theorem FABL.peresMajorityUpperBound_sub_main_isBigO :
  (fun δ =>
      FABL.peresMajorityUpperBound δ -
        √(2 / Real.pi) *
          √δ) =O[nhdsWithin 0 (Set.Ici 0)]
    fun δ => δ ^ (3 / 2)
    The uniform majority-based modulus in Remark 5.36 has leading term
`sqrt (2 / π) * sqrt δ` and an `O(δ^(3/2))` remainder from the right at zero.
Theorem5.5.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
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagssection-5-5refutedconjecture

Majority Is Least Stable Conjecture. Let f:\{-1,1\}^n\to\{-1,1\} be a linear threshold function with n odd. The conjecture asserted that, for every \rho\in[0,1], \operatorname{Stab}_\rho[f] \ge\operatorname{Stab}_\rho[\operatorname{Maj}_n]. The book immediately records that this conjecture is false: a counterexample already exists for n=5.

Theorem5.5.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.
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagssection-5-5openconjecture

Plausible replacement conjecture. Every linear threshold function f:\{-1,1\}^n\to\{-1,1\} should satisfy \operatorname{Stab}_\rho[f]\ge\frac2\pi\arcsin\rho \qquad\text{for every }\rho\in[0,1]. This conjecture remains open.

Theorem5.5.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 2
Statement dependency previews
Preview
Definition 2.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagssection-5-5openconjecture

Gotsman--Linial Conjecture. Let \mathcal P_{n,k} be the class of degree-at-most-k polynomial threshold functions on n variables. Every f\in\mathcal P_{n,k} should satisfy \mathbf I[f]\le O_k(1)\sqrt n. More strongly, the factor O_k(1) should be O(k). In the strongest form, for 0\le k\le n, the member of \mathcal P_{n,k} with maximal total influence is the symmetric function f(x)=\operatorname{sgn}(p(x_1+\cdots+x_n)), where p is a degree-k univariate polynomial alternating sign on the k+1 attainable values of x_1+\cdots+x_n nearest to 0.

All forms of this statement remain open for general k.

Theorem5.5.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 3
Statement dependency previews
Preview
Definition 2.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0XL∃∀N
Tagssection-5-5external-resultunformalized

Theorem 5.37 (Kane). Every f\in\mathcal P_{n,k} satisfies \mathbf I[f] \le\sqrt n\,(2^k\log n)^{O(k\log k)}. Consequently, for each fixed k\in\mathbb N^+ and every f\in\mathcal P_k=\bigcup_n\mathcal P_{n,k}, \operatorname{NS}_\delta[f] \le\sqrt\delta\,\operatorname{polylog}(1/\delta). The book cites this external theorem without proof.