Analysis of Boolean Functions in Lean

2.5. Highlight: Arrow's Theorem🔗

Lemma2.5.1
uses 0
Used by 2
Reverse dependency previews
Preview
Definition 2.5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-5supportfidelity-exact

Exercise 1.1(i). The not-all-equal function \operatorname{NAE}_n:\{-1,1\}^n\to\{0,1\} is defined by \operatorname{NAE}_n(x)=1 \quad\Longleftrightarrow\quad x_1,\ldots,x_n\text{ are not all equal}. For n=3, its satisfying inputs are exactly \{(+1,+1,-1),(+1,-1,-1),(-1,+1,-1), (-1,+1,+1),(+1,-1,+1),(-1,-1,+1)\}.

Lean code for Lemma2.5.1●5 declarations
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.IsNAE3 (w : FABL.PairwiseContest → FABL.Sign) : Prop
    def FABL.IsNAE3
  (w : FABL.PairwiseContest → FABL.Sign) :
  Prop
    O'Donnell, Exercise 1.1(i): the three signs are not all equal.
  • inductive(6 constructors)defined in FABL/Chapter02/Arrow.lean
    complete
    inductive FABL.Ranking3 : Type
    inductive FABL.Ranking3 : Type
    The six strict rankings of three named candidates.

    Constructors

    FABL.Ranking3.abc : FABL.Ranking3
    Candidate `a` is ranked above `b`, which is ranked above `c`. 
    FABL.Ranking3.acb : FABL.Ranking3
    Candidate `a` is ranked above `c`, which is ranked above `b`. 
    FABL.Ranking3.bac : FABL.Ranking3
    Candidate `b` is ranked above `a`, which is ranked above `c`. 
    FABL.Ranking3.bca : FABL.Ranking3
    Candidate `b` is ranked above `c`, which is ranked above `a`. 
    FABL.Ranking3.cab : FABL.Ranking3
    Candidate `c` is ranked above `a`, which is ranked above `b`. 
    FABL.Ranking3.cba : FABL.Ranking3
    Candidate `c` is ranked above `b`, which is ranked above `a`.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.rankingPreference :
  FABL.Ranking3 → FABL.PairwiseContest → FABL.Sign
    def FABL.rankingPreference :
  FABL.Ranking3 →
    FABL.PairwiseContest → FABL.Sign
    Encode a strict ranking by its preferences in `(a,b)`, `(b,c)`, and `(c,a)`, with the
first-listed candidate represented by `+1`.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.rankingPreference_isNAE3 (r : FABL.Ranking3) :
  FABL.IsNAE3 (FABL.rankingPreference r)
    theorem FABL.rankingPreference_isNAE3
  (r : FABL.Ranking3) :
  FABL.IsNAE3 (FABL.rankingPreference r)
    Every strict three-candidate ranking gives one of the six satisfying inputs of `NAE₃`.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.exists_rankingPreference_eq_iff_isNAE3
  (w : FABL.PairwiseContest → FABL.Sign) :
  (∃ r, FABL.rankingPreference r = w) ↔ FABL.IsNAE3 w
    theorem FABL.exists_rankingPreference_eq_iff_isNAE3
  (w : FABL.PairwiseContest → FABL.Sign) :
  (∃ r, FABL.rankingPreference r = w) ↔
    FABL.IsNAE3 w
    O'Donnell, Exercise 1.1(i): the satisfying inputs of `NAE₃` are exactly the six strict
rankings.
Definition2.5.2
uses 1used by 1✓L∃∀N
Tagssection-2-5supportfidelity-exact

Three-candidate Condorcet model. Let the candidates be a,b,c and let f:\{-1,1\}^n\to\{-1,1\} be a two-candidate voting rule. Write x,y,z\in\{-1,1\}^n for the voters' pairwise preferences in the elections a versus b, b versus c, and c versus a, respectively, with the first-listed candidate encoded by +1. Each voter's strict ranking is therefore encoded by one of the six triples satisfying \operatorname{NAE}_3. The three societal pairwise outcomes are (f(x),f(y),f(z)).

