Analysis of Boolean Functions in Lean

2.3. Total influence🔗

Definition2.3.1
uses 1
Used by 10
Reverse dependency previews
Preview
Proposition 2.3.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-3fidelity-exact

Definition 2.27. For every f:\{-1,1\}^n\to\mathbb R, the total influence of f is \mathbf I[f]=\sum_{i=1}^{n}\operatorname{Inf}_i[f].

Lean code for Definition2.3.1●1 definition
  • defdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    def FABL.totalInfluence {n : ℕ} (f : FABL.SignCube n → ℝ) : ℝ
    def FABL.totalInfluence {n : ℕ}
  (f : FABL.SignCube n → ℝ) : ℝ
    O'Donnell, Definition 2.27: the total influence is the sum of the coordinate influences.
Proposition2.3.2
Statement uses 3
Statement dependency previews
Preview
Definition 2.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-2-3fidelity-exact

Proposition 2.28. For every Boolean-valued function f:\{-1,1\}^n\to\{-1,1\}, \mathbf I[f] =\mathbb E_{\boldsymbol{x}\sim\{-1,1\}^n} [\operatorname{sens}_f(\boldsymbol{x})], where the sensitivity \operatorname{sens}_f(x) of f at x is the number of coordinates that are pivotal for f on input x.

Lean code for Proposition2.3.2●2 declarations
  • defdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    def FABL.sensitivity {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) : ℕ
    def FABL.sensitivity {n : ℕ}
  (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) : ℕ
    O'Donnell, Proposition 2.28: the sensitivity at an input is the number of pivotal
coordinates.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_toReal_eq_expect_sensitivity {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal =
    Finset.univ.expect fun x => ↑(FABL.sensitivity f x)
    theorem FABL.totalInfluence_toReal_eq_expect_sensitivity
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal =
    Finset.univ.expect fun x =>
      ↑(FABL.sensitivity f x)
    O'Donnell, Proposition 2.28: total influence of a Boolean function is its expected
sensitivity.
Lemma2.3.3
Statement uses 2
Statement dependency previews
Preview
Lemma 2.2.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-3fidelity-exact

Fact 2.29. For every f:\{-1,1\}^n\to\{-1,1\}, the fraction of all edges in the Hamming cube \{-1,1\}^n that are boundary edges for f is \frac{1}{n}\mathbf I[f].

Lean code for Lemma2.3.3●3 declarations
  • abbrevdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    abbrev FABL.UndirectedCubeEdge (n : ℕ) : Type
    abbrev FABL.UndirectedCubeEdge (n : ℕ) : Type
    The finite type of all undirected cube edges, indexed by their coordinate dimension.
  • defdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    def FABL.undirectedCubeBoundaryFraction {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) : ℝ
    def FABL.undirectedCubeBoundaryFraction
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) : ℝ
    The literal fraction of all undirected cube edges crossing the boundary. Positivity of `n`
ensures that the edge type is nonempty.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.undirectedCubeBoundaryFraction_eq_totalInfluence_div {n : ℕ}
  (f : FABL.BooleanFunction n) (hn : 0 < n) :
  FABL.undirectedCubeBoundaryFraction f hn =
    FABL.totalInfluence f.toReal / ↑n
    theorem FABL.undirectedCubeBoundaryFraction_eq_totalInfluence_div
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hn : 0 < n) :
  FABL.undirectedCubeBoundaryFraction f
      hn =
    FABL.totalInfluence f.toReal / ↑n
    O'Donnell, Fact 2.29 in the literal all-undirected-edges model: the boundary-edge fraction
is total influence divided by `n`.
Lemma2.3.4
Statement uses 2
Statement dependency previews
Preview
Lemma 2.2.4
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-3fidelity-exact

Example 2.30. For Boolean-valued functions f:\{-1,1\}^n\to\{-1,1\}, total influence ranges from 0 to n. The constant functions \pm1 minimize it, with total influence 0. The parity function \chi_{[n]} and its negation maximize it, with total influence n; every coordinate is pivotal on every input for these functions. The dictator functions and their negations have total influence 1. Moreover, \mathbf I[\operatorname{OR}_n]=\mathbf I[\operatorname{AND}_n]=n2^{1-n}, whereas, for odd n, \mathbf I[\operatorname{Maj}_n]=\sqrt{\frac{2}{\pi}}\sqrt n+O(n^{-1/2}).

