Analysis of Boolean Functions in Lean

2.1. Social choice functions🔗

Definition2.1.1
uses 0
Used by 7
Reverse dependency previews
Preview
Definition 2.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.1. For odd n, the majority function \operatorname{Maj}_n:\{-1,1\}^n\to\{-1,1\} is \operatorname{Maj}_n(x)=\operatorname{sgn}(x_1+x_2+\cdots+x_n). Occasionally, when n is even, a function is called a majority function if its value is the sign of x_1+\cdots+x_n whenever this sum is nonzero.

Lean code for Definition2.1.1●4 declarations
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.thresholdSign (t : ℝ) : FABL.Sign
    def FABL.thresholdSign (t : ℝ) : FABL.Sign
    The book's sign convention: `sgn(t) = 1` for `t ≥ 0` and `-1` otherwise.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.majority (n : ℕ) : FABL.BooleanFunction n
    def FABL.majority (n : ℕ) :
  FABL.BooleanFunction n
    O'Donnell, Definition 2.1: the majority function, with ties resolved as `+1`.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.IsMajorityFunction {n : ℕ} (f : FABL.BooleanFunction n) : Prop
    def FABL.IsMajorityFunction {n : ℕ}
  (f : FABL.BooleanFunction n) : Prop
    O'Donnell, Definition 2.1: a Boolean rule is a majority function when it agrees with the
sign of the vote margin away from tied profiles.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    theorem FABL.majority_isMajorityFunction (n : ℕ) :
  FABL.IsMajorityFunction (FABL.majority n)
    theorem FABL.majority_isMajorityFunction (n : ℕ) :
  FABL.IsMajorityFunction
    (FABL.majority n)
    The canonical tie-to-`+1` majority rule is a majority function.
Definition2.1.2
uses 0
Used by 3
Reverse dependency previews
Preview
Definition 2.1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.2. The function \operatorname{AND}_n:\{-1,1\}^n\to\{-1,1\} is +1 unless x=(-1,-1,\ldots,-1). The function \operatorname{OR}_n:\{-1,1\}^n\to\{-1,1\} is -1 unless x=(+1,+1,\ldots,+1).

Lean code for Definition2.1.2●2 definitions
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.andFunction (n : ℕ) : FABL.BooleanFunction n
    def FABL.andFunction (n : ℕ) :
  FABL.BooleanFunction n
    O'Donnell, Definition 2.2: Boolean AND in the book's `-1 = True` convention.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.orFunction (n : ℕ) : FABL.BooleanFunction n
    def FABL.orFunction (n : ℕ) :
  FABL.BooleanFunction n
    O'Donnell, Definition 2.2: Boolean OR in the book's `-1 = True` convention.
Definition2.1.3
uses 1
Used by 5
Reverse dependency previews
Preview
Lemma 2.1.11
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.3. The ith dictator function \chi_i:\{-1,1\}^n\to\{-1,1\} is \chi_i(x)=x_i. Here \chi_i abbreviates the singleton parity function \chi_{\{i\}}.

Lean code for Definition2.1.3●2 declarations
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.dictator {n : ℕ} (i : Fin n) : FABL.BooleanFunction n
    def FABL.dictator {n : ℕ} (i : Fin n) :
  FABL.BooleanFunction n
    O'Donnell, Definition 2.3: the `i`th dictator function.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    theorem FABL.dictator_toReal_eq_monomial_singleton {n : ℕ} (i : Fin n)
  (x : FABL.SignCube n) :
  (FABL.dictator i).toReal x = FABL.monomial {i} x
    theorem FABL.dictator_toReal_eq_monomial_singleton
  {n : ℕ} (i : Fin n)
  (x : FABL.SignCube n) :
  (FABL.dictator i).toReal x =
    FABL.monomial {i} x
    The real encoding of a dictator is the singleton monomial from Chapter 1.