Lean code for Definition2.5.2●6 declarations
  • abbrevdefined in FABL/Chapter02/Arrow.lean
    complete
    abbrev FABL.PairwiseContest : Type
    abbrev FABL.PairwiseContest : Type
    The three pairwise contests `(a,b)`, `(b,c)`, and `(c,a)`.
  • abbrevdefined in FABL/Chapter02/Arrow.lean
    complete
    abbrev FABL.RankingProfile (n : ℕ) : Type
    abbrev FABL.RankingProfile (n : ℕ) : Type
    O'Donnell's three-candidate preference profile: one strict ranking per voter.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.pairwiseVotes {n : ℕ} (p : FABL.RankingProfile n)
  (c : FABL.PairwiseContest) : FABL.SignCube n
    def FABL.pairwiseVotes {n : ℕ}
  (p : FABL.RankingProfile n)
  (c : FABL.PairwiseContest) :
  FABL.SignCube n
    The sign-cube of votes in one pairwise contest extracted from a ranking profile.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.societalOutcome {n : ℕ} (f : FABL.BooleanFunction n)
  (p : FABL.RankingProfile n) : FABL.PairwiseContest → FABL.Sign
    def FABL.societalOutcome {n : ℕ}
  (f : FABL.BooleanFunction n)
  (p : FABL.RankingProfile n) :
  FABL.PairwiseContest → FABL.Sign
    The three societal pairwise outcomes produced by the same two-candidate rule.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.SatisfiesIIA {n : ℕ}
  (F : FABL.RankingProfile n → FABL.PairwiseContest → FABL.Sign) : Prop
    def FABL.SatisfiesIIA {n : ℕ}
  (F :
    FABL.RankingProfile n →
      FABL.PairwiseContest → FABL.Sign) :
  Prop
    Independence of irrelevant alternatives for a three-candidate social aggregation rule.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.societalOutcome_satisfiesIIA {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.SatisfiesIIA (FABL.societalOutcome f)
    theorem FABL.societalOutcome_satisfiesIIA {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.SatisfiesIIA
    (FABL.societalOutcome f)
    Applying one fixed two-candidate voting rule separately to every contest satisfies IIA by
construction.
Definition2.5.3
uses 1
Used by 3
Reverse dependency previews
Preview
Theorem 2.5.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-5fidelity-exact

Definition 2.55. In an election employing Condorcet's method with voting rule f:\{-1,1\}^n\to\{-1,1\}, a candidate is a Condorcet winner if it wins every pairwise election in which it participates.

For three candidates, there is no Condorcet winner precisely when the societal outcome (f(x),f(y),f(z)) is one of the two all-equal triples (-1,-1,-1) and (+1,+1,+1); this event is Condorcet's Paradox.

Lean code for Definition2.5.3●4 declarations
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.IsCondorcetWinner (w : FABL.PairwiseContest → FABL.Sign)
  (c : Fin 3) : Prop
    def FABL.IsCondorcetWinner
  (w : FABL.PairwiseContest → FABL.Sign)
  (c : Fin 3) : Prop
    O'Donnell, Definition 2.55: candidate `c` wins both pairwise contests in which it
participates. Candidates `0`, `1`, and `2` denote `a`, `b`, and `c`.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.HasCondorcetWinner (w : FABL.PairwiseContest → FABL.Sign) : Prop
    def FABL.HasCondorcetWinner
  (w : FABL.PairwiseContest → FABL.Sign) :
  Prop
    A societal outcome has a Condorcet winner.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.HasSocietalCondorcetWinner {n : ℕ} (f : FABL.BooleanFunction n)
  (p : FABL.RankingProfile n) : Prop
    def FABL.HasSocietalCondorcetWinner {n : ℕ}
  (f : FABL.BooleanFunction n)
  (p : FABL.RankingProfile n) : Prop
    The event that the societal pairwise outcome has a Condorcet winner.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.hasCondorcetWinner_iff_isNAE3
  (w : FABL.PairwiseContest → FABL.Sign) :
  FABL.HasCondorcetWinner w ↔ FABL.IsNAE3 w
    theorem FABL.hasCondorcetWinner_iff_isNAE3
  (w : FABL.PairwiseContest → FABL.Sign) :
  FABL.HasCondorcetWinner w ↔
    FABL.IsNAE3 w
    O'Donnell, Definition 2.55: a three-candidate outcome has a Condorcet winner exactly when
it is not one of the two all-equal cyclic outcomes.
Theorem2.5.4
Statement uses 6
Statement dependency previews
Preview
Definition 2.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-5fidelity-exact

Arrow's Theorem. Suppose f:\{-1,1\}^n\to\{-1,1\} is a unanimous voting rule used in a three-candidate Condorcet election. If every profile of voters' strict rankings has a Condorcet winner, then f is a dictatorship: there exists i\in[n] such that f(x)=\chi_i(x)=x_i for every x\in\{-1,1\}^n.

Lean code for Theorem2.5.4●1 theorem
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.arrowsTheorem {n : ℕ} (f : FABL.BooleanFunction n)
  (hunanimous : FABL.IsUnanimous f)
  (hwinner :
    ∀ (p : FABL.RankingProfile n),
      FABL.HasSocietalCondorcetWinner f p) :
  ∃ i, f = FABL.dictator i
    theorem FABL.arrowsTheorem {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hunanimous : FABL.IsUnanimous f)
  (hwinner :
    ∀ (p : FABL.RankingProfile n),
      FABL.HasSocietalCondorcetWinner f
        p) :
  ∃ i, f = FABL.dictator i
    Arrow's Theorem for the common-rule three-candidate Condorcet model.
Lemma2.5.5
Statement uses 5
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-5supportfidelity-exact

Kalai's Condorcet calculation. Under impartial culture for a three-candidate election, the triples (\boldsymbol x_i,\boldsymbol y_i,\boldsymbol z_i) are independent across i and are each uniform on the six satisfying inputs of \operatorname{NAE}_3. Moreover, \Pr[\text{there is a Condorcet winner}] =\mathbb E[\operatorname{NAE}_3( f(\boldsymbol x),f(\boldsymbol y),f(\boldsymbol z))], \tag{2.8} the multilinear expansion is \operatorname{NAE}_3(w_1,w_2,w_3) =\frac34-\frac14w_1w_2-\frac14w_1w_3-\frac14w_2w_3, and each of (\boldsymbol x,\boldsymbol y), (\boldsymbol x,\boldsymbol z), and (\boldsymbol y,\boldsymbol z) is a (-1/3)-correlated pair.

Lean code for Lemma2.5.5●9 declarations
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.expect_rankingPreference (c : FABL.PairwiseContest) :
  (Finset.univ.expect fun r =>
      FABL.signValue (FABL.rankingPreference r c)) =
    0
    theorem FABL.expect_rankingPreference
  (c : FABL.PairwiseContest) :
  (Finset.univ.expect fun r =>
      FABL.signValue
        (FABL.rankingPreference r c)) =
    0
    Under impartial culture, each one of the three pairwise preferences is unbiased.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.expect_rankingPreference_mul (a b : FABL.PairwiseContest)
  (hab : a ≠ b) :
  (Finset.univ.expect fun r =>
      FABL.signValue (FABL.rankingPreference r a) *
        FABL.signValue (FABL.rankingPreference r b)) =
    -1 / 3
    theorem FABL.expect_rankingPreference_mul
  (a b : FABL.PairwiseContest)
  (hab : a ≠ b) :
  (Finset.univ.expect fun r =>
      FABL.signValue
          (FABL.rankingPreference r a) *
        FABL.signValue
          (FABL.rankingPreference r b)) =
    -1 / 3
    Under impartial culture, any two distinct pairwise preferences have correlation `-1/3`.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.expect_rankingProfile_prod {n : ℕ}
  (q : Fin n → FABL.Ranking3 → ℝ) :
  (Finset.univ.expect fun p => ∏ i, q i (p i)) =
    ∏ i, Finset.univ.expect fun r => q i r
    theorem FABL.expect_rankingProfile_prod {n : ℕ}
  (q : Fin n → FABL.Ranking3 → ℝ) :
  (Finset.univ.expect fun p =>
      ∏ i, q i (p i)) =
    ∏ i, Finset.univ.expect fun r => q i r
    Uniform expectation on a finite product factors for coordinatewise products.
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.nae3Indicator (w : FABL.PairwiseContest → FABL.Sign) : ℝ
    def FABL.nae3Indicator
  (w : FABL.PairwiseContest → FABL.Sign) :
  ℝ
    The real-valued indicator of the three-bit not-all-equal predicate.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.nae3Indicator_eq_polynomial
  (w : FABL.PairwiseContest → FABL.Sign) :
  FABL.nae3Indicator w =
    3 / 4 - 1 / 4 * FABL.signValue (w 0) * FABL.signValue (w 1) -
        1 / 4 * FABL.signValue (w 0) * FABL.signValue (w 2) -
      1 / 4 * FABL.signValue (w 1) * FABL.signValue (w 2)
    theorem FABL.nae3Indicator_eq_polynomial
  (w : FABL.PairwiseContest → FABL.Sign) :
  FABL.nae3Indicator w =
    3 / 4 -
          1 / 4 * FABL.signValue (w 0) *
            FABL.signValue (w 1) -
        1 / 4 * FABL.signValue (w 0) *
          FABL.signValue (w 2) -
      1 / 4 * FABL.signValue (w 1) *
        FABL.signValue (w 2)
    The multilinear expansion of `NAE₃` used in Kalai's proof.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.expect_monomial_pairwiseVotes_mul {n : ℕ}
  (a b : FABL.PairwiseContest) (hab : a ≠ b) (S T : Finset (Fin n)) :
  (Finset.univ.expect fun p =>
      FABL.monomial S (FABL.pairwiseVotes p a) *
        FABL.monomial T (FABL.pairwiseVotes p b)) =
    if S = T then (-1 / 3) ^ S.card else 0
    theorem FABL.expect_monomial_pairwiseVotes_mul
  {n : ℕ} (a b : FABL.PairwiseContest)
  (hab : a ≠ b) (S T : Finset (Fin n)) :
  (Finset.univ.expect fun p =>
      FABL.monomial S
          (FABL.pairwiseVotes p a) *
        FABL.monomial T
          (FABL.pairwiseVotes p b)) =
    if S = T then (-1 / 3) ^ S.card else 0
    Walsh monomials evaluated on two distinct pairwise contests have the orthogonality law of a
`(-1/3)`-correlated pair.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.expect_pairwiseVotes_mul_eq_fourier_sum {n : ℕ}
  (a b : FABL.PairwiseContest) (hab : a ≠ b)
  (f g : FABL.SignCube n → ℝ) :
  (Finset.univ.expect fun p =>
      f (FABL.pairwiseVotes p a) * g (FABL.pairwiseVotes p b)) =
    ∑ S,
      (-1 / 3) ^ S.card * FABL.fourierCoeff f S * FABL.fourierCoeff g S
    theorem FABL.expect_pairwiseVotes_mul_eq_fourier_sum
  {n : ℕ} (a b : FABL.PairwiseContest)
  (hab : a ≠ b)
  (f g : FABL.SignCube n → ℝ) :
  (Finset.univ.expect fun p =>
      f (FABL.pairwiseVotes p a) *
        g (FABL.pairwiseVotes p b)) =
    ∑ S,
      (-1 / 3) ^ S.card *
          FABL.fourierCoeff f S *
        FABL.fourierCoeff g S
    Under impartial culture, evaluating arbitrary real functions on two distinct pairwise
contests gives their `(-1/3)` Fourier correlation.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.expect_pairwiseVotes_mul_eq_noiseStability {n : ℕ}
  (a b : FABL.PairwiseContest) (hab : a ≠ b)
  (f : FABL.BooleanFunction n) :
  (Finset.univ.expect fun p =>
      f.toReal (FABL.pairwiseVotes p a) *
        f.toReal (FABL.pairwiseVotes p b)) =
    FABL.noiseStability (-1 / 3) FABL.neg_one_third_mem_Icc f.toReal
    theorem FABL.expect_pairwiseVotes_mul_eq_noiseStability
  {n : ℕ} (a b : FABL.PairwiseContest)
  (hab : a ≠ b)
  (f : FABL.BooleanFunction n) :
  (Finset.univ.expect fun p =>
      f.toReal (FABL.pairwiseVotes p a) *
        f.toReal
          (FABL.pairwiseVotes p b)) =
    FABL.noiseStability (-1 / 3)
      FABL.neg_one_third_mem_Icc f.toReal
    The profile correlation of `f` on any two distinct contests is its noise stability at
correlation `-1/3`.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.condorcetWinnerIndicator_eq_nae3 {n : ℕ}
  (f : FABL.BooleanFunction n) (p : FABL.RankingProfile n) :
  (if FABL.HasSocietalCondorcetWinner f p then 1 else 0) =
    FABL.nae3Indicator (FABL.societalOutcome f p)
    theorem FABL.condorcetWinnerIndicator_eq_nae3
  {n : ℕ} (f : FABL.BooleanFunction n)
  (p : FABL.RankingProfile n) :
  (if
        FABL.HasSocietalCondorcetWinner f
          p then
      1
    else 0) =
    FABL.nae3Indicator
      (FABL.societalOutcome f p)
    The Condorcet-winner indicator is `NAE₃` applied to the three societal outcomes.
Theorem2.5.6
Statement uses 4
Statement dependency previews
Preview
Definition 2.1.13
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 2.5.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-5fidelity-exact

Theorem 2.56. Consider a three-candidate Condorcet election using f:\{-1,1\}^n\to\{-1,1\}. Under the impartial culture assumption, the probability of a Condorcet winner is exactly \frac34-\frac34\operatorname{Stab}_{-1/3}[f].

Lean code for Theorem2.5.6●2 declarations
  • defdefined in FABL/Chapter02/Arrow.lean
    complete
    def FABL.condorcetWinnerProbability {n : ℕ} (f : FABL.BooleanFunction n) : ℝ
    def FABL.condorcetWinnerProbability {n : ℕ}
  (f : FABL.BooleanFunction n) : ℝ
    O'Donnell, Equation (2.8): under impartial culture, the probability of a Condorcet winner
is a uniform expectation over strict-ranking profiles.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.condorcetWinnerProbability_eq_noiseStability {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.condorcetWinnerProbability f =
    3 / 4 -
      3 / 4 *
        FABL.noiseStability (-1 / 3) FABL.neg_one_third_mem_Icc f.toReal
    theorem FABL.condorcetWinnerProbability_eq_noiseStability
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.condorcetWinnerProbability f =
    3 / 4 -
      3 / 4 *
        FABL.noiseStability (-1 / 3)
          FABL.neg_one_third_mem_Icc
          f.toReal
    O'Donnell, Theorem 2.56: under impartial culture, the probability of a Condorcet winner is
`3/4 - (3/4) Stab_{-1/3}[f]`.
Theorem2.5.7
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 0✓L∃∀N
Tagssection-2-5fidelity-exact

Guilbaud's Formula. In a three-candidate Condorcet election using \operatorname{Maj}_n, the probability of a Condorcet winner tends, as odd n tends to infinity, to \frac{3}{2\pi}\arccos(-1/3)\approx91.2\%.

Lean code for Theorem2.5.7●1 theorem
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.tendsto_condorcetWinnerProbability_majority_odd :
  Filter.Tendsto
    (fun k =>
      FABL.condorcetWinnerProbability (FABL.majority (2 * k + 1)))
    Filter.atTop (nhds (3 / (2 * Real.pi) * Real.arccos (-1 / 3)))
    theorem FABL.tendsto_condorcetWinnerProbability_majority_odd :
  Filter.Tendsto
    (fun k =>
      FABL.condorcetWinnerProbability
        (FABL.majority (2 * k + 1)))
    Filter.atTop
    (nhds
      (3 / (2 * Real.pi) *
        Real.arccos (-1 / 3)))
    Guilbaud's Formula: for odd-arity majority rules, the probability of a Condorcet winner
converges to `3 / (2π) * arccos (-1/3)`.
Theorem2.5.8
Statement uses 2
Statement dependency previews
Preview
Proposition 2.5.10
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-5fidelity-exact

Theorem 2.57. In a three-candidate Condorcet election using a rule f:\{-1,1\}^n\to\{-1,1\} whose singleton Fourier coefficients \widehat f(i) are all equal, the probability of a Condorcet winner is at most \frac79+\frac{4}{9\pi}+o_n(1)\approx91.9\%.

Lean code for Theorem2.5.8●4 theorems
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.condorcetWinnerProbability_le_of_equalSingletonFourierCoefficients
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf : FABL.HasEqualSingletonFourierCoefficients f) (hn : 0 < n) :
  FABL.condorcetWinnerProbability f ≤
    7 / 9 + 4 / (9 * Real.pi) + 2 / 3 / ↑n
    theorem FABL.condorcetWinnerProbability_le_of_equalSingletonFourierCoefficients
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf :
    FABL.HasEqualSingletonFourierCoefficients
      f)
  (hn : 0 < n) :
  FABL.condorcetWinnerProbability f ≤
    7 / 9 + 4 / (9 * Real.pi) + 2 / 3 / ↑n
    The finite explicit estimate underlying O'Donnell's Theorem 2.57.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.two_thirds_div_nat_isLittleO_one :
  (fun n => 2 / 3 / ↑n) =o[Filter.atTop] fun _n => 1
    theorem FABL.two_thirds_div_nat_isLittleO_one :
  (fun n => 2 / 3 / ↑n) =o[Filter.atTop]
    fun _n => 1
    The explicit remainder in Theorem 2.57 is little-oh of one.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.exists_condorcetWinnerProbability_upperError_isLittleO
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf : ∀ (n : ℕ), FABL.HasEqualSingletonFourierCoefficients (f n)) :
  ∃ r,
    (r =o[Filter.atTop] fun _n => 1) ∧
      ∀ᶠ (n : ℕ) in Filter.atTop,
        FABL.condorcetWinnerProbability (f n) ≤
          7 / 9 + 4 / (9 * Real.pi) + r n
    theorem FABL.exists_condorcetWinnerProbability_upperError_isLittleO
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf :
    ∀ (n : ℕ),
      FABL.HasEqualSingletonFourierCoefficients
        (f n)) :
  ∃ r,
    (r =o[Filter.atTop] fun _n => 1) ∧
      ∀ᶠ (n : ℕ) in Filter.atTop,
        FABL.condorcetWinnerProbability
            (f n) ≤
          7 / 9 + 4 / (9 * Real.pi) + r n
    O'Donnell, Theorem 2.57 in its literal