Lean code for Lemma2.3.4●8 theorems
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.totalInfluence_toReal_mem_Icc {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal ∈ Set.Icc 0 ↑n
    theorem FABL.totalInfluence_toReal_mem_Icc {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal ∈
    Set.Icc 0 ↑n
    O'Donnell, Example 2.30: Boolean total influence lies between zero and `n`.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_const {n : ℕ} (c : ℝ) :
  (FABL.totalInfluence fun x => c) = 0
    theorem FABL.totalInfluence_const {n : ℕ}
  (c : ℝ) :
  (FABL.totalInfluence fun x => c) = 0
    O'Donnell, Example 2.30: constant real-valued functions have total influence zero.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_monomial {n : ℕ} (S : Finset (Fin n)) :
  FABL.totalInfluence (FABL.monomial S) = ↑S.card
    theorem FABL.totalInfluence_monomial {n : ℕ}
  (S : Finset (Fin n)) :
  FABL.totalInfluence (FABL.monomial S) =
    ↑S.card
    O'Donnell, Example 2.30: the total influence of a parity monomial is its number of
coordinates.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_neg {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence (-f) = FABL.totalInfluence f
    theorem FABL.totalInfluence_neg {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence (-f) =
    FABL.totalInfluence f
    Negating a real-valued function does not change its total influence.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_dictator {n : ℕ} (i : Fin n) :
  FABL.totalInfluence (FABL.dictator i).toReal = 1
    theorem FABL.totalInfluence_dictator {n : ℕ}
  (i : Fin n) :
  FABL.totalInfluence
      (FABL.dictator i).toReal =
    1
    O'Donnell, Example 2.30: a dictator has total influence one.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_orFunction (n : ℕ) :
  FABL.totalInfluence (FABL.orFunction n).toReal = ↑n / 2 ^ (n - 1)
    theorem FABL.totalInfluence_orFunction (n : ℕ) :
  FABL.totalInfluence
      (FABL.orFunction n).toReal =
    ↑n / 2 ^ (n - 1)
    O'Donnell, Example 2.30: `ORₙ` has total influence `n / 2^(n-1)`.
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_andFunction (n : ℕ) :
  FABL.totalInfluence (FABL.andFunction n).toReal = ↑n / 2 ^ (n - 1)
    theorem FABL.totalInfluence_andFunction (n : ℕ) :
  FABL.totalInfluence
      (FABL.andFunction n).toReal =
    ↑n / 2 ^ (n - 1)
    O'Donnell, Example 2.30: `ANDₙ` has total influence `n / 2^(n-1)`.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.totalInfluence_majority_odd_eq_main_add_error (m : ℕ) :
  FABL.totalInfluence (FABL.majority (2 * m + 1)).toReal =
    √(2 / Real.pi) * √↑(2 * m + 1) +
      FABL.oddMajorityTotalInfluenceError m
    theorem FABL.totalInfluence_majority_odd_eq_main_add_error
  (m : ℕ) :
  FABL.totalInfluence
      (FABL.majority (2 * m + 1)).toReal =
    √(2 / Real.pi) * √↑(2 * m + 1) +
      FABL.oddMajorityTotalInfluenceError
        m
    Example 2.30's complete odd-majority estimate, with its exact nonnegative remainder.
Proposition2.3.5
Statement uses 2
Statement dependency previews
Preview
Proposition 2.2.11
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-2-3fidelity-exact

Proposition 2.31. If f:\{-1,1\}^n\to\{-1,1\} is monotone, then \mathbf I[f]=\sum_{i=1}^{n}\widehat f(i), where \widehat f(i) abbreviates \widehat f(\{i\}).

Lean code for Proposition2.3.5●1 theorem
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    theorem FABL.totalInfluence_eq_sum_fourierCoeff_singleton_of_monotone {n : ℕ}
  (f : FABL.BooleanFunction n) (hf : Monotone f) :
  FABL.totalInfluence f.toReal = ∑ i, FABL.fourierCoeff f.toReal {i}
    theorem FABL.totalInfluence_eq_sum_fourierCoeff_singleton_of_monotone
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) :
  FABL.totalInfluence f.toReal =
    ∑ i, FABL.fourierCoeff f.toReal {i}
    O'Donnell, Proposition 2.31: for a monotone Boolean function, total influence is the sum of
the singleton Fourier coefficients.
Proposition2.3.6
Statement uses 2
Statement dependency previews
Preview
Proposition 1.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-3fidelity-exact

Proposition 2.32. Let f:\{-1,1\}^n\to\{-1,1\} be a voting rule for a two-candidate election. Under the impartial culture assumption, let \boldsymbol{x}=(\boldsymbol{x}_1,\ldots,\boldsymbol{x}_n) be the votes and let w be the number of votes that agree with the election outcome f(\boldsymbol{x}). Then \mathbb E[w] =\frac n2+\frac12\sum_{i=1}^{n}\widehat f(i).

Lean code for Proposition2.3.6●2 declarations
  • defdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    def FABL.agreeingVoteCount {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) : ℝ
    def FABL.agreeingVoteCount {n : ℕ}
  (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) : ℝ
    The real-valued number of votes agreeing with the outcome of a two-candidate voting rule.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    theorem FABL.expect_agreeingVoteCount {n : ℕ} (f : FABL.BooleanFunction n) :
  (Finset.univ.expect fun x => FABL.agreeingVoteCount f x) =
    ↑n / 2 + 1 / 2 * ∑ i, FABL.fourierCoeff f.toReal {i}
    theorem FABL.expect_agreeingVoteCount {n : ℕ}
  (f : FABL.BooleanFunction n) :
  (Finset.univ.expect fun x =>
      FABL.agreeingVoteCount f x) =
    ↑n / 2 +
      1 / 2 *
        ∑ i,
          FABL.fourierCoeff f.toReal {i}
    O'Donnell, Proposition 2.32: under impartial culture, the expected number of votes agreeing
with the outcome is `n/2` plus half the sum of singleton Fourier coefficients.
Lemma2.3.7
uses 1used by 1✓L∃∀N
Tagssection-2-3supportfidelity-exact

Equation (2.3). For every f:\{-1,1\}^n\to\mathbb R, with \boldsymbol{x} uniform on \{-1,1\}^n, \sum_{i=1}^{n}\widehat f(i) =\sum_{i=1}^{n}\mathbb E[f(\boldsymbol{x})\boldsymbol{x}_i] =\mathbb E\left[ f(\boldsymbol{x})(\boldsymbol{x}_1+\cdots+\boldsymbol{x}_n) \right]. \tag{2.3}

Lean code for Lemma2.3.7●1 theorem
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    theorem FABL.sum_fourierCoeff_singleton_eq_expect_mul_sum_signValue {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  ∑ i, FABL.fourierCoeff f {i} =
    Finset.univ.expect fun x => f x * ∑ i, FABL.signValue (x i)
    theorem FABL.sum_fourierCoeff_singleton_eq_expect_mul_sum_signValue
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  ∑ i, FABL.fourierCoeff f {i} =
    Finset.univ.expect fun x =>
      f x * ∑ i, FABL.signValue (x i)
    O'Donnell, Equation (2.3): the sum of singleton Fourier coefficients is the expected
correlation with the sum of the input coordinates.
Lemma2.3.8
Statement uses 4
Statement dependency previews
Preview
Definition 1.4.15
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Lemma 2.2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-3supportfidelity-exact

Exercise 2.22. For odd n:

  1. For every i\in[n], \operatorname{Inf}_i[\operatorname{Maj}_n] =\binom{n-1}{(n-1)/2}2^{1-n}.

  2. \operatorname{Inf}_1[\operatorname{Maj}_n] is a decreasing function of odd n.

  3. Using Stirling's formula m!=(m/e)^m(\sqrt{2\pi m}+O(m^{-1/2})), \operatorname{Inf}_1[\operatorname{Maj}_n] =\sqrt{\frac{2}{\pi n}}+O(n^{-3/2}), where the O(\cdot) terms are nonnegative.

  4. Consequently, \frac{2}{\pi} \le \mathbf W^1[\operatorname{Maj}_n] \le \frac{2}{\pi}+O(n^{-1}).

  5. Consequently, \sqrt{\frac{2}{\pi}}\sqrt n \le \mathbf I[\operatorname{Maj}_n] \le \sqrt{\frac{2}{\pi}}\sqrt n+O(n^{-1/2}).

If n is even and f:\{-1,1\}^n\to\{-1,1\} is a majority function, then \mathbf I[f]=\mathbf I[\operatorname{Maj}_{n-1}] =\sqrt{\frac{2}{\pi}}\sqrt n+O(n^{-1/2}).

Lean code for Lemma2.3.8●18 declarations
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.booleanInfluence_majority_odd_eq_oddMajorityInfluence (m : ℕ)
  (i : Fin (2 * m + 1)) :
  FABL.booleanInfluence (FABL.majority (2 * m + 1)) i =
    FABL.oddMajorityInfluence m
    theorem FABL.booleanInfluence_majority_odd_eq_oddMajorityInfluence
  (m : ℕ) (i : Fin (2 * m + 1)) :
  FABL.booleanInfluence
      (FABL.majority (2 * m + 1)) i =
    FABL.oddMajorityInfluence m
    Exercise 2.22(a), restated using the central-binomial probability.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityInfluence_strictAnti :
  StrictAnti FABL.oddMajorityInfluence
    theorem FABL.oddMajorityInfluence_strictAnti :
  StrictAnti FABL.oddMajorityInfluence
    O'Donnell, Exercise 2.22(b): coordinate influence of odd majority strictly decreases with
the odd arity.
  • defdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    def FABL.oddMajorityInfluenceMain (m : ℕ) : ℝ
    def FABL.oddMajorityInfluenceMain (m : ℕ) : ℝ
    The leading term in Exercise 2.22(c), written for odd arity `2m+1`.
  • defdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    def FABL.oddMajorityInfluenceError (m : ℕ) : ℝ
    def FABL.oddMajorityInfluenceError (m : ℕ) : ℝ
    The nonnegative remainder in the majority-influence estimate of Exercise 2.22(c).
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityInfluenceError_mem_Icc (m : ℕ) :
  FABL.oddMajorityInfluenceError m ∈
    Set.Icc 0 (FABL.oddMajorityInfluenceMain m / ↑(2 * m + 1))
    theorem FABL.oddMajorityInfluenceError_mem_Icc
  (m : ℕ) :
  FABL.oddMajorityInfluenceError m ∈
    Set.Icc 0
      (FABL.oddMajorityInfluenceMain m /
        ↑(2 * m + 1))
    Exercise 2.22(c), with an explicit nonnegative error bound.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityInfluenceError_isBigO :
  FABL.oddMajorityInfluenceError =O[Filter.atTop] fun m =>
    ↑(2 * m + 1) ^ (-(3 / 2))
    theorem FABL.oddMajorityInfluenceError_isBigO :
  FABL.oddMajorityInfluenceError =O[Filter.atTop]
    fun m => ↑(2 * m + 1) ^ (-(3 / 2))
    O'Donnell, Exercise 2.22(c), in literal asymptotic notation, including the book's
nonnegative remainder convention.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_majority_odd (m : ℕ) :
  FABL.fourierWeightAtLevel 1 (FABL.majority (2 * m + 1)).toReal =
    ↑(2 * m + 1) * FABL.oddMajorityInfluence m ^ 2
    theorem FABL.fourierWeightAtLevel_one_majority_odd
  (m : ℕ) :
  FABL.fourierWeightAtLevel 1
      (FABL.majority (2 * m + 1)).toReal =
    ↑(2 * m + 1) *
      FABL.oddMajorityInfluence m ^ 2
    Exercise 2.22(d): the level-one Fourier weight of odd majority is `n` times the square of
its common coordinate influence.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.two_div_pi_le_fourierWeightAtLevel_one_majority_odd (m : ℕ) :
  2 / Real.pi ≤
    FABL.fourierWeightAtLevel 1 (FABL.majority (2 * m + 1)).toReal
    theorem FABL.two_div_pi_le_fourierWeightAtLevel_one_majority_odd
  (m : ℕ) :
  2 / Real.pi ≤
    FABL.fourierWeightAtLevel 1
      (FABL.majority (2 * m + 1)).toReal
    Exercise 2.22(d), lower bound: `2/π ≤ W¹[Majₙ]` for odd `n`.
  • defdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    def FABL.oddMajorityLevelOneWeightError (m : ℕ) : ℝ
    def FABL.oddMajorityLevelOneWeightError
  (m : ℕ) : ℝ
    The nonnegative `O(n⁻¹)` remainder in Exercise 2.22(d).
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityLevelOneWeightError_mem_Icc (m : ℕ) :
  FABL.oddMajorityLevelOneWeightError m ∈
    Set.Icc 0 (2 / (Real.pi * ↑(2 * m + 1)))
    theorem FABL.oddMajorityLevelOneWeightError_mem_Icc
  (m : ℕ) :
  FABL.oddMajorityLevelOneWeightError m ∈
    Set.Icc 0
      (2 / (Real.pi * ↑(2 * m + 1)))
    Exercise 2.22(d), with a global explicit error interval.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityLevelOneWeightError_isBigO :
  FABL.oddMajorityLevelOneWeightError =O[Filter.atTop] fun m =>
    ↑(2 * m + 1) ^ (-1)
    theorem FABL.oddMajorityLevelOneWeightError_isBigO :
  FABL.oddMajorityLevelOneWeightError =O[Filter.atTop]
    fun m => ↑(2 * m + 1) ^ (-1)
    Exercise 2.22(d), in literal asymptotic notation.
  • defdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    def FABL.oddMajorityTotalInfluenceError (m : ℕ) : ℝ
    def FABL.oddMajorityTotalInfluenceError
  (m : ℕ) : ℝ
    The nonnegative remainder in the total-influence estimate of Exercise 2.22(e) and
Example 2.30.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityTotalInfluenceError_mem_Icc (m : ℕ) :
  FABL.oddMajorityTotalInfluenceError m ∈ Set.Icc 0 (1 / √↑(2 * m + 1))
    theorem FABL.oddMajorityTotalInfluenceError_mem_Icc
  (m : ℕ) :
  FABL.oddMajorityTotalInfluenceError m ∈
    Set.Icc 0 (1 / √↑(2 * m + 1))
    Exercise 2.22(e), with the explicit global `n⁻¹ᐟ²` error bound.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityInfluence.lean
    complete
    theorem FABL.oddMajorityTotalInfluenceError_isBigO :
  FABL.oddMajorityTotalInfluenceError =O[Filter.atTop] fun m =>
    ↑(2 * m + 1) ^ (-(1 / 2))
    theorem FABL.oddMajorityTotalInfluenceError_isBigO :
  FABL.oddMajorityTotalInfluenceError =O[Filter.atTop]
    fun m => ↑(2 * m + 1) ^ (-(1 / 2))
    O'Donnell, Exercise 2.22(e) and Example 2.30, in literal asymptotic notation.
  • theoremdefined in FABL/Chapter02/TotalInfluence/EvenMajority.lean
    complete
    theorem FABL.totalInfluence_evenMajority_eq_predecessor {n : ℕ} (hn : Even n)
  (hnpos : 0 < n) (f : FABL.BooleanFunction n)
  (hf : FABL.IsMajorityFunction f) :
  FABL.totalInfluence f.toReal =
    FABL.totalInfluence (FABL.majority (n - 1)).toReal
    theorem FABL.totalInfluence_evenMajority_eq_predecessor
  {n : ℕ} (hn : Even n) (hnpos : 0 < n)
  (f : FABL.BooleanFunction n)
  (hf : FABL.IsMajorityFunction f) :
  FABL.totalInfluence f.toReal =
    FABL.totalInfluence
      (FABL.majority (n - 1)).toReal
    Exercise 2.22(f), stated for an arbitrary positive even arity `n`.
  • theoremdefined in FABL/Chapter02/TotalInfluence/EvenMajority.lean
    complete
    theorem FABL.totalInfluence_evenMajority_exact (m : ℕ)
  (f : FABL.BooleanFunction (2 * m + 2))
  (hf : FABL.IsMajorityFunction f) :
  FABL.totalInfluence f.toReal =
    ↑(2 * m + 1) * ↑((2 * m).choose m) / 2 ^ (2 * m)
    theorem FABL.totalInfluence_evenMajority_exact
  (m : ℕ)
  (f : FABL.BooleanFunction (2 * m + 2))
  (hf : FABL.IsMajorityFunction f) :
  FABL.totalInfluence f.toReal =
    ↑(2 * m + 1) * ↑((2 * m).choose m) /
      2 ^ (2 * m)
    Exercise 2.22(f), expanded using the exact odd-majority central-binomial formula.
  • theoremdefined in FABL/Chapter02/TotalInfluence/EvenMajority.lean
    complete
    theorem FABL.abs_evenMajorityTotalInfluenceError_le (m : ℕ)
  (f : FABL.BooleanFunction (2 * m + 2))
  (hf : FABL.IsMajorityFunction f) :
  |FABL.evenMajorityTotalInfluenceError m f| ≤ 4 / √↑(2 * m + 2)
    theorem FABL.abs_evenMajorityTotalInfluenceError_le
  (m : ℕ)
  (f : FABL.BooleanFunction (2 * m + 2))
  (hf : FABL.IsMajorityFunction f) :
  |FABL.evenMajorityTotalInfluenceError m
        f| ≤
    4 / √↑(2 * m + 2)
    Exercise 2.22(f): the signed even-arity remainder is bounded by `4 n⁻¹ᐟ²`.
  • theoremdefined in FABL/Chapter02/TotalInfluence/EvenMajority.lean
    complete
    theorem FABL.evenMajorityTotalInfluenceError_isBigO
  (f : (m : ℕ) → FABL.BooleanFunction (2 * m + 2))
  (hf : ∀ (m : ℕ), FABL.IsMajorityFunction (f m)) :
  (fun m =>
      FABL.evenMajorityTotalInfluenceError m (f m)) =O[Filter.atTop]
    fun m => ↑(2 * m + 2) ^ (-(1 / 2))
    theorem FABL.evenMajorityTotalInfluenceError_isBigO
  (f :
    (m : ℕ) →
      FABL.BooleanFunction (2 * m + 2))
  (hf :
    ∀ (m : ℕ),
      FABL.IsMajorityFunction (f m)) :
  (fun m =>
      FABL.evenMajorityTotalInfluenceError
        m (f m)) =O[Filter.atTop]
    fun m => ↑(2 * m + 2) ^ (-(1 / 2))
    O'Donnell, Exercise 2.22(f), in literal `O(n⁻¹ᐟ²)` notation for any family of
even-arity majority functions.
Theorem2.3.9
Statement uses 3
Statement dependency previews
Preview
Proposition 2.3.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Lemma 2.5.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-3fidelity-exact

Theorem 2.33. Among all functions f:\{-1,1\}^n\to\{-1,1\}, the unique maximizers of \sum_{i=1}^{n}\widehat f(i) are the majority functions: f(x) must equal \operatorname{sgn}(x_1+\cdots+x_n) whenever x_1+\cdots+x_n\ne0. In particular, every monotone f:\{-1,1\}^n\to\{-1,1\} satisfies \mathbf I[f] \le \mathbf I[\operatorname{Maj}_n] =\sqrt{\frac{2}{\pi}}\sqrt n+O(n^{-1/2}).

Lean code for Theorem2.3.9●4 theorems
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    theorem FABL.sum_fourierCoeff_singleton_le_majority {n : ℕ}
  (f : FABL.BooleanFunction n) :
  ∑ i, FABL.fourierCoeff f.toReal {i} ≤
    ∑ i, FABL.fourierCoeff (FABL.majority n).toReal {i}
    theorem FABL.sum_fourierCoeff_singleton_le_majority
  {n : ℕ} (f : FABL.BooleanFunction n) :
  ∑ i, FABL.fourierCoeff f.toReal {i} ≤
    ∑ i,
      FABL.fourierCoeff
        (FABL.majority n).toReal {i}
    O'Donnell, Theorem 2.33: majority maximizes the sum of the singleton Fourier
coefficients.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    theorem FABL.sum_fourierCoeff_singleton_eq_majority_iff {n : ℕ}
  (f : FABL.BooleanFunction n) :
  ∑ i, FABL.fourierCoeff f.toReal {i} =
      ∑ i, FABL.fourierCoeff (FABL.majority n).toReal {i} ↔
    ∀ (x : FABL.SignCube n),
      ∑ i, FABL.signValue (x i) ≠ 0 → f x = FABL.majority n x
    theorem FABL.sum_fourierCoeff_singleton_eq_majority_iff
  {n : ℕ} (f : FABL.BooleanFunction n) :
  ∑ i, FABL.fourierCoeff f.toReal {i} =
      ∑ i,
        FABL.fourierCoeff
          (FABL.majority n).toReal {i} ↔
    ∀ (x : FABL.SignCube n),
      ∑ i, FABL.signValue (x i) ≠ 0 →
        f x = FABL.majority n x
    O'Donnell, Theorem 2.33: equality in the singleton-coefficient bound holds exactly when the
rule agrees with majority away from tied vote profiles.
  • theoremdefined in FABL/Chapter02/TotalInfluence/MajorityOptimality.lean
    complete
    theorem FABL.totalInfluence_toReal_le_majority_of_monotone {n : ℕ}
  (f : FABL.BooleanFunction n) (hf : Monotone f) :
  FABL.totalInfluence f.toReal ≤
    FABL.totalInfluence (FABL.majority n).toReal
    theorem FABL.totalInfluence_toReal_le_majority_of_monotone
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : Monotone f) :
  FABL.totalInfluence f.toReal ≤
    FABL.totalInfluence
      (FABL.majority n).toReal
    O'Donnell, Theorem 2.33: among monotone Boolean functions, majority maximizes total
influence.
  • theoremdefined in FABL/Chapter02/TotalInfluence/EvenMajority.lean
    complete
    theorem FABL.totalInfluence_toReal_le_majority_main_add_error_of_monotone
  (m : ℕ) (f : FABL.BooleanFunction (2 * m + 1)) (hf : Monotone f) :
  FABL.totalInfluence f.toReal ≤
    √(2 / Real.pi) * √↑(2 * m + 1) +
      FABL.oddMajorityTotalInfluenceError m
    theorem FABL.totalInfluence_toReal_le_majority_main_add_error_of_monotone
  (m : ℕ)
  (f : FABL.BooleanFunction (2 * m + 1))
  (hf : Monotone f) :
  FABL.totalInfluence f.toReal ≤
    √(2 / Real.pi) * √↑(2 * m + 1) +
      FABL.oddMajorityTotalInfluenceError
        m
    Theorem 2.33 with the complete Exercise 2.22(e) asymptotic bound substituted.
Lemma2.3.10
Statement uses 2
Statement dependency previews
Preview
Definition 2.2.7
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-2-3supportfidelity-exact

Equation (2.4). For every f:\{-1,1\}^n\to\mathbb R, \mathbf I[f] =\sum_{i=1}^{n}\operatorname{Inf}_i[f] =\sum_{i=1}^{n}\mathbb E[D_i f(\boldsymbol{x})^2] =\mathbb E\left[\sum_{i=1}^{n}D_i f(\boldsymbol{x})^2\right]. \tag{2.4}

Lean code for Lemma2.3.10●1 theorem
  • theoremdefined in FABL/Chapter02/TotalInfluence/Basic.lean
    complete
    theorem FABL.totalInfluence_eq_expect_sum_sq_discreteDerivative {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    Finset.univ.expect fun x => ∑ i, (FABL.discreteDerivative i) f x ^ 2
    theorem FABL.totalInfluence_eq_expect_sum_sq_discreteDerivative
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    Finset.univ.expect fun x =>
      ∑ i,
        (FABL.discreteDerivative i) f x ^
          2
    O'Donnell, Equation (2.4): total influence is the expected sum of the squared discrete
derivatives.
Definition2.3.11
Statement uses 2
Statement dependency previews
Preview
Definition 2.2.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-2-3fidelity-exact

Definition 2.34. The discrete gradient operator maps every f:\{-1,1\}^n\to\mathbb R to \nabla f:\{-1,1\}^n\to\mathbb R^n defined by \nabla f(x)=(D_1f(x),D_2f(x),\ldots,D_nf(x)). If f:\{-1,1\}^n\to\{-1,1\}, then \lVert\nabla f(x)\rVert_2^2=\operatorname{sens}_f(x), where \lVert\cdot\rVert_2 is the usual Euclidean norm on \mathbb R^n.

Lean code for Definition2.3.11●2 declarations
  • defdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    def FABL.discreteGradient {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) : EuclideanSpace ℝ (Fin n)
    def FABL.discreteGradient {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  EuclideanSpace ℝ (Fin n)
    O'Donnell, Definition 2.34: the discrete gradient, valued in Mathlib's Euclidean space.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.norm_discreteGradient_toReal_sq_eq_sensitivity {n : ℕ}
  (f : FABL.BooleanFunction n) (x : FABL.SignCube n) :
  ‖FABL.discreteGradient f.toReal x‖ ^ 2 = ↑(FABL.sensitivity f x)
    theorem FABL.norm_discreteGradient_toReal_sq_eq_sensitivity
  {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) :
  ‖FABL.discreteGradient f.toReal x‖ ^ 2 =
    ↑(FABL.sensitivity f x)
    O'Donnell, Definition 2.34: for Boolean-valued functions, squared gradient norm equals
sensitivity.
Proposition2.3.12
Statement uses 2
Statement dependency previews
Preview
Lemma 2.3.10
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-3fidelity-exact

Proposition 2.35. For every f:\{-1,1\}^n\to\mathbb R, \mathbf I[f] =\mathbb E_{\boldsymbol{x}\sim\{-1,1\}^n} [\lVert\nabla f(\boldsymbol{x})\rVert_2^2].

Lean code for Proposition2.3.12●1 theorem
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.totalInfluence_eq_expect_norm_discreteGradient_sq {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    Finset.univ.expect fun x => ‖FABL.discreteGradient f x‖ ^ 2
    theorem FABL.totalInfluence_eq_expect_norm_discreteGradient_sq
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    Finset.univ.expect fun x =>
      ‖FABL.discreteGradient f x‖ ^ 2
    O'Donnell, Proposition 2.35: total influence is the expected squared Euclidean norm of the
discrete gradient.
Definition2.3.13
uses 1used by 1✓L∃∀N
Tagssection-2-3fidelity-exact

Definition 2.36. The Laplacian is the linear operator on functions f:\{-1,1\}^n\to\mathbb R defined by L=\sum_{i=1}^{n}L_i; equivalently, Lf=\sum_{i=1}^{n}L_if.

Lean code for Definition2.3.13●1 definition
  • defdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    def FABL.laplacian {n : ℕ} : (FABL.SignCube n → ℝ) →ₗ[ℝ] FABL.SignCube n → ℝ
    def FABL.laplacian {n : ℕ} :
  (FABL.SignCube n → ℝ) →ₗ[ℝ]
    FABL.SignCube n → ℝ
    O'Donnell, Definition 2.36: the Laplacian is the sum of the coordinate Laplacians.
Lemma2.3.14
Statement uses 4
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-2-3supportfidelity-exact

Exercise 2.17. Prove that for every f:\{-1,1\}^n\to\mathbb R:

  1. Lf(x)=\frac n2\left( f(x)-\operatorname*{avg}_{i\in[n]}\{f(x^{\oplus i})\} \right).

  2. If f:\{-1,1\}^n\to\{-1,1\}, then Lf(x)=f(x)\operatorname{sens}_f(x).

  3. Lf=\sum_{S\subseteq[n]}|S|\widehat f(S)\chi_S.

  4. \langle f,Lf\rangle=\mathbf I[f].

Lean code for Lemma2.3.14●4 theorems
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.laplacian_eq_sum_sub_flip_div_two {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  FABL.laplacian f x = ∑ i, (f x - f (FABL.flipCoordinate x i)) / 2
    theorem FABL.laplacian_eq_sum_sub_flip_div_two
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  FABL.laplacian f x =
    ∑ i,
      (f x -
          f (FABL.flipCoordinate x i)) /
        2
    O'Donnell, Proposition 2.37(1): the Laplacian is half the sum of the differences across all
incident cube edges.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.laplacian_toReal_eq_mul_sensitivity {n : ℕ}
  (f : FABL.BooleanFunction n) (x : FABL.SignCube n) :
  FABL.laplacian f.toReal x = f.toReal x * ↑(FABL.sensitivity f x)
    theorem FABL.laplacian_toReal_eq_mul_sensitivity
  {n : ℕ} (f : FABL.BooleanFunction n)
  (x : FABL.SignCube n) :
  FABL.laplacian f.toReal x =
    f.toReal x * ↑(FABL.sensitivity f x)
    O'Donnell, Proposition 2.37(2): on a Boolean-valued function the Laplacian is the output
times the sensitivity.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.laplacian_eq_fourier_sum {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  FABL.laplacian f x =
    ∑ S, ↑S.card * FABL.fourierCoeff f S * FABL.monomial S x
    theorem FABL.laplacian_eq_fourier_sum {n : ℕ}
  (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  FABL.laplacian f x =
    ∑ S,
      ↑S.card * FABL.fourierCoeff f S *
        FABL.monomial S x
    O'Donnell, Proposition 2.37(3): the Fourier expansion of the Laplacian multiplies the
coefficient at `S` by `|S|`.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.uniformInner_laplacian_eq_totalInfluence {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.uniformInner f (FABL.laplacian f) = FABL.totalInfluence f
    theorem FABL.uniformInner_laplacian_eq_totalInfluence
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.uniformInner f (FABL.laplacian f) =
    FABL.totalInfluence f
    O'Donnell, Proposition 2.37(4): pairing a function with its Laplacian gives total influence.
Proposition2.3.15
uses 1used by 0✓L∃∀N
Tagssection-2-3fidelity-exact

Proposition 2.37. For every f:\{-1,1\}^n\to\mathbb R:

  1. Lf(x)=\frac n2\left( f(x)-\operatorname*{avg}_{i\in[n]}\{f(x^{\oplus i})\} \right).

  2. If f:\{-1,1\}^n\to\{-1,1\}, then Lf(x)=f(x)\operatorname{sens}_f(x).

  3. Lf=\sum_{S\subseteq[n]}|S|\widehat f(S)\chi_S.

  4. \langle f,Lf\rangle=\mathbf I[f].

Lean code for Proposition2.3.15●1 theorem
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.laplacian_eq_card_mul_sub_expect_flip {n : ℕ}
  (f : FABL.SignCube n → ℝ) (x : FABL.SignCube n) :
  FABL.laplacian f x =
    ↑n / 2 *
      (f x - Finset.univ.expect fun i => f (FABL.flipCoordinate x i))
    theorem FABL.laplacian_eq_card_mul_sub_expect_flip
  {n : ℕ} (f : FABL.SignCube n → ℝ)
  (x : FABL.SignCube n) :
  FABL.laplacian f x =
    ↑n / 2 *
      (f x -
        Finset.univ.expect fun i =>
          f (FABL.flipCoordinate x i))
    O'Donnell, Proposition 2.37(1), average-neighbor form: the Laplacian is `n/2` times the
difference between the value at `x` and the average value at its neighbors.
Theorem2.3.16
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 5
Reverse dependency previews
Preview
Theorem 2.3.18
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-3fidelity-exact

Theorem 2.38. For every f:\{-1,1\}^n\to\mathbb R, \mathbf I[f] =\sum_{S\subseteq[n]}|S|\widehat f(S)^2 =\sum_{k=0}^{n}k\,\mathbf W^k[f]. \tag{2.5} If f:\{-1,1\}^n\to\{-1,1\} and \mathcal S_f is its spectral distribution, then equivalently \mathbf I[f]=\mathbb E_{\boldsymbol S\sim\mathcal S_f}[|\boldsymbol S|].

Lean code for Theorem2.3.16●3 theorems
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.totalInfluence_eq_sum_card_mul_sq_fourierCoeff {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f = ∑ S, ↑S.card * FABL.fourierCoeff f S ^ 2
    theorem FABL.totalInfluence_eq_sum_card_mul_sq_fourierCoeff
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    ∑ S,
      ↑S.card * FABL.fourierCoeff f S ^ 2
    O'Donnell, Theorem 2.38, first Fourier formula: total influence is Fourier weight weighted
by subset cardinality.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.totalInfluence_eq_sum_level_mul_fourierWeight {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    ∑ k ∈ Finset.range (n + 1), ↑k * FABL.fourierWeightAtLevel k f
    theorem FABL.totalInfluence_eq_sum_level_mul_fourierWeight
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.totalInfluence f =
    ∑ k ∈ Finset.range (n + 1),
      ↑k * FABL.fourierWeightAtLevel k f
    O'Donnell, Theorem 2.38, second Fourier formula: regrouping by degree expresses total
influence as the degree-weighted sum of level Fourier weights.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.totalInfluence_toReal_eq_spectralSample_expectedCard {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal =
    ∑ S, ((FABL.spectralSample f) S).toReal * ↑S.card
    theorem FABL.totalInfluence_toReal_eq_spectralSample_expectedCard
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.totalInfluence f.toReal =
    ∑ S,
      ((FABL.spectralSample f) S).toReal *
        ↑S.card
    O'Donnell, Theorem 2.38, spectral-distribution form: total influence of a Boolean function
is the finite expectation of the spectral sample's cardinality.
Lemma2.3.17
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 3
Reverse dependency previews
Preview
Theorem 2.3.18
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-3supportfidelity-exact

Exercise 1.19(a),(b). Let f:\{-1,1\}^n\to\{-1,1\}.

  1. If \mathbf W^1[f]=1, then f(x)=\pm\chi_S(x) for some S\subseteq[n] with |S|=1.

  2. If \mathbf W^{\le1}[f]=1, then f depends on at most one input coordinate.

Lean code for Lemma2.3.17●2 theorems
  • theoremdefined in FABL/Chapter02/InfluencesAndDerivatives/DegreeOneRigidity.lean
    complete
    theorem FABL.eq_dictator_or_neg_dictator_of_fourierWeightAtLevel_one_eq_one
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hweight : FABL.fourierWeightAtLevel 1 f.toReal = 1) :
  ∃ i, f = FABL.dictator i ∨ f = -FABL.dictator i
    theorem FABL.eq_dictator_or_neg_dictator_of_fourierWeightAtLevel_one_eq_one
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hweight :
    FABL.fourierWeightAtLevel 1 f.toReal =
      1) :
  ∃ i,
    f = FABL.dictator i ∨
      f = -FABL.dictator i
    O'Donnell, Exercise 1.19(a): a Boolean function with all Fourier weight at level one is a
signed dictator.
  • theoremdefined in FABL/Chapter02/InfluencesAndDerivatives/DegreeOneRigidity.lean
    complete
    theorem FABL.isKJunta_one_of_fourierWeightAtMost_one_eq_one {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hweight : FABL.fourierWeightAtMost 1 f.toReal = 1) :
  FABL.IsKJunta f 1
    theorem FABL.isKJunta_one_of_fourierWeightAtMost_one_eq_one
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hweight :
    FABL.fourierWeightAtMost 1 f.toReal =
      1) :
  FABL.IsKJunta f 1
    O'Donnell, Exercise 1.19(b): a Boolean function with all Fourier weight through level one
depends on at most one coordinate.
Theorem2.3.18
Statement uses 3
Statement dependency previews
Preview
Proposition 1.4.8
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-3fidelity-exact

Poincaré Inequality. For every f:\{-1,1\}^n\to\mathbb R, \operatorname{Var}[f]\le\mathbf I[f]. Equality holds if and only if all Fourier weight of f is on degrees 0 and 1, equivalently \mathbf W^{\le1}[f]=\mathbb E[f^2]. If f:\{-1,1\}^n\to\{-1,1\} is Boolean-valued, equality holds if and only if f=\pm1 or f=\pm\chi_i for some i\in[n].

Lean code for Theorem2.3.18●5 theorems
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.variance_le_totalInfluence {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f ≤ FABL.totalInfluence f
    theorem FABL.variance_le_totalInfluence {n : ℕ}
  (f : FABL.SignCube n → ℝ) :
  FABL.variance f ≤ FABL.totalInfluence f
    The core Poincaré inequality in Section 2.3: variance is at most total influence.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.variance_eq_totalInfluence_iff {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f = FABL.totalInfluence f ↔
    ∀ (S : Finset (Fin n)), 1 < S.card → FABL.fourierCoeff f S = 0
    theorem FABL.variance_eq_totalInfluence_iff
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f =
      FABL.totalInfluence f ↔
    ∀ (S : Finset (Fin n)),
      1 < S.card →
        FABL.fourierCoeff f S = 0
    Equality in the Poincaré inequality is equivalent to vanishing of every Fourier coefficient
above degree one.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.variance_eq_totalInfluence_iff_fourierWeightAbove_one_eq_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f = FABL.totalInfluence f ↔
    FABL.fourierWeightAbove 1 f = 0
    theorem FABL.variance_eq_totalInfluence_iff_fourierWeightAbove_one_eq_zero
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f =
      FABL.totalInfluence f ↔
    FABL.fourierWeightAbove 1 f = 0
    The Poincaré equality condition in Fourier-weight notation: equality holds exactly when
there is no Fourier weight above degree one.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.variance_eq_totalInfluence_iff_lowDegreeWeight_eq_secondMoment
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f = FABL.totalInfluence f ↔
    ∑ S with S.card ≤ 1, FABL.fourierCoeff f S ^ 2 =
      Finset.univ.expect fun x => f x ^ 2
    theorem FABL.variance_eq_totalInfluence_iff_lowDegreeWeight_eq_secondMoment
  {n : ℕ} (f : FABL.SignCube n → ℝ) :
  FABL.variance f =
      FABL.totalInfluence f ↔
    ∑ S with S.card ≤ 1,
        FABL.fourierCoeff f S ^ 2 =
      Finset.univ.expect fun x => f x ^ 2
    The Poincaré equality condition in the book's `W^{≤1}` form: all second moment lies on
degrees zero and one.
  • theoremdefined in FABL/Chapter02/TotalInfluence/LaplacianAndPoincare.lean
    complete
    theorem FABL.variance_eq_totalInfluence_toReal_iff {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.variance f.toReal = FABL.totalInfluence f.toReal ↔
    (f = fun x => 1) ∨
      (f = fun x => -1) ∨
        ∃ i, f = FABL.dictator i ∨ f = -FABL.dictator i
    theorem FABL.variance_eq_totalInfluence_toReal_iff
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.variance f.toReal =
      FABL.totalInfluence f.toReal ↔
    (f = fun x => 1) ∨
      (f = fun x => -1) ∨
        ∃ i,
          f = FABL.dictator i ∨
            f = -FABL.dictator i
    The Boolean equality classification in the Poincaré inequality: equality holds exactly for
the two constants and the signed dictators.
Theorem2.3.19
Statement uses 2
Statement dependency previews
Preview
Definition 1.3.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-3fidelity-exact-log-base-two

Theorem 2.39. Let f:\{-1,1\}^n\to\{-1,1\} and set \alpha =\min\{\Pr[f(\boldsymbol{x})=1],\Pr[f(\boldsymbol{x})=-1]\}, where \boldsymbol{x} is uniform on \{-1,1\}^n. Then 2\alpha\log_2(1/\alpha)\le\mathbf I[f].

Lean code for Theorem2.3.19●4 declarations
  • defdefined in FABL/Chapter02/TotalInfluence/EdgeIsoperimetric.lean
    complete
    def FABL.positiveProbability {n : ℕ} (f : FABL.BooleanFunction n) : ℝ
    def FABL.positiveProbability {n : ℕ}
  (f : FABL.BooleanFunction n) : ℝ
    The uniform probability that a Boolean function takes the value `1`.
  • defdefined in FABL/Chapter02/TotalInfluence/EdgeIsoperimetric.lean
    complete
    def FABL.negativeProbability {n : ℕ} (f : FABL.BooleanFunction n) : ℝ
    def FABL.negativeProbability {n : ℕ}
  (f : FABL.BooleanFunction n) : ℝ
    The uniform probability that a Boolean function takes the value `-1`.
  • defdefined in FABL/Chapter02/TotalInfluence/EdgeIsoperimetric.lean
    complete
    def FABL.minorityProbability {n : ℕ} (f : FABL.BooleanFunction n) : ℝ
    def FABL.minorityProbability {n : ℕ}
  (f : FABL.BooleanFunction n) : ℝ
    The smaller of the probabilities of the two Boolean output values.
  • theoremdefined in FABL/Chapter02/TotalInfluence/EdgeIsoperimetric.lean
    complete
    theorem FABL.two_mul_minorityProbability_mul_logb_inv_le_totalInfluence {n : ℕ}
  (f : FABL.BooleanFunction n) :
  2 * FABL.minorityProbability f *
      Real.logb 2 (FABL.minorityProbability f)⁻¹ ≤
    FABL.totalInfluence f.toReal
    theorem FABL.two_mul_minorityProbability_mul_logb_inv_le_totalInfluence
  {n : ℕ} (f : FABL.BooleanFunction n) :
  2 * FABL.minorityProbability f *
      Real.logb 2
        (FABL.minorityProbability f)⁻¹ ≤
    FABL.totalInfluence f.toReal
    O'Donnell, Theorem 2.39: if `α` is the smaller output probability of a Boolean function,
then `2 α log₂(1/α) ≤ I[f]`.