Definition2.1.4
uses 0
Used by 2
Reverse dependency previews
Preview
Lemma 3.1.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.4. A function f:\{-1,1\}^n\to\{-1,1\} is a k-junta, for k\in\mathbb N, if it depends on at most k input coordinates; that is, there are i_1,\ldots,i_k\in[n] and a function g:\{-1,1\}^k\to\{-1,1\} such that f(x)=g(x_{i_1},\ldots,x_{i_k}) for every x\in\{-1,1\}^n. Informally, f is called a junta when it depends on only a constant number of coordinates.

Lean code for Definition2.1.4●2 declarations
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.IsKJunta.{u_1} {n : ℕ} {β : Type u_1} (f : FABL.SignCube n → β)
  (k : ℕ) : Prop
    def FABL.IsKJunta.{u_1} {n : ℕ} {β : Type u_1}
  (f : FABL.SignCube n → β) (k : ℕ) : Prop
    O'Donnell, Definition 2.4: a function is a `k`-junta when it depends on a set of at most
`k` coordinates. The dependence predicate is Mathlib's `DependsOn`.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    theorem FABL.isKJunta_iff_exists_factorization.{u_1} {n : ℕ} {β : Type u_1}
  [Nonempty β] (f : FABL.SignCube n → β) (k : ℕ) :
  FABL.IsKJunta f k ↔ ∃ S, S.card ≤ k ∧ ∃ g, f = g ∘ (↑S).restrict
    theorem FABL.isKJunta_iff_exists_factorization.{u_1}
  {n : ℕ} {β : Type u_1} [Nonempty β]
  (f : FABL.SignCube n → β) (k : ℕ) :
  FABL.IsKJunta f k ↔
    ∃ S,
      S.card ≤ k ∧
        ∃ g, f = g ∘ (↑S).restrict
    Mathlib's factorization characterization of coordinate dependence, specialized to juntas.
Definition2.1.5
uses 0used by 1✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.5. A function f:\{-1,1\}^n\to\{-1,1\} is a weighted majority, or a linear threshold function, if there are a_0,a_1,\ldots,a_n\in\mathbb R such that f(x)=\operatorname{sgn}(a_0+a_1x_1+\cdots+a_nx_n).

Lean code for Definition2.1.5●1 definition
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.IsLinearThreshold {n : ℕ} (f : FABL.BooleanFunction n) : Prop
    def FABL.IsLinearThreshold {n : ℕ}
  (f : FABL.BooleanFunction n) : Prop
    O'Donnell, Definition 2.5: a Boolean linear threshold function.
Definition2.1.6
uses 1used by 1✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.6. The depth-d recursive majority of n, denoted \operatorname{Maj}_n^{\otimes d}, is the Boolean function on n^d bits defined inductively by \operatorname{Maj}_n^{\otimes 1}=\operatorname{Maj}_n and \operatorname{Maj}_n^{\otimes(d+1)} (x^{(1)},\ldots,x^{(n)}) =\operatorname{Maj}_n\bigl( \operatorname{Maj}_n^{\otimes d}(x^{(1)}),\ldots, \operatorname{Maj}_n^{\otimes d}(x^{(n)})\bigr), where each x^{(i)}\in\{-1,1\}^{n^d}.

Lean code for Definition2.1.6●3 declarations
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.recursiveMajority (n d : ℕ) : FABL.BooleanFunction (n ^ d)
    def FABL.recursiveMajority (n d : ℕ) :
  FABL.BooleanFunction (n ^ d)
    O'Donnell, Definition 2.6: the depth-`d` recursive majority of arity `n`.