`7/9 + 4/(9π) + o_n(1)` formulation.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.condorcetWinnerProbability_eventually_le_seven_ninths_add_four_div_nine_pi_add
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf : ∀ (n : ℕ), FABL.HasEqualSingletonFourierCoefficients (f n))
  {ε : ℝ} (hε : 0 < ε) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    FABL.condorcetWinnerProbability (f n) ≤
      7 / 9 + 4 / (9 * Real.pi) + ε
    theorem FABL.condorcetWinnerProbability_eventually_le_seven_ninths_add_four_div_nine_pi_add
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf :
    ∀ (n : ℕ),
      FABL.HasEqualSingletonFourierCoefficients
        (f n))
  {ε : ℝ} (hε : 0 < ε) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    FABL.condorcetWinnerProbability
        (f n) ≤
      7 / 9 + 4 / (9 * Real.pi) + ε
    The epsilon-eventual form of O'Donnell's Theorem 2.57.
Lemma2.5.9
uses 1used by 1✓L∃∀N
Tagssection-2-5supportfidelity-exact

Exercise 2.24. Prove Proposition 2.58 with O(n^{-1}) in place of o_n(1). The suggested estimate, obtained using Theorem 2.33, is \widehat f(i) \le \frac{\sqrt{2/\pi}}{\sqrt n}+O(n^{-3/2}) for every i\in[n] when all singleton Fourier coefficients are equal.