At depth zero this is the identity on the unique input coordinate; the book starts the indexing at
depth one.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    theorem FABL.recursiveMajority_one (n : ℕ) (x : FABL.SignCube (n ^ 1)) :
  FABL.recursiveMajority n 1 x =
    FABL.majority n fun i => x (Fin.cast ⋯ i)
    theorem FABL.recursiveMajority_one (n : ℕ)
  (x : FABL.SignCube (n ^ 1)) :
  FABL.recursiveMajority n 1 x =
    FABL.majority n fun i =>
      x (Fin.cast ⋯ i)
    The depth-one recursive majority is majority, after the canonical index cast.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    theorem FABL.recursiveMajority_succ (n d : ℕ)
  (x : FABL.SignCube (n ^ (d + 1))) :
  FABL.recursiveMajority n (d + 1) x =
    FABL.majority n fun i =>
      FABL.recursiveMajority n d (FABL.recursiveInputBlock x i)
    theorem FABL.recursiveMajority_succ (n d : ℕ)
  (x : FABL.SignCube (n ^ (d + 1))) :
  FABL.recursiveMajority n (d + 1) x =
    FABL.majority n fun i =>
      FABL.recursiveMajority n d
        (FABL.recursiveInputBlock x i)
Definition2.1.7
uses 1used by 1✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.7. The tribes function of width w and size s is \operatorname{Tribes}_{w,s}:\{-1,1\}^{sw}\to\{-1,1\} defined by \operatorname{Tribes}_{w,s}(x^{(1)},\ldots,x^{(s)}) =\operatorname{OR}_s\bigl( \operatorname{AND}_w(x^{(1)}),\ldots, \operatorname{AND}_w(x^{(s)})\bigr), where each x^{(i)}\in\{-1,1\}^w.

Lean code for Definition2.1.7●2 definitions
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.inputBlock {s w : ℕ} (x : FABL.SignCube (s * w)) (i : Fin s) :
  FABL.SignCube w
    def FABL.inputBlock {s w : ℕ}
  (x : FABL.SignCube (s * w))
  (i : Fin s) : FABL.SignCube w
    View a flat input of length `s * w` as `s` consecutive blocks of width `w`.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.tribes (w s : ℕ) : FABL.BooleanFunction (s * w)
    def FABL.tribes (w s : ℕ) :
  FABL.BooleanFunction (s * w)
    O'Donnell, Definition 2.7: OR of `s` width-`w` AND blocks.
Lemma2.1.8
uses 1
Used by 3
Reverse dependency previews
Preview
Definition 2.1.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1supportfidelity-exact

Exercise 1.30(a). A permutation \pi\in S_n acts on strings by (x^\pi)_i=x_{\pi(i)} and on functions by f^\pi(x)=f(x^\pi). For every f:\{-1,1\}^n\to\mathbb R and S\subseteq[n], its Fourier coefficients obey \widehat{f^\pi}(S)=\widehat f\bigl(\pi^{-1}(S)\bigr).

Lean code for Lemma2.1.8●3 declarations
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.permuteInput {n : ℕ} (π : Equiv.Perm (Fin n))
  (x : FABL.SignCube n) : FABL.SignCube n
    def FABL.permuteInput {n : ℕ}
  (π : Equiv.Perm (Fin n))
  (x : FABL.SignCube n) : FABL.SignCube n
    Reindex a sign-cube input by a coordinate permutation.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.permuteFinset {n : ℕ} (π : Equiv.Perm (Fin n))
  (S : Finset (Fin n)) : Finset (Fin n)
    def FABL.permuteFinset {n : ℕ}
  (π : Equiv.Perm (Fin n))
  (S : Finset (Fin n)) : Finset (Fin n)
    Image of a Fourier index under a coordinate permutation.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    theorem FABL.fourierCoeff_comp_permuteInput {n : ℕ} (π : Equiv.Perm (Fin n))
  (f : FABL.SignCube n → ℝ) (S : Finset (Fin n)) :
  FABL.fourierCoeff (f ∘ FABL.permuteInput π) S =
    FABL.fourierCoeff f (FABL.permuteFinset (Equiv.symm π) S)
    theorem FABL.fourierCoeff_comp_permuteInput
  {n : ℕ} (π : Equiv.Perm (Fin n))
  (f : FABL.SignCube n → ℝ)
  (S : Finset (Fin n)) :
  FABL.fourierCoeff
      (f ∘ FABL.permuteInput π) S =
    FABL.fourierCoeff f
      (FABL.permuteFinset (Equiv.symm π)
        S)
    O'Donnell, Exercise 1.30(a): Fourier coefficients reindex under coordinate permutations.