Lean code for Lemma2.5.9●8 declarations
  • defdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    def FABL.HasEqualSingletonFourierCoefficients {n : ℕ}
  (f : FABL.BooleanFunction n) : Prop
    def FABL.HasEqualSingletonFourierCoefficients
  {n : ℕ} (f : FABL.BooleanFunction n) :
  Prop
    All singleton Fourier coefficients of a Boolean function are equal.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.sum_fourierCoeff_singleton_neg {n : ℕ}
  (f : FABL.BooleanFunction n) :
  ∑ i, FABL.fourierCoeff (-f).toReal {i} =
    -∑ i, FABL.fourierCoeff f.toReal {i}
    theorem FABL.sum_fourierCoeff_singleton_neg
  {n : ℕ} (f : FABL.BooleanFunction n) :
  ∑ i, FABL.fourierCoeff (-f).toReal {i} =
    -∑ i, FABL.fourierCoeff f.toReal {i}
    Negating a Boolean function negates the sum of its singleton Fourier coefficients.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.abs_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.abs_sum_fourierCoeff_singleton_le_majority
  {n : ℕ} (f : FABL.BooleanFunction n) :
  |∑ i, FABL.fourierCoeff f.toReal {i}| ≤
    ∑ i,
      FABL.fourierCoeff
        (FABL.majority n).toReal {i}
    The absolute singleton-coefficient sum of any Boolean function is at most majority's