Definition2.1.9
uses 1
Used by 5
Reverse dependency previews
Preview
Lemma 2.1.10
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.8. A function f:\{-1,1\}^n\to\{-1,1\} is:

  • monotone if f(x)\le f(y) whenever x\le y coordinatewise;

  • odd if f(-x)=-f(x);

  • unanimous if f(1,\ldots,1)=1 and f(-1,\ldots,-1)=-1;

  • symmetric if f(x^\pi)=f(x) for every \pi\in S_n; equivalently, f(x) depends only on the number of coordinates of x equal to 1.

The definitions of monotone, odd, and symmetric also apply to f:\{-1,1\}^n\to\mathbb R.

Lean code for Definition2.1.9●5 declarations
  • defdefined in Mathlib/Order/Monotone/Defs.lean
    complete
    def Monotone.{u, v} {α : Type u} {β : Type v} [Preorder α] [Preorder β]
  (f : α → β) : Prop
    def Monotone.{u, v} {α : Type u} {β : Type v}
  [Preorder α] [Preorder β] (f : α → β) :
  Prop
    A function `f` is monotone if `a ≤ b` implies `f a ≤ f b`.
  • defdefined in Mathlib/Algebra/Group/EvenFunction.lean
    complete
    def Function.Odd.{u_1, u_2} {α : Type u_1} {β : Type u_2} [Neg α] [Neg β]
  (f : α → β) : Prop
    def Function.Odd.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} [Neg α] [Neg β]
  (f : α → β) : Prop
    A function `f` is _odd_ if it satisfies `f (-x) = -f x` for all `x`.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/MayTheorem.lean
    complete
    def FABL.IsUnanimous {n : ℕ} (f : FABL.BooleanFunction n) : Prop
    def FABL.IsUnanimous {n : ℕ}
  (f : FABL.BooleanFunction n) : Prop
    The unanimity property from O'Donnell, Definition 2.8.
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/MayTheorem.lean
    complete
    def FABL.IsSymmetric.{u_1} {n : ℕ} {β : Type u_1}
  (f : FABL.SignCube n → β) : Prop
    def FABL.IsSymmetric.{u_1} {n : ℕ}
  {β : Type u_1}
  (f : FABL.SignCube n → β) : Prop
    The symmetry property from O'Donnell, Definition 2.8.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/MayTheorem.lean
    complete
    theorem FABL.isSymmetric_iff_eq_of_positiveCoordinateCount_eq.{u_1} {n : ℕ}
  {β : Type u_1} (f : FABL.SignCube n → β) :
  FABL.IsSymmetric f ↔
    ∀ (x y : FABL.SignCube n),
      FABL.positiveCoordinateCount x = FABL.positiveCoordinateCount y →
        f x = f y
    theorem FABL.isSymmetric_iff_eq_of_positiveCoordinateCount_eq.{u_1}
  {n : ℕ} {β : Type u_1}
  (f : FABL.SignCube n → β) :
  FABL.IsSymmetric f ↔
    ∀ (x y : FABL.SignCube n),
      FABL.positiveCoordinateCount x =
          FABL.positiveCoordinateCount y →
        f x = f y
    O'Donnell, Definition 2.8: symmetry is equivalently dependence only on the number of `+1`
coordinates.
Lemma2.1.10
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 1✓L∃∀N
Tagssection-2-1supportfidelity-exact

Exercise 2.3: May's Theorem.

  1. A function f:\{-1,1\}^n\to\{-1,1\} is symmetric and monotone if and only if it has a weighted-majority representation f(x)=\operatorname{sgn}(a_0+x_1+\cdots+x_n) with all nonconstant weights equal to 1.

  2. If f:\{-1,1\}^n\to\{-1,1\} is symmetric, monotone, and odd, then n is odd and f=\operatorname{Maj}_n.

Lean code for Lemma2.1.10●3 declarations
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Definitions.lean
    complete
    def FABL.IsEqualWeightThreshold {n : ℕ} (f : FABL.BooleanFunction n) : Prop
    def FABL.IsEqualWeightThreshold {n : ℕ}
  (f : FABL.BooleanFunction n) : Prop
    A weighted-majority representation whose nonconstant weights are all one.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/MayTheorem.lean
    complete
    theorem FABL.symmetric_and_monotone_iff_isEqualWeightThreshold {n : ℕ}
  (f : FABL.BooleanFunction n) :
  FABL.IsSymmetric f ∧ Monotone f ↔ FABL.IsEqualWeightThreshold f
    theorem FABL.symmetric_and_monotone_iff_isEqualWeightThreshold
  {n : ℕ} (f : FABL.BooleanFunction n) :
  FABL.IsSymmetric f ∧ Monotone f ↔
    FABL.IsEqualWeightThreshold f
    May's Theorem, Exercise 2.3(a): symmetric monotone Boolean functions are exactly the
equal-weight threshold functions.
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/MayTheorem.lean
    complete
    theorem FABL.may_theorem {n : ℕ} (f : FABL.BooleanFunction n)
  (hsym : FABL.IsSymmetric f) (hmono : Monotone f)
  (hodd : Function.Odd f) : Odd n ∧ f = FABL.majority n
    theorem FABL.may_theorem {n : ℕ}
  (f : FABL.BooleanFunction n)
  (hsym : FABL.IsSymmetric f)
  (hmono : Monotone f)
  (hodd : Function.Odd f) :
  Odd n ∧ f = FABL.majority n
    May's Theorem, Exercise 2.3(b): a symmetric, monotone, odd Boolean function has odd arity
and is majority.
Lemma2.1.11
Statement uses 7
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-1fidelity-exact

Example 2.9. For odd n, \operatorname{Maj}_n is monotone, odd, unanimous, and symmetric; by May's Theorem it is the only function with all four properties. Dictator functions and recursive majority functions are monotone, odd, and unanimous. For n\ge2, the functions \operatorname{AND}_n and \operatorname{OR}_n are monotone, unanimous, and symmetric, but are not odd. For w,s\ge2, tribes functions are monotone and unanimous; they are not symmetric, but they have the weaker property defined next. (These lower bounds make explicit the degenerate arities suppressed in the book's prose.)