singleton-coefficient sum.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_le_totalInfluence_majority_sq_div {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : FABL.HasEqualSingletonFourierCoefficients f) (hn : 0 < n) :
  FABL.fourierWeightAtLevel 1 f.toReal ≤
    FABL.totalInfluence (FABL.majority n).toReal ^ 2 / ↑n
    theorem FABL.fourierWeightAtLevel_one_le_totalInfluence_majority_sq_div
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf :
    FABL.HasEqualSingletonFourierCoefficients
      f)
  (hn : 0 < n) :
  FABL.fourierWeightAtLevel 1 f.toReal ≤
    FABL.totalInfluence
          (FABL.majority n).toReal ^
        2 /
      ↑n
    If all singleton coefficients are equal, level-one weight is bounded by majority's squared
total influence divided by the arity.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.totalInfluence_majority_odd_sq_div_card (m : ℕ) :
  FABL.totalInfluence (FABL.majority (2 * m + 1)).toReal ^ 2 /
      ↑(2 * m + 1) =
    FABL.fourierWeightAtLevel 1 (FABL.majority (2 * m + 1)).toReal
    theorem FABL.totalInfluence_majority_odd_sq_div_card
  (m : ℕ) :
  FABL.totalInfluence
          (FABL.majority
              (2 * m + 1)).toReal ^
        2 /
      ↑(2 * m + 1) =
    FABL.fourierWeightAtLevel 1
      (FABL.majority (2 * m + 1)).toReal
    The squared total influence of odd majority, divided by its arity, is its level-one Fourier
weight.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.totalInfluence_majority_sq_div_card_le (n : ℕ) (hn : 0 < n) :
  FABL.totalInfluence (FABL.majority n).toReal ^ 2 / ↑n ≤
    2 / Real.pi + 3 / ↑n
    theorem FABL.totalInfluence_majority_sq_div_card_le
  (n : ℕ) (hn : 0 < n) :
  FABL.totalInfluence
          (FABL.majority n).toReal ^
        2 /
      ↑n ≤
    2 / Real.pi + 3 / ↑n
    The majority quotient needed for Exercise 2.24 has the uniform explicit `O(1/n)` bound
`2/π + 3/n`.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_le_two_div_pi_add_three_div_card {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hf : FABL.HasEqualSingletonFourierCoefficients f) (hn : 0 < n) :
  FABL.fourierWeightAtLevel 1 f.toReal ≤ 2 / Real.pi + 3 / ↑n
    theorem FABL.fourierWeightAtLevel_one_le_two_div_pi_add_three_div_card
  {n : ℕ} (f : FABL.BooleanFunction n)
  (hf :
    FABL.HasEqualSingletonFourierCoefficients
      f)
  (hn : 0 < n) :
  FABL.fourierWeightAtLevel 1 f.toReal ≤
    2 / Real.pi + 3 / ↑n
    O'Donnell, Exercise 2.24: equal singleton coefficients imply the explicit strengthened
bound `W¹[f] ≤ 2/π + 3/n`.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.three_div_nat_isLittleO_one :
  (fun n => 3 / ↑n) =o[Filter.atTop] fun _n => 1
    theorem FABL.three_div_nat_isLittleO_one :
  (fun n => 3 / ↑n) =o[Filter.atTop]
    fun _n => 1
    The explicit `3/n` remainder in Exercise 2.24 is little-oh of one.
Proposition2.5.10
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-2-5fidelity-exact

Proposition 2.58. Suppose f:\{-1,1\}^n\to\{-1,1\} has all singleton Fourier coefficients \widehat f(i) equal. Then \mathbf W^1[f]\le\frac2\pi+o_n(1). Exercise 2.24 asks for the stronger error term O(n^{-1}).

Lean code for Proposition2.5.10●2 theorems
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.exists_levelOneWeight_upperError_isLittleO
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf : ∀ (n : ℕ), FABL.HasEqualSingletonFourierCoefficients (f n)) :
  ∃ r,
    (r =o[Filter.atTop] fun _n => 1) ∧
      ∀ᶠ (n : ℕ) in Filter.atTop,
        FABL.fourierWeightAtLevel 1 (f n).toReal ≤ 2 / Real.pi + r n
    theorem FABL.exists_levelOneWeight_upperError_isLittleO
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf :
    ∀ (n : ℕ),
      FABL.HasEqualSingletonFourierCoefficients
        (f n)) :
  ∃ r,
    (r =o[Filter.atTop] fun _n => 1) ∧
      ∀ᶠ (n : ℕ) in Filter.atTop,
        FABL.fourierWeightAtLevel 1
            (f n).toReal ≤
          2 / Real.pi + r n
    O'Donnell, Proposition 2.58 in literal `2/π + o_n(1)` form for a family of Boolean