Lean code for Lemma2.1.11●1 theorem
  • theoremdefined in FABL/Chapter02/SocialChoiceFunctions/Examples.lean
    complete
    theorem FABL.example2_9 {n : ℕ} (hn : Odd n) (i : Fin n) (d m w s : ℕ)
  (hm : 1 < m) (hw : 1 < w) (hs : 1 < s) :
  (Monotone (FABL.majority n) ∧
      Function.Odd (FABL.majority n) ∧
        FABL.IsUnanimous (FABL.majority n) ∧
          FABL.IsSymmetric (FABL.majority n)) ∧
    (∀ (f : FABL.BooleanFunction n),
        FABL.IsSymmetric f →
          Monotone f → Function.Odd f → f = FABL.majority n) ∧
      (Monotone (FABL.dictator i) ∧
          Function.Odd (FABL.dictator i) ∧
            FABL.IsUnanimous (FABL.dictator i)) ∧
        (Monotone (FABL.recursiveMajority n d) ∧
            Function.Odd (FABL.recursiveMajority n d) ∧
              FABL.IsUnanimous (FABL.recursiveMajority n d)) ∧
          (Monotone (FABL.andFunction m) ∧
              FABL.IsUnanimous (FABL.andFunction m) ∧
                FABL.IsSymmetric (FABL.andFunction m) ∧
                  ¬Function.Odd (FABL.andFunction m)) ∧
            (Monotone (FABL.orFunction m) ∧
                FABL.IsUnanimous (FABL.orFunction m) ∧
                  FABL.IsSymmetric (FABL.orFunction m) ∧
                    ¬Function.Odd (FABL.orFunction m)) ∧
              Monotone (FABL.tribes w s) ∧
                FABL.IsUnanimous (FABL.tribes w s) ∧
                  ¬FABL.IsSymmetric (FABL.tribes w s) ∧
                    FABL.IsTransitiveSymmetric (FABL.tribes w s)
    theorem FABL.example2_9 {n : ℕ} (hn : Odd n)
  (i : Fin n) (d m w s : ℕ) (hm : 1 < m)
  (hw : 1 < w) (hs : 1 < s) :
  (Monotone (FABL.majority n) ∧
      Function.Odd (FABL.majority n) ∧
        FABL.IsUnanimous
            (FABL.majority n) ∧
          FABL.IsSymmetric
            (FABL.majority n)) ∧
    (∀ (f : FABL.BooleanFunction n),
        FABL.IsSymmetric f →
          Monotone f →
            Function.Odd f →
              f = FABL.majority n) ∧
      (Monotone (FABL.dictator i) ∧
          Function.Odd (FABL.dictator i) ∧
            FABL.IsUnanimous
              (FABL.dictator i)) ∧
        (Monotone
              (FABL.recursiveMajority n
                d) ∧
            Function.Odd
                (FABL.recursiveMajority n
                  d) ∧
              FABL.IsUnanimous
                (FABL.recursiveMajority n
                  d)) ∧
          (Monotone (FABL.andFunction m) ∧
              FABL.IsUnanimous
                  (FABL.andFunction m) ∧
                FABL.IsSymmetric
                    (FABL.andFunction m) ∧
                  ¬Function.Odd
                      (FABL.andFunction
                        m)) ∧
            (Monotone
                  (FABL.orFunction m) ∧
                FABL.IsUnanimous
                    (FABL.orFunction m) ∧
                  FABL.IsSymmetric
                      (FABL.orFunction
                        m) ∧
                    ¬Function.Odd
                        (FABL.orFunction
                          m)) ∧
              Monotone (FABL.tribes w s) ∧
                FABL.IsUnanimous
                    (FABL.tribes w s) ∧
                  ¬FABL.IsSymmetric
                        (FABL.tribes w
                          s) ∧
                    FABL.IsTransitiveSymmetric
                      (FABL.tribes w s)
    O'Donnell, Example 2.9: the stated properties of the standard social-choice functions.

The hypotheses record the nondegenerate cases suppressed in the prose: AND and OR are non-odd
only from arity two onward, and tribes is non-symmetric only with at least two blocks of width at
least two.
Definition2.1.12
uses 1used by 1✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.10. A function f:\{-1,1\}^n\to\{-1,1\} is transitive-symmetric if, for every i,i'\in[n], there is a permutation \pi\in S_n such that \pi(i)=i' and f(x^\pi)=f(x) for every x\in\{-1,1\}^n.

Lean code for Definition2.1.12●1 definition
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Examples.lean
    complete
    def FABL.IsTransitiveSymmetric.{u_1} {n : ℕ} {β : Type u_1}
  (f : FABL.SignCube n → β) : Prop
    def FABL.IsTransitiveSymmetric.{u_1} {n : ℕ}
  {β : Type u_1}
  (f : FABL.SignCube n → β) : Prop
    O'Donnell, Definition 2.10: every two coordinates are equivalent under a symmetry of `f`.
Definition2.1.13
uses 1
Used by 3
Reverse dependency previews
Preview
Proposition 2.3.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N
Tagssection-2-1fidelity-exact

Definition 2.11. The impartial culture assumption is that the n voters' preferences are independent and uniformly random.

Lean code for Definition2.1.13●1 definition
  • defdefined in FABL/Chapter02/SocialChoiceFunctions/Examples.lean
    complete
    def FABL.impartialCulture (n : ℕ) : PMF (FABL.SignCube n)
    def FABL.impartialCulture (n : ℕ) :
  PMF (FABL.SignCube n)
    O'Donnell, Definition 2.11: impartial culture is the uniform distribution on vote profiles.