functions with equal singleton coefficients.
  • theoremdefined in FABL/Chapter02/ArrowLevelOneBound.lean
    complete
    theorem FABL.fourierWeightAtLevel_one_eventually_le_two_div_pi_add
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf : ∀ (n : ℕ), FABL.HasEqualSingletonFourierCoefficients (f n))
  {ε : ℝ} (hε : 0 < ε) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    FABL.fourierWeightAtLevel 1 (f n).toReal ≤ 2 / Real.pi + ε
    theorem FABL.fourierWeightAtLevel_one_eventually_le_two_div_pi_add
  (f : (n : ℕ) → FABL.BooleanFunction n)
  (hf :
    ∀ (n : ℕ),
      FABL.HasEqualSingletonFourierCoefficients
        (f n))
  {ε : ℝ} (hε : 0 < ε) :
  ∀ᶠ (n : ℕ) in Filter.atTop,
    FABL.fourierWeightAtLevel 1
        (f n).toReal ≤
      2 / Real.pi + ε
    The epsilon-eventual formulation of Proposition 2.58.
Corollary2.5.11
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 2
Reverse dependency previews
Preview
Theorem 2.5.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-5fidelity-exact

Corollary 2.59. In a three-candidate Condorcet election using f:\{-1,1\}^n\to\{-1,1\}, the probability of a Condorcet winner is at most \frac79+\frac29\mathbf W^1[f].

Lean code for Corollary2.5.11●1 theorem
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.condorcetWinnerProbability_le {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.condorcetWinnerProbability f ≤
    7 / 9 + 2 / 9 * FABL.fourierWeightAtLevel 1 f.toReal
    theorem FABL.condorcetWinnerProbability_le {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.condorcetWinnerProbability f ≤
    7 / 9 +
      2 / 9 *
        FABL.fourierWeightAtLevel 1
          f.toReal
    O'Donnell, Corollary 2.59: the probability of a Condorcet winner is bounded by the
level-one Fourier weight.
Corollary2.5.12
Statement uses 3
Statement dependency previews
Preview
Definition 1.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
Tagssection-2-5fidelity-exact

Corollary 2.60. Suppose that, in a three-candidate Condorcet election using f:\{-1,1\}^n\to\{-1,1\}, the probability of a Condorcet winner is 1-\epsilon. Then there is an i\in[n] and a sign \sigma\in\{-1,1\} such that \operatorname{dist}(f,\sigma\chi_i)=O(\epsilon).

Lean code for Corollary2.5.12●2 theorems
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.exists_signedDictator_relativeHammingDist_le_of_condorcetWinnerProbability_eq_one_sub
  {n : ℕ} (f : FABL.BooleanFunction n) (ε : ℝ)
  (hprobability : FABL.condorcetWinnerProbability f = 1 - ε)
  (hε₀ : 0 ≤ ε) (hε : 9 / 2 * ε ≤ 1 / 1600) :
  ∃ i negated,
    FABL.relativeHammingDist f (FABL.signedDictator i negated) ≤
      1601 * (9 / 2) * ε
    theorem FABL.exists_signedDictator_relativeHammingDist_le_of_condorcetWinnerProbability_eq_one_sub
  {n : ℕ} (f : FABL.BooleanFunction n)
  (ε : ℝ)
  (hprobability :
    FABL.condorcetWinnerProbability f =
      1 - ε)
  (hε₀ : 0 ≤ ε)
  (hε : 9 / 2 * ε ≤ 1 / 1600) :
  ∃ i negated,
    FABL.relativeHammingDist f
        (FABL.signedDictator i negated) ≤
      1601 * (9 / 2) * ε
    O'Donnell, Corollary 2.60, with the explicit constant supplied by `fkn`: if the
Condorcet-winner probability is `1 - ε` and `(9 / 2) * ε ≤ 1 / 1600`, then the voting
rule is within `1601 * (9 / 2) * ε` of a signed dictator.
  • theoremdefined in FABL/Chapter02/Arrow.lean
    complete
    theorem FABL.relativeHammingDist_signedDictator_family_isBigO_of_condorcetWinnerProbability_eq_one_sub.{u_1}
  {ι : Type u_1} (l : Filter ι) (arity : ι → ℕ)
  (f : (t : ι) → FABL.BooleanFunction (arity t)) (ε : ι → ℝ)
  (hprobability :
    ∀ (t : ι), FABL.condorcetWinnerProbability (f t) = 1 - ε t)
  (hε₀ : ∀ (t : ι), 0 ≤ ε t) (hε : ∀ (t : ι), 9 / 2 * ε t ≤ 1 / 1600) :
  ∃ i negated,
    (fun t =>
        FABL.relativeHammingDist (f t)
          (FABL.signedDictator (i t) (negated t))) =O[l]
      ε
    theorem FABL.relativeHammingDist_signedDictator_family_isBigO_of_condorcetWinnerProbability_eq_one_sub.{u_1}
  {ι : Type u_1} (l : Filter ι)
  (arity : ι → ℕ)
  (f :
    (t : ι) →
      FABL.BooleanFunction (arity t))
  (ε : ι → ℝ)
  (hprobability :
    ∀ (t : ι),
      FABL.condorcetWinnerProbability
          (f t) =
        1 - ε t)
  (hε₀ : ∀ (t : ι), 0 ≤ ε t)
  (hε :
    ∀ (t : ι), 9 / 2 * ε t ≤ 1 / 1600) :
  ∃ i negated,
    (fun t =>
        FABL.relativeHammingDist (f t)
          (FABL.signedDictator (i t)
            (negated t))) =O[l]
      ε
    O'Donnell, Corollary 2.60 in its literal uniform family formulation: when the
Condorcet-winner deficit is `ε`, the distance to a suitable signed dictator is `O(ε)`.
Theorem2.5.13
Statement uses 3
Statement dependency previews
Preview
Definition 1.4.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N
Tagssection-2-5fidelity-exact

Friedgut-Kalai-Naor (FKN) Theorem. Suppose f:\{-1,1\}^n\to\{-1,1\} satisfies \mathbf W^1[f]\ge1-\delta. Then there is an i\in[n] and a sign \sigma\in\{-1,1\} such that \operatorname{dist}(f,\sigma\chi_i)=O(\delta). The book proves this theorem in Chapter 9.1. It later improves the distance bound in Chapter 5.4 to \delta/4+O(\delta^2\log(2/\delta)).

Lean code for Theorem2.5.13●3 declarations
  • defdefined in FABL/Chapter02/FKN.lean
    complete
    def FABL.signedDictator {n : ℕ} (i : Fin n) (negated : Bool) :
  FABL.BooleanFunction n
    def FABL.signedDictator {n : ℕ} (i : Fin n)
  (negated : Bool) :
  FABL.BooleanFunction n
    A dictator or its negation, selected by a Boolean flag.
  • theoremdefined in FABL/Chapter02/FKN.lean
    complete
    theorem FABL.fkn {n : ℕ} (f : FABL.BooleanFunction n) (δ : ℝ) (hδ₀ : 0 ≤ δ)
  (hδ : δ ≤ 1 / 1600)
  (hweight : 1 - δ ≤ FABL.fourierWeightAtLevel 1 f.toReal) :
  ∃ i negated,
    FABL.relativeHammingDist f (FABL.signedDictator i negated) ≤
      1601 * δ
    theorem FABL.fkn {n : ℕ}
  (f : FABL.BooleanFunction n) (δ : ℝ)
  (hδ₀ : 0 ≤ δ) (hδ : δ ≤ 1 / 1600)
  (hweight :
    1 - δ ≤
      FABL.fourierWeightAtLevel 1
        f.toReal) :
  ∃ i negated,
    FABL.relativeHammingDist f
        (FABL.signedDictator i negated) ≤
      1601 * δ
    Friedgut--Kalai--Naor (FKN): if the level-one Fourier weight is at least `1 - δ`, then
the function is within `1601 * δ` of a signed dictator. The positivity of the arity follows
from the hypotheses and is not an extra assumption.
  • theoremdefined in FABL/Chapter02/FKN.lean
    complete
    theorem FABL.fkn_family_isBigO.{u_1} {ι : Type u_1} (l : Filter ι)
  (arity : ι → ℕ) (f : (t : ι) → FABL.BooleanFunction (arity t))
  (δ : ι → ℝ) (hδ₀ : ∀ (t : ι), 0 ≤ δ t)
  (hδ : ∀ (t : ι), δ t ≤ 1 / 1600)
  (hweight :
    ∀ (t : ι), 1 - δ t ≤ FABL.fourierWeightAtLevel 1 (f t).toReal) :
  ∃ i negated,
    (fun t =>
        FABL.relativeHammingDist (f t)
          (FABL.signedDictator (i t) (negated t))) =O[l]
      δ
    theorem FABL.fkn_family_isBigO.{u_1}
  {ι : Type u_1} (l : Filter ι)
  (arity : ι → ℕ)
  (f :
    (t : ι) →
      FABL.BooleanFunction (arity t))
  (δ : ι → ℝ) (hδ₀ : ∀ (t : ι), 0 ≤ δ t)
  (hδ : ∀ (t : ι), δ t ≤ 1 / 1600)
  (hweight :
    ∀ (t : ι),
      1 - δ t ≤
        FABL.fourierWeightAtLevel 1
          (f t).toReal) :
  ∃ i negated,
    (fun t =>
        FABL.relativeHammingDist (f t)
          (FABL.signedDictator (i t)
            (negated t))) =O[l]
      δ
    The literal uniform `O(δ)` family formulation of FKN, with constant `1601`.