text:
(*
    Author:      Jose Divasón
    Email:       jose.divason@unirioja.es
*)

section \<open>Some theorems about rings and ideals\<close>

theory Rings2_Extended
  imports
    Echelon_Form.Rings2
    "HOL-Types_To_Sets.Types_To_Sets"
begin

subsection \<open>Missing properties on ideals\<close>

lemma ideal_generated_subset2:
  assumes  "\<forall>b\<in>B. b \<in> ideal_generated A"
  shows "ideal_generated B \<subseteq> ideal_generated A"
  by (metis (mono_tags, lifting) InterE assms ideal_generated_def
ideal_ideal_generated mem_Collect_eq subsetI)

context comm_ring_1
begin

lemma ideal_explicit: "ideal_generated S
      = {y. \<exists>f U. finite U \<and> U \<subseteq> S \<and> (\<Sum>i\<in>U. f i * i) = y}"
  by (simp add: ideal_generated_eq_left_ideal left_ideal_explicit)
end

lemma ideal_generated_minus:
  assumes a: "a \<in> ideal_generated (S-{a})"
  shows "ideal_generated S = ideal_generated (S-{a})"
proof (cases "a \<in> S")
  case True note a_in_S = True
  show ?thesis
  proof
    show "ideal_generated S \<subseteq> ideal_generated (S - {a})"
    proof (rule ideal_generated_subset2, auto)
      fix b assume b: "b \<in> S" show "b \<in> ideal_generated (S - {a})"
      proof (cases "b = a")
        case True
        then show ?thesis using a by auto
      next
        case False
        then show ?thesis using b
          by (simp add: ideal_generated_in)
      qed
    qed
    show "ideal_generated (S - {a}) \<subseteq> ideal_generated S"
      by (rule ideal_generated_subset, auto)
  qed
next
  case False
  then show ?thesis by simp
qed

lemma ideal_generated_dvd_eq:
  assumes a_dvd_b: "a dvd b"
  and a: "a \<in> S"
  and a_not_b: "a \<noteq> b"
  shows "ideal_generated S = ideal_generated (S - {b})"
proof
  show "ideal_generated S \<subseteq> ideal_generated (S - {b})"
  proof (rule ideal_generated_subset2, auto)
    fix x assume x: "x \<in> S"
    show "x \<in> ideal_generated (S - {b})"
    proof (cases "x = b")
      case True
      obtain k where b_ak: "b = a * k" using a_dvd_b unfolding dvd_def by blast
      let ?f = "\<lambda>c. k"
      have "(\<Sum>i\<in>{a}. i * ?f i) = x" using True b_ak by auto
      moreover have "{a} \<subseteq> S - {b}" using a_not_b a by auto
      moreover have "finite {a}" by auto
      ultimately show ?thesis
        unfolding ideal_def
        by (metis True b_ak ideal_def ideal_generated_in ideal_ideal_generated insert_subset right_ideal_def)
    next
      case False
      then show ?thesis by (simp add: ideal_generated_in x)
    qed
  qed
  show "ideal_generated (S - {b}) \<subseteq> ideal_generated S" by (rule ideal_generated_subset, auto)
qed

lemma ideal_generated_dvd_eq_diff_set:
  assumes i_in_I: "i\<in>I" and i_in_J: "i \<notin> J" and i_dvd_j: "\<forall>j\<in>J. i dvd j"
  and f: "finite J"
  shows "ideal_generated I = ideal_generated (I - J)"
  using f i_in_J i_dvd_j i_in_I
  proof (induct J arbitrary: I)
  case empty
    then show ?case by auto
  next
    case (insert x J)
    have "ideal_generated I = ideal_generated (I-{x})"
      by (rule ideal_generated_dvd_eq[of i], insert insert.prems , auto)
    also have "... = ideal_generated ((I-{x}) - J)"
      by (rule insert.hyps, insert insert.prems insert.hyps, auto)
    also have "... = ideal_generated (I - insert x J)"
      using Diff_insert2[of I x J] by auto
    finally show ?case .
  qed

context comm_ring_1
begin

lemma ideal_generated_singleton_subset:
  assumes d: "d \<in> ideal_generated S" and fin_S: "finite S"
  shows "ideal_generated {d} \<subseteq> ideal_generated S"
proof
  fix x assume x: "x \<in> ideal_generated {d}"
  obtain k where x_kd: "x = k*d " using x using obtain_sum_ideal_generated[OF x]
    by (metis finite.emptyI finite.insertI sum_singleton)
  show "x \<in> ideal_generated S"
    using d ideal_eq_right_ideal ideal_ideal_generated right_ideal_def mult_commute x_kd by auto
qed

lemma ideal_generated_singleton_dvd:
  assumes i: "ideal_generated S = ideal_generated {d}" and x: "x \<in> S"
  shows "d dvd x"
  by (metis i x finite.intros dvd_ideal_generated_singleton
      ideal_generated_in ideal_generated_singleton_subset)

lemma ideal_generated_UNIV_insert:
  assumes "ideal_generated S = UNIV"
  shows "ideal_generated (insert a S) = UNIV" using assms
  using local.ideal_generated_subset by blast

lemma ideal_generated_UNIV_union:
  assumes "ideal_generated S = UNIV"
  shows "ideal_generated (A \<union> S) = UNIV"
  using assms local.ideal_generated_subset
  by (metis UNIV_I Un_subset_iff equalityI subsetI)

lemma ideal_explicit2:
  assumes "finite S"
  shows "ideal_generated S = {y. \<exists>f. (\<Sum>i\<in>S. f i * i) = y}"
  by (smt Collect_cong assms ideal_explicit obtain_sum_ideal_generated mem_Collect_eq subsetI)

lemma ideal_generated_unit:
  assumes u: "u dvd 1"
  shows "ideal_generated {u} = UNIV"
proof -
  have "x \<in> ideal_generated {u}" for x
  proof -
    obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
      using local.mult_ac(2) by blast
    have "x = x * inv_u * u" using inv_u by (simp add: local.mult_ac(1))
    also have "... \<in> {k * u |k. k \<in> UNIV}" by auto
    also have "... = ideal_generated {u}" unfolding ideal_generated_singleton by simp
    finally show ?thesis .
  qed
  thus ?thesis by auto
qed

lemma ideal_generated_dvd_subset:
  assumes x: "\<forall>x \<in> S. d dvd x" and S: "finite S"
  shows "ideal_generated S \<subseteq> ideal_generated {d}"
proof
  fix x assume "x\<in> ideal_generated S"
  from this obtain f where f: "(\<Sum>i\<in>S. f i * i) = x" using ideal_explicit2[OF S] by auto
  have "d dvd (\<Sum>i\<in>S. f i * i)" by (rule dvd_sum, insert x, auto)
  thus "x \<in> ideal_generated {d}"
    using f dvd_ideal_generated_singleton' ideal_generated_in singletonI by blast
qed

lemma ideal_generated_mult_unit:
  assumes f: "finite S" and u: "u dvd 1"
  shows "ideal_generated ((\<lambda>x. u*x)` S) = ideal_generated S"
  using f
proof (induct S)
  case empty
  then show ?case by auto
next
  case (insert x S)
  obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
    using mult_ac by blast
  have f: "finite (insert (u*x) ((\<lambda>x. u*x)` S))" using insert.hyps by auto
  have f2: "finite (insert x S)" by (simp add: insert(1))
  have f3: "finite S" by (simp add: insert)
  have f4: "finite ((*) u ` S)" by (simp add: insert)
  have inj_ux: "inj_on (\<lambda>x. u*x) S" unfolding inj_on_def
    by (auto, metis inv_u local.mult_1_left local.semiring_normalization_rules(18))
  have "ideal_generated ((\<lambda>x. u*x)` (insert x S)) = ideal_generated (insert (u*x) ((\<lambda>x. u*x)` S))"
    by auto
  also have "... = {y. \<exists>f. (\<Sum>i\<in>insert (u*x) ((\<lambda>x. u*x)` S). f i * i) = y}"
    using ideal_explicit2[OF f] by auto
  also have "... = {y. \<exists>f. (\<Sum>i\<in>(insert x S). f i * i) = y}" (is "?L = ?R")
  proof -
    have "a \<in> ?L"  if a: "a \<in> ?R" for a
    proof -
      obtain f where sum_rw: "(\<Sum>i\<in>(insert x S). f i * i) = a" using a by auto
      define b where "b=(\<Sum>i\<in>S. f i * i)"
      have "b \<in> ideal_generated S" unfolding b_def ideal_explicit2[OF f3] by auto
      hence "b \<in> ideal_generated ((*) u ` S)" using insert.hyps(3) by auto
      from this obtain g where "(\<Sum>i\<in>((*) u ` S). g i * i) = b"
        unfolding ideal_explicit2[OF f4] by auto
      hence sum_rw2: "(\<Sum>i\<in>S. f i * i) = (\<Sum>i\<in>((*) u ` S). g i * i)" unfolding b_def by auto
      let ?g = "\<lambda>i. if i = u*x then f x * inv_u else g i"
       have sum_rw3: "sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S = sum ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) S"
        by (rule sum.cong, auto, metis inv_u local.insert(2) local.mult_1_right
              local.mult_ac(2) local.semiring_normalization_rules(18))
      have sum_rw4: "(\<Sum>i\<in>(\<lambda>x. u*x)` S. g i * i) = sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S"
        by (rule sum.reindex[OF inj_ux])
      have "a = f x * x + (\<Sum>i\<in>S. f i * i)"
        using sum_rw local.insert(1) local.insert(2) by auto
      also have "... = f x * x + (\<Sum>i\<in>(\<lambda>x. u*x)` S. g i * i)" using sum_rw2 by auto
      also have "... = ?g (u * x) * (u * x) + (\<Sum>i\<in>(\<lambda>x. u*x)` S. g i * i)"
        using inv_u by (smt local.mult_1_right local.mult_ac(1))
      also have "... =  ?g (u * x) * (u * x) + sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S"
        using sum_rw4 by auto
      also have "... = ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) x + sum ((\<lambda>i. g i * i) \<circ> (\<lambda>x. u*x)) S" by auto
      also have "... = ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) x + sum ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) S"
        using sum_rw3 by auto
      also have "... = sum ((\<lambda>i. ?g i * i) \<circ> (\<lambda>x. u*x)) (insert x S)"
        by (rule sum.insert[symmetric], auto simp add: insert)
      also have "... = (\<Sum>i\<in>insert (u * x) ((\<lambda>x. u*x)` S). ?g i * i)"
        by (smt abel_semigroup.commute f2 image_insert inv_u mult.abel_semigroup_axioms mult_1_right
            semiring_normalization_rules(18) sum.reindex_nontrivial)
      also have "... = (\<Sum>i\<in>(\<lambda>x. u*x)` (insert x S). ?g i * i)" by auto
      finally show ?thesis by auto
    qed
    moreover have "a \<in> ?R" if a: "a \<in> ?L" for a
    proof -
      obtain f where sum_rw: "(\<Sum>i\<in>(insert (u * x) ((*) u ` S)). f i * i) = a" using a by auto
      have ux_notin: "u*x \<notin> ((*) u ` S)"
        by (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI inv_u local.insert(2) local.mult_1_left
            local.semiring_normalization_rules(18) subsetI)
      let ?f = "(\<lambda>x. f x * x)"
      have "sum ?f ((*) u ` S) \<in> ideal_generated ((*) u ` S)"
        unfolding ideal_explicit2[OF f4] by auto
      from this obtain g where sum_rw1: "sum (\<lambda>i. g i * i) S = sum ?f (((*) u ` S))"
        using insert.hyps(3) unfolding ideal_explicit2[OF f3] by blast
      let ?g = "(\<lambda>i. if i = x  then (f (u*x) *u) * x else g i * i)"
      let ?g' = "\<lambda>i. if i = x  then f (u*x) * u else g i"
      have sum_rw2: "sum (\<lambda>i. g i * i) S = sum ?g S" by (rule sum.cong, insert inj_ux ux_notin, auto)
      have "a = (\<Sum>i\<in>(insert (u * x) ((*) u ` S)). f i * i)" using sum_rw by simp
      also have "... = ?f (u*x) +  sum ?f (((*) u ` S))"
        by (rule sum.insert[OF f4], insert inj_ux) (metis UNIV_I inj_on_image_mem_iff inj_on_inverseI
            inv_u local.insert(2) local.mult_1_left local.semiring_normalization_rules(18) subsetI)
      also have "... = ?f (u*x) + sum (\<lambda>i. g i * i) S" unfolding sum_rw1 by auto
      also have "... = ?g x + sum ?g S" unfolding sum_rw2 using mult.assoc by auto
      also have "... = sum ?g (insert x S)" by (rule sum.insert[symmetric, OF f3 insert.hyps(2)])
      also have "... = sum (\<lambda>i. ?g' i * i) (insert x S)" by (rule sum.cong, auto)
      finally show ?thesis by fast
    qed
    ultimately show ?thesis by blast
  qed
  also have "... = ideal_generated (insert x S)" using ideal_explicit2[OF f2] by auto
  finally show ?case by auto
qed

corollary ideal_generated_mult_unit2:
  assumes u: "u dvd 1"
  shows "ideal_generated {u*a,u*b} = ideal_generated {a,b}"
proof -
  let ?S = "{a,b}"
  have "ideal_generated {u*a,u*b} = ideal_generated ((\<lambda>x. u*x)` {a,b})" by auto
  also have "... = ideal_generated {a,b}" by (rule ideal_generated_mult_unit[OF _ u], simp)
  finally show ?thesis .
qed

lemma ideal_generated_1[simp]: "ideal_generated {1} = UNIV"
  by (metis ideal_generated_unit dvd_ideal_generated_singleton order_refl)

lemma ideal_generated_pair: "ideal_generated {a,b} = {p*a+q*b | p q. True}"
proof -
  have i: "ideal_generated {a,b} = {y. \<exists>f. (\<Sum>i\<in>{a,b}. f i * i) = y}" using ideal_explicit2 by auto
  show ?thesis
  proof (cases "a=b")
    case True
    show ?thesis using True i
      by (auto, metis mult_ac(2) semiring_normalization_rules)
      (metis (no_types, opaque_lifting) add_minus_cancel mult_ac ring_distribs semiring_normalization_rules)
  next
    case False
    have 1: "\<exists>p q. (\<Sum>i\<in>{a, b}. f i * i) = p * a + q * b" for f
      by (rule exI[of _ "f a"], rule exI[of _ "f b"], rule sum_two_elements[OF False])
    moreover have "\<exists>f. (\<Sum>i\<in>{a, b}. f i * i) = p * a + q * b" for p q
      by (rule exI[of _ "\<lambda>i. if i=a then p else q"],
          unfold sum_two_elements[OF False], insert False, auto)
    ultimately show ?thesis using i by auto
  qed
qed

lemma ideal_generated_pair_exists_pq1:
  assumes i: "ideal_generated {a,b} = (UNIV::'a set)"
  shows "\<exists>p q. p*a + q*b = 1"
  using i unfolding ideal_generated_pair
  by (smt iso_tuple_UNIV_I mem_Collect_eq)

lemma ideal_generated_pair_UNIV:
  assumes sa_tb_u: "s*a+t*b = u" and u: "u dvd 1"
  shows "ideal_generated {a,b} = UNIV"
proof -
  have f: "finite {a,b}" by simp
  obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
    by (metis mult.commute)
  have "x \<in> ideal_generated {a,b}" for x
  proof (cases "a = b")
    case True
    then show ?thesis
      by (metis UNIV_I dvd_def dvd_ideal_generated_singleton' ideal_generated_unit insert_absorb2
          mult.commute sa_tb_u semiring_normalization_rules(34) subsetI subset_antisym u)
  next
    case False note a_not_b = False
    let ?f = "\<lambda>y. if y = a then inv_u * x * s else inv_u * x * t"
    have "(\<Sum>i\<in>{a,b}. ?f i * i) = ?f a * a + ?f b * b" by (rule sum_two_elements[OF a_not_b])
    also have "... = x" using a_not_b sa_tb_u inv_u
      by (auto, metis mult_ac(1) mult_ac(2) ring_distribs(1) semiring_normalization_rules(12))
    finally show ?thesis unfolding ideal_explicit2[OF f] by auto
  qed
  thus ?thesis by auto
qed

lemma ideal_generated_pair_exists:
  assumes l: "(ideal_generated {a,b} = ideal_generated {d})"
  shows "(\<exists> p q. p*a+q*b = d)"
proof -
  have d: "d \<in> ideal_generated {d}" by (simp add: ideal_generated_in)
  hence "d \<in> ideal_generated {a,b}" using l by auto
  from this obtain p q where "d = p*a+q*b" using ideal_generated_pair[of a b] by auto
  thus ?thesis by auto
qed

lemma obtain_ideal_generated_pair:
  assumes "c \<in> ideal_generated {a,b}"
  obtains p q where "p*a+q*b=c"
proof -
  have "c \<in> {p * a + q * b |p q. True}" using assms ideal_generated_pair by auto
  thus ?thesis using that by auto
qed

lemma ideal_generated_pair_exists_UNIV:
  shows "(ideal_generated {a,b} = ideal_generated {1}) = (\<exists>p q. p*a+q*b = 1)" (is "?lhs = ?rhs")
proof
  assume r: ?rhs
  have "x \<in> ideal_generated {a,b}" for x
  proof (cases "a=b")
    case True
    then show ?thesis
      by (metis UNIV_I r dvd_ideal_generated_singleton finite.intros ideal_generated_1
          ideal_generated_pair_UNIV ideal_generated_singleton_subset)
  next
    case False
    have f: "finite {a,b}" by simp
    have 1: "1 \<in> ideal_generated {a,b}"
      using ideal_generated_pair_UNIV local.one_dvd r by blast
    hence i: "ideal_generated {a,b} = {y. \<exists>f. (\<Sum>i\<in>{a,b}. f i * i) = y}"
      using ideal_explicit2[of "{a,b}"] by auto
    from this obtain f where f: "f a * a + f b * b = 1" using sum_two_elements 1 False by auto
    let ?f = "\<lambda>y. if y = a then x * f a else x * f b"
    have "(\<Sum>i\<in>{a,b}. ?f i * i) = x" unfolding sum_two_elements[OF False] using f False
      using mult_ac(1) ring_distribs(1) semiring_normalization_rules(12) by force
    thus ?thesis unfolding i by auto
  qed
  thus ?lhs by auto
next
  assume ?lhs thus ?rhs using ideal_generated_pair_exists[of a b 1] by auto
qed

corollary ideal_generated_UNIV_obtain_pair:
  assumes "ideal_generated {a,b} = ideal_generated {1}"
  shows " (\<exists>p q. p*a+q*b = d)"
proof -
  obtain x y where "x*a+y*b = 1" using ideal_generated_pair_exists_UNIV assms by auto
  hence "d*x*a+d*y*b=d"
    using local.mult_ac(1) local.ring_distribs(1) local.semiring_normalization_rules(12) by force
  thus ?thesis by auto
qed

lemma sum_three_elements:
  shows "\<exists>x y z::'a. (\<Sum>i\<in>{a,b,c}. f i * i) = x * a + y * b + z * c"
proof (cases "a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c")
  case True
  then show ?thesis by (auto, metis add.assoc)
next
  case False
  have 1: "\<exists>x y z. f c * c = x * c + y * c + z * c"
    by (rule exI[of _ 0],rule exI[of _ 0], rule exI[of _ "f c"], auto)
  have 2: "\<exists>x y z. f b * b + f c * c = x * b + y * b + z * c"
    by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], auto)
  have 3: "\<exists>x y z. f a * a + f c * c = x * a + y * c + z * c"
    by (rule exI[of _ "f a"],rule exI[of _ 0], rule exI[of _ "f c"], auto)
  have 4: "\<exists>x y z. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b \<noteq> c"
    by (rule exI[of _ 0],rule exI[of _ "f b"], rule exI[of _ "f c"], insert a b,
        auto simp add: insert_commute)
  show ?thesis using False
    by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4)
qed

lemma sum_three_elements':
  shows "\<exists>f::'a\<Rightarrow>'a. (\<Sum>i\<in>{a,b,c}. f i * i) = x * a + y * b + z * c"
proof (cases "a \<noteq> b \<and> b \<noteq> c \<and> a \<noteq> c")
  case True
  let ?f = "\<lambda>i. if i = a then x else if i = b then y else if i = c then z else 0"
  show ?thesis by (rule exI[of _ "?f"], insert True mult.assoc, auto simp add: local.add_ac)
next
  case False
  have 1: "\<exists>f. f c * c = x * c + y * c + z * c"
    by (rule exI[of _ "\<lambda>i. if i = c then x+y+z else 0"], auto simp add: local.ring_distribs)
  have 2: "\<exists>f. f a * a + f c * c = x * a + y * c + z * c" if bc: " b = c" and ac: "a \<noteq> c"
    by (rule exI[of _ "\<lambda>i. if i = a then x else y+z"], insert ac bc add_ac ring_distribs, auto)
  have 3: "\<exists>f. f b * b + f c * c = x * b + y * b + z * c" if bc: " b \<noteq> c" and ac: "a = b"
    by (rule exI[of _ "\<lambda>i. if i = a then x+y else z"], insert ac bc add_ac ring_distribs, auto)
  have 4: "\<exists>f. (\<Sum>i\<in>{c, b, c}. f i * i) = x * c + y * b + z * c" if a: "a = c" and b: "b \<noteq> c"
    by (rule exI[of _ "\<lambda>i. if i = c then x+z else y"], insert a b add_ac ring_distribs,
        auto simp add: insert_commute)
  show ?thesis using False
    by (cases "b=c", cases "a=c", auto simp add: 1 2 3 4)
qed

(*This is generalizable to arbitrary sets.*)
lemma ideal_generated_triple_pair_rewrite:
  assumes i1: "ideal_generated {a, b, c} = ideal_generated {d}"
    and i2: "ideal_generated {a, b} = ideal_generated {d'}"
  shows "ideal_generated{d',c} = ideal_generated {d}"
proof
  have d': "d' \<in> ideal_generated {a,b}" using i2 by (simp add: ideal_generated_in)
  show "ideal_generated {d', c} \<subseteq> ideal_generated {d}"
  proof
    fix x assume x: "x \<in> ideal_generated {d', c}"
    obtain f1 f2 where f: "f1*d' + f2*c = x" using obtain_ideal_generated_pair[OF x] by auto
    obtain g1 g2 where g: "g1*a + g2*b = d'" using obtain_ideal_generated_pair[OF d'] by blast
    have 1: "f1*g1*a + f1*g2*b + f2*c = x"
      using f g local.ring_distribs(1) local.semiring_normalization_rules(18) by auto
    have "x \<in> ideal_generated {a, b, c}"
    proof -
      obtain f where "(\<Sum>i\<in>{a,b,c}. f i * i) = f1*g1*a + f1*g2*b + f2*c"
        using sum_three_elements' 1 by blast
      moreover have "ideal_generated {a,b,c} = {y. \<exists>f. (\<Sum>i\<in>{a,b,c}. f i * i) = y}"
        using ideal_explicit2[of "{a,b,c}"] by simp
      ultimately show ?thesis using 1 by auto
    qed
    thus "x \<in> ideal_generated {d}" using i1 by auto
  qed
  show "ideal_generated {d} \<subseteq> ideal_generated {d', c}"
  proof (rule ideal_generated_singleton_subset)
    obtain f1 f2 f3 where f: "f1*a + f2*b + f3*c = d"
    proof -
      have "d \<in> ideal_generated {a,b,c}" using i1  by (simp add: ideal_generated_in)
      from this obtain f where d: "(\<Sum>i\<in>{a,b,c}. f i * i) = d"
        using ideal_explicit2[of "{a,b,c}"] by auto
      obtain x y z where "(\<Sum>i\<in>{a,b,c}. f i * i) = x * a + y * b + z * c"
        using sum_three_elements by blast
      thus ?thesis using d that by auto
    qed
    obtain k where k: "f1*a + f2*b = k*d'"
    proof -
      have "f1*a + f2*b \<in> ideal_generated{a,b}" using ideal_generated_pair by blast
      also have "... = ideal_generated {d'}" using i2 by simp
      also have "... = {k*d' |k. k\<in>UNIV}" using ideal_generated_singleton by auto
      finally show ?thesis using that by auto
    qed
    have "k*d'+f3*c=d" using f k by auto
    thus "d \<in> ideal_generated {d', c}"
      using ideal_generated_pair by blast
  qed (simp)
qed

lemma ideal_generated_dvd:
  assumes i: "ideal_generated {a,b::'a} = ideal_generated{d} "
  and a: "d' dvd a" and b: "d' dvd b"
shows "d' dvd d"
proof -
  obtain p q where "p*a+q*b = d"
    using i ideal_generated_pair_exists by blast
  thus ?thesis using a b by auto
qed

lemma ideal_generated_dvd2:
  assumes i: "ideal_generated S = ideal_generated{d::'a} "
  and "finite S"
  and x: "\<forall>x\<in>S. d' dvd x"
shows "d' dvd d"
  by (metis assms dvd_ideal_generated_singleton ideal_generated_dvd_subset)

end

subsection \<open>An equivalent characterization of B\'ezout rings\<close>

text \<open>The goal of this subsection is to prove that a ring is B\'ezout ring if and only if every
  finitely generated ideal is principal.\<close>

definition "finitely_generated_ideal I = (ideal I \<and> (\<exists>S. finite S \<and> ideal_generated S = I))"

context
  assumes "SORT_CONSTRAINT('a::comm_ring_1)"
begin

lemma sum_two_elements':
  fixes d::'a
  assumes s: "(\<Sum>i\<in>{a,b}. f i * i) = d"
  obtains p and q where "d = p * a + q * b"
proof (cases "a=b")
  case True
  then show ?thesis
    by (metis (no_types, lifting) add_diff_cancel_left' emptyE finite.emptyI insert_absorb2
        left_diff_distrib' s sum.insert sum_singleton that)
next
  case False
  show ?thesis using s unfolding sum_two_elements[OF False]
    using that by auto
qed

text \<open>This proof follows Theorem 6-3 in "First Course in Rings and Ideals" by Burton\<close>

lemma all_fin_gen_ideals_are_principal_imp_bezout:
  assumes all: "\<forall>I::'a set. finitely_generated_ideal I \<longrightarrow> principal_ideal I"
  shows "OFCLASS ('a, bezout_ring_class)"
proof (intro_classes)
  fix a b::'a
  obtain d where ideal_d: "ideal_generated {a,b} = ideal_generated {d}"
    using all unfolding finitely_generated_ideal_def
    by (metis finite.emptyI finite_insert ideal_ideal_generated principal_ideal_def)
  have a_in_d: "a \<in> ideal_generated {d}"
    using ideal_d ideal_generated_subset_generator by blast
  have b_in_d: "b \<in> ideal_generated {d}"
    using ideal_d ideal_generated_subset_generator by blast
  have d_in_ab: "d \<in> ideal_generated {a,b}"
    using ideal_d ideal_generated_subset_generator by auto
  obtain f where "(\<Sum>i\<in>{a,b}. f i * i) = d" using obtain_sum_ideal_generated[OF d_in_ab] by auto
  from this obtain p q where d_eq: "d = p*a + q*b" using sum_two_elements' by blast
  moreover have d_dvd_a: "d dvd a"
    by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset insert_commute
        subset_insertI)
  moreover have "d dvd b"
    by (metis dvd_ideal_generated_singleton ideal_d ideal_generated_subset subset_insertI)
  moreover have "d' dvd d" if d'_dvd: "d' dvd a \<and> d' dvd b" for d'
  proof -
    obtain s1 s2 where s1_dvd: "a = s1*d'" and s2_dvd: "b = s2*d'"
      using mult.commute d'_dvd unfolding dvd_def by auto
    have "d = p*a + q*b" using d_eq .
    also have "...= p * s1 * d' + q * s2 *d'" unfolding s1_dvd s2_dvd by auto
    also have "... = (p * s1 + q * s2) * d'" by (simp add: ring_class.ring_distribs(2))
    finally show "d' dvd d" using mult.commute unfolding dvd_def by auto
  qed
  ultimately show "\<exists>p q d. p * a + q * b = d \<and> d dvd a \<and> d dvd b
  \<and> (\<forall>d'. d' dvd a \<and> d' dvd b \<longrightarrow> d' dvd d)" by auto
qed
end

context bezout_ring
begin

lemma exists_bezout_extended:
  assumes S: "finite S" and ne: "S \<noteq> {}"
  shows "\<exists>f d. (\<Sum>a\<in>S. f a * a) = d \<and> (\<forall>a\<in>S. d dvd a) \<and> (\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
  using S ne
proof (induct S)
  case empty
  then show ?case by auto
next
  case (insert x S)
  show ?case
  proof (cases  "S={}")
    case True
    let ?f = "\<lambda>x. 1"
    show ?thesis by (rule exI[of _ ?f], insert True, auto)
  next
    case False note ne = False
    note x_notin_S = insert.hyps(2)
    obtain f d where sum_eq_d: "(\<Sum>a\<in>S. f a * a) = d"
      and d_dvd_each_a: "(\<forall>a\<in>S. d dvd a)"
      and d_is_gcd: "(\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
      using insert.hyps(3)[OF ne] by auto
    have "\<exists>p q d'. p * d + q * x = d' \<and> d' dvd d \<and> d' dvd x \<and> (\<forall>c. c dvd d \<and> c dvd x \<longrightarrow> c dvd d')"
      using exists_bezout by auto
    from this obtain p q d' where pd_qx_d': "p*d + q*x = d'"
      and d'_dvd_d: "d' dvd d" and d'_dvd_x: "d' dvd x"
      and d'_dvd: "\<forall>c. (c dvd d \<and> c dvd x) \<longrightarrow> c dvd d'" by blast
    let ?f = "\<lambda>a. if a = x then q else p * f a"
    have "(\<Sum>a\<in>insert x S. ?f a * a) = d'"
    proof -
      have "(\<Sum>a\<in>insert x S. ?f a * a) = (\<Sum>a\<in>S. ?f a * a) + ?f x * x"
        by (simp add: add_commute insert.hyps(1) insert.hyps(2))
      also have "... = p * (\<Sum>a\<in>S. f a * a) + q * x"
        unfolding sum_distrib_left
        by (auto, rule sum.cong, insert x_notin_S,
            auto simp add: mult.semigroup_axioms semigroup.assoc)
      finally show ?thesis using pd_qx_d' sum_eq_d by auto
    qed
    moreover have "(\<forall>a\<in>insert x S. d' dvd a)"
      by (metis d'_dvd_d d'_dvd_x d_dvd_each_a insert_iff local.dvdE local.dvd_mult_left)
    moreover have " (\<forall>c. (\<forall>a\<in>insert x S. c dvd a) \<longrightarrow> c dvd d')"
      by (simp add: d'_dvd d_is_gcd)
    ultimately show ?thesis by auto
  qed
qed

end

lemma ideal_generated_empty: "ideal_generated {} = {0}"
  unfolding ideal_generated_def using ideal_generated_0
  by (metis empty_subsetI ideal_generated_def ideal_generated_subset ideal_ideal_generated
      ideal_not_empty subset_singletonD)

lemma bezout_imp_all_fin_gen_ideals_are_principal:
  fixes I::"'a :: bezout_ring set"
  assumes fin: "finitely_generated_ideal I"
  shows "principal_ideal I"
proof -
  obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I"
    using fin unfolding finitely_generated_ideal_def by auto
  show ?thesis
  proof (cases "S = {}")
    case True
    then show ?thesis
      using ideal_gen_S unfolding True
      using ideal_generated_empty ideal_generated_0 principal_ideal_def by fastforce
  next
    case False note ne = False
    obtain d f where sum_S_d: "(\<Sum>i\<in>S. f i * i) = d"
    and d_dvd_a: "(\<forall>a\<in>S. d dvd a)" and d_is_gcd: "(\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
      using exists_bezout_extended[OF fin_S ne] by auto
    have d_in_S: "d \<in> ideal_generated S"
      by (metis fin_S ideal_def ideal_generated_subset_generator
          ideal_ideal_generated sum_S_d sum_left_ideal)
    have "ideal_generated {d} \<subseteq> ideal_generated S"
      by (rule ideal_generated_singleton_subset[OF d_in_S fin_S])
    moreover have "ideal_generated S \<subseteq> ideal_generated {d}"
    proof
      fix x assume x_in_S: "x \<in> ideal_generated S"
      obtain f where sum_S_x: "(\<Sum>a\<in>S. f a * a) = x"
        using fin_S obtain_sum_ideal_generated x_in_S by blast
      have d_dvd_each_a: "\<exists>k. a = k * d" if "a \<in> S" for a
        by (metis d_dvd_a dvdE mult.commute that)
      let ?g = "\<lambda>a. SOME k. a = k*d"
      have "x = (\<Sum>a\<in>S. f a * a)" using sum_S_x by simp
      also have "... = (\<Sum>a\<in>S. f a * (?g a * d))"
      proof (rule sum.cong)
        fix a assume a_in_S: "a \<in> S"
        obtain k where a_kd: "a = k * d" using d_dvd_each_a a_in_S by auto
        have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd)
        thus "f a * a = f a * ((SOME k. a = k * d) * d)" by auto
      qed (simp)
      also have "... = (\<Sum>a\<in>S. f a * ?g a * d)" by (rule sum.cong, auto)
      also have "... = (\<Sum>a\<in>S. f a * ?g a)*d" using sum_distrib_right[of _ S d] by auto
      finally show "x \<in> ideal_generated {d}"
        by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right
            ideal_generated_in singletonI)
    qed
    ultimately show ?thesis unfolding principal_ideal_def using ideal_gen_S by auto
  qed
qed

text \<open>Now we have the required lemmas to prove the theorem that states that
  a ring is B\'ezout ring if and only if every
  finitely generated ideal is principal. They are the following ones.

\begin{itemize}
\item @{text "all_fin_gen_ideals_are_principal_imp_bezout"}
\item @{text "bezout_imp_all_fin_gen_ideals_are_principal"}
\end{itemize}

However, in order to prove the final lemma, we need the lemmas with no type restrictions.
For instance, we need a version of theorem @{text "bezout_imp_all_fin_gen_ideals_are_principal"}
as

@{text "OFCLASS('a,bezout_ring) \<Longrightarrow>"} the theorem with generic types
  (i.e., @{text "'a"} with no type restrictions)

or as

@{text "class.bezout_ring _ _ _ _ \<Longrightarrow>"} the theorem with generic
  types (i.e., @{text "'a"} with no type restrictions)
\<close>

(*A possible workaround is to adapt the proof*)
(*
lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory:
  assumes a1: "class.bezout_ring ( * ) (1::'a::comm_ring_1) (+) 0 (-) uminus" (*Me da igual esto que OFCLASS*)
  shows "\<forall>I::'a set. finitely_generated_ideal I \<longrightarrow> principal_ideal I"
proof (rule allI, rule impI)
  fix I::"'a set" assume fin: "finitely_generated_ideal I"
  interpret a: bezout_ring "( * )" "(1::'a)" "(+)" 0 "(-)" uminus using a1 .
  interpret dvd "( * )::'a\<Rightarrow>'a\<Rightarrow>'a" .
  interpret b: comm_monoid_add "(+)" "(0::'a)" using a1 by intro_locales
  have c: " class.comm_monoid_add (+) (0::'a)"  using a1 by intro_locales
  have [simp]: "(dvd.dvd ( * ) d a) = (d dvd a)" for d a::'a
    by (auto simp add: dvd.dvd_def dvd_def)
  have [simp]: "comm_monoid_add.sum (+) 0 (\<lambda>a. f a * a) S = sum (\<lambda>a. f a * a) S"
    for f and S::"'a set"
    unfolding sum_def unfolding comm_monoid_add.sum_def[OF c] ..
  obtain S where fin_S: "finite S" and ideal_gen_S: "ideal_generated S = I"
    using fin unfolding finitely_generated_ideal_def by auto
  show "principal_ideal I"
  proof (cases "S = {}")
    case True
    then show ?thesis
      using ideal_gen_S unfolding True
      using ideal_generated_empty ideal_generated_0 principal_ideal_def by fastforce
  next
    case False note ne = False
    obtain d f where sum_S_d: "(\<Sum>i\<in>S. f i * i) = d"
    and d_dvd_a: "(\<forall>a\<in>S. d dvd a)" and d_is_gcd: "(\<forall>d'. (\<forall>a\<in>S. d' dvd a) \<longrightarrow> d' dvd d)"
      using a.exists_bezout_extended[OF fin_S ne] by auto
    have d_in_S: "d \<in> ideal_generated S"
      by (metis fin_S ideal_def ideal_generated_subset_generator
          ideal_ideal_generated sum_S_d sum_left_ideal)
    have "ideal_generated {d} \<subseteq> ideal_generated S"
      by (rule ideal_generated_singleton_subset[OF d_in_S fin_S])
    moreover have "ideal_generated S \<subseteq> ideal_generated {d}"
    proof
      fix x assume x_in_S: "x \<in> ideal_generated S"
      obtain f where sum_S_x: "(\<Sum>a\<in>S. f a * a) = x"
        using fin_S obtain_sum_ideal_generated x_in_S by blast
      have d_dvd_each_a: "\<exists>k. a = k * d" if "a \<in> S" for a
        by (metis d_dvd_a dvdE mult.commute that)
      let ?g = "\<lambda>a. SOME k. a = k*d"
      have "x = (\<Sum>a\<in>S. f a * a)" using sum_S_x by simp
      also have "... = (\<Sum>a\<in>S. f a * (?g a * d))"
      proof (rule sum.cong)
        fix a assume a_in_S: "a \<in> S"
        obtain k where a_kd: "a = k * d" using d_dvd_each_a a_in_S by auto
        have "a = ((SOME k. a = k * d) * d)" by (rule someI_ex, auto simp add: a_kd)
        thus "f a * a = f a * ((SOME k. a = k * d) * d)" by auto
      qed (simp)
      also have "... = (\<Sum>a\<in>S. f a * ?g a * d)" by (rule sum.cong, auto)
      also have "... = (\<Sum>a\<in>S. f a * ?g a)*d" using sum_distrib_right[of _ S d] by auto
      finally show "x \<in> ideal_generated {d}"
        by (meson contra_subsetD dvd_ideal_generated_singleton' dvd_triv_right
            ideal_generated_in singletonI)
    qed
    ultimately show ?thesis unfolding principal_ideal_def using ideal_gen_S by auto
  qed
qed
*)

text \<open>Thanks to local type definitions, we can obtain it automatically by means
  of @{text "internalize-sort"}.\<close>

lemma bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory:
  assumes a1: "class.bezout_ring (*) (1::'b::comm_ring_1) (+) 0 (-) uminus" (*It is algo possible to prove it using OFCLASS*)
  shows "\<forall>I::'b set. finitely_generated_ideal I \<longrightarrow> principal_ideal I"
  using bezout_imp_all_fin_gen_ideals_are_principal[internalize_sort "'a::bezout_ring"]
  using a1 by auto

text \<open>The standard library does not connect @{text "OFCLASS"} and @{text "class.bezout_ring"}
in both directions. Here we show that @{text "OFCLASS \<Longrightarrow> class.bezout_ring"}. \<close>

lemma OFCLASS_bezout_ring_imp_class_bezout_ring:
  assumes "OFCLASS('a::comm_ring_1,bezout_ring_class)"
  shows "class.bezout_ring ((*)::'a\<Rightarrow>'a\<Rightarrow>'a) 1 (+) 0 (-) uminus"
  using assms
  unfolding bezout_ring_class_def class.bezout_ring_def
  using conjunctionD2[of "OFCLASS('a, comm_ring_1_class)"
                         "class.bezout_ring_axioms ((*)::'a\<Rightarrow>'a\<Rightarrow>'a) (+)"]
  by (auto, intro_locales)

text \<open>The other implication can be obtained
  by thm @{text "Rings2.class.Rings2.bezout_ring.of_class.intro"} \<close>
thm Rings2.class.Rings2.bezout_ring.of_class.intro

(*OFCLASS is a proposition (Prop), and then the following statement is not valid.*)

(*
lemma
  shows "(\<forall>I::'a::comm_ring_1 set. finitely_generated_ideal I \<longrightarrow> principal_ideal I)
    = OFCLASS('a, bezout_ring_class)"
*)

(*Thus, we use the meta-equality and the meta universal quantifier.*)
text \<open>Final theorem (with OFCLASS)\<close>
lemma bezout_ring_iff_fin_gen_principal_ideal:
    "(\<And>I::'a::comm_ring_1 set. finitely_generated_ideal I \<Longrightarrow> principal_ideal I)
    \<equiv> OFCLASS('a, bezout_ring_class)"
proof
  show "(\<And>I::'a::comm_ring_1 set. finitely_generated_ideal I \<Longrightarrow> principal_ideal I)
    \<Longrightarrow> OFCLASS('a, bezout_ring_class)"
    using all_fin_gen_ideals_are_principal_imp_bezout [where ?'a='a] by auto
  show "\<And>I::'a::comm_ring_1 set. OFCLASS('a, bezout_ring_class)
    \<Longrightarrow> finitely_generated_ideal I \<Longrightarrow> principal_ideal I"
    using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory[where ?'b='a]
    using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a] by auto
qed

text \<open>Final theorem (with @{text "class.bezout_ring"})\<close>

lemma bezout_ring_iff_fin_gen_principal_ideal2:
    "(\<forall>I::'a::comm_ring_1 set. finitely_generated_ideal I \<longrightarrow> principal_ideal I)
    = (class.bezout_ring ((*)::'a\<Rightarrow>'a\<Rightarrow>'a) 1 (+) 0 (-) uminus)"
proof
  show "\<forall>I::'a::comm_ring_1 set. finitely_generated_ideal I \<longrightarrow> principal_ideal I
      \<Longrightarrow> class.bezout_ring (*) 1 (+) (0::'a) (-) uminus"
    using all_fin_gen_ideals_are_principal_imp_bezout[where ?'a='a]
    using OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a]
    by auto
  show "class.bezout_ring (*) 1 (+) (0::'a) (-) uminus \<Longrightarrow> \<forall>I::'a set.
    finitely_generated_ideal I \<longrightarrow> principal_ideal I"
    using bezout_imp_all_fin_gen_ideals_are_principal_unsatisfactory by auto
qed

end

subset_name: curated


TITLE: Double cover of $SO(2)$
QUESTION [1 upvotes]: In most textbooks i found that $SPIN(2)$ group is isomorphic to $U(1)$. That is $U(1)$ is double cover of $SO(2)$. But $U(1)$ is isomorphic to $SO(2)$.
So how can it be? Does  this definition of double cover does not work for $n=2$ ?

REPLY [3 votes]: As it happens $U(1)$ is an $n$-fold cover of itself for all positive integers $n$ by the mapping $e^{it}\mapsto e^{nit}$. Therefore it is also an $n$-fold covering of $SO(2)$ for all $n$.


TITLE: Fourier coefficients of even and odd functions
QUESTION [1 upvotes]: I am unable to confirm the following. If a signal is odd, then does the following hold?
$$a_k = -a_{-k}$$
If a signal is even, then: $$a_k = a_{-k}$$ If the aforementioned qualities hold, then is the following true?
If a signal is odd and the period is $2k$, then $a_k = -a_{-k} = 0$.

REPLY [2 votes]: Your first two affirmations hold.

Let $f$ be $p$-periodic and $f \in L^1[-p/2,p/2]$. Then the Fourier coefficients of $f$ are
$$
\hat{f}(k) = \frac{1}{p} \int_{-p/2}^{p/2} f(t) e^{-i2\pi k t/p} \,dt
$$
If $f$ is odd then the change of variable $u=-t$ gives (we can keep the interval of integration $[-p/2,p/2]$ by $p$-periodicity)
\begin{align}
\hat{f}(k) &= -\frac{1}{p} \int_{-p/2}^{p/2} (-f(-t)) e^{i2\pi k t/p} \,dt \\
&= -\frac{1}{p} \int_{-p/2}^{p/2} f(t) e^{-i2\pi (-k) t/p} \,dt \\
&= -\hat{f}(-k)
\end{align}
If $f$ is even then the same change of variable gives
\begin{align}
\hat{f}(k) &= \frac{1}{p} \int_{-p/2}^{p/2} f(-t) e^{i2\pi k t/p} \,dt \\
&= \frac{1}{p} \int_{-p/2}^{p/2} f(t) e^{-i2\pi (-k) t/p} \,dt \\
&= \hat{f}(-k)
\end{align}

I don't think your third affirmation holds.

Take $f(t):=\sin(\pi t)$. Then $f$ is odd and of period $2\cdot1$. Yet, we can calculate $\hat{f}(1)=-i/2 \neq 0$.


TITLE: Banach's fixed point theorem
QUESTION [1 upvotes]: For the following question, we are to use Banach's fixed point theorem to show that $\{x_n\}$ converges to the root of the polynomial: $x^4 - 4x^2 - x + 4 = 0$ ; lying between $\sqrt{3}$ and $2$. Let ${x_1} =  \sqrt{2}$ and $x_{n+1} = \sqrt {2 + \sqrt{x_n}}$.
I know the theorem states that if $f: X \to X$ is a contraction of a complete metric space X, then f has a unique fixed point.
I think I need to prove that f has a contraction, but I don't quite understand how to proceed with that. Is that the right approach or is there another approach that would be more efficient, per se.
Thank you in advance.

REPLY [3 votes]: Let $X=[\sqrt{3},2]$ and $f(x)= \sqrt {2 + \sqrt{x}}$. $X$ is a complete metric space.
Show that $f(X) \subset X$ and that there is $q \in (0,1)$ such that  $|f'(x)| \le q$ for all $x \in X$. By the mean value theorem:
$|f(x)-f(y)| \le q|x-y|$ for all $x,y \in X$.
Hence there is $x \in X$ with $f(x)=x$.
But: $f(x)=x \iff x^4 - 4x^2 - x + 4 = 0$.


TITLE: Write $\frac{2}{1+x}$ as an infinite geometric series
QUESTION [2 upvotes]: The question on the test was to write $\frac{2}{1+x}$ as an infinite geometric series (IGS).

My thought is that the sum of an IGS is $S = \dfrac{a_1}{1-r}$ .  So, I viewed $a_1$ as = 2 and $r = (-x)$.
Writing this in the form of an IGS:
$$\sum_{i=1}^\infty {2\cdot{(-x)}^{i-1}}$$
Am I on the correct path here?

REPLY [1 votes]: community wiki post so that the question can be closed
Your are correct.


text:
\begin{document}
\title[On a Subdiffusive Tumour Growth Model with Fractional Time Derivative]{On a Subdiffusive Tumour Growth Model \\ with Fractional Time Derivative}

\author{Marvin Fritz$^1$, Christina Kuttler$^1$, Mabel L. Rajendran$^{1,*}$, \\ Barbara Wohlmuth$^1$, Laura Scarabosio$^2$}
\address{${}^1$Department of Mathematics, Technical University of Munich}
\address{${}^2$Institute for Mathematics, Astrophysics and Particle Physics, Radboud University}

\email{\{fritzm, kuttler, rajendrm, wohlmuth\}@ma.tum.de; scarabosio@science.ru.nl}
\subjclass[2020]{35K35, 35A01, 35D30, 35Q92, 65M60, 35R11.}
\keywords{subdiffusive tumour growth; mechanical deformation; fractional time derivative; nonlinear partial differential equation; well-posedness}
\thanks{${}^*$Corresponding author}

\maketitle

\begin{abstract}
In this work, we present and analyse a system of coupled partial differential equations, which models tumour growth under the influence of subdiffusion, mechanical effects, nutrient supply, and chemotherapy. The subdiffusion of the system is modelled by a time fractional derivative in the equation governing the volume fraction of the tumour cells. The mass densities of the nutrients and the chemotherapeutic agents are modelled by reaction diffusion equations. We prove the existence and uniqueness of a weak solution to the model via the Faedo--Galerkin method and the application of appropriate compactness theorems. Lastly, we propose a fully discretised system and illustrate the effects of the fractional derivative and the influence of the fractional parameter in numerical examples.
\end{abstract}

\input{Introduction.tex}
\input{MathematicalModel.tex}
\input{Preliminaries.tex}
\input{Analysis.tex}
\input{NumericalDiscretization.tex}
\input{ConvolutionQuadrature.tex}
\input{NumericalSimulations.tex}

\section{Conclusions}
We have presented a new model for tumour growth with fractional time derivatives, including mechanical effects and treatment by chemotherapy. Existence and uniqueness of a weak solution to the coupled, nonlinear model are obtained by a Galerkin method. Numerical experiments, based on low order finite elements in space and convolution quadrature in time, show that the order of the fractional time derivative influences strongly the evolution. Using the fractional order as an additional parameter results in a larger model class. This can be of future interest for calibration of the model parameters by experimental data.

\section*{Funding}
Deutsche Forschungsgemeinschaft (DFG) through TUM International Graduate School of Science and Engineering (GSC 81); Laura Bassi Postdoctoral Fellowship (Technical University of Munich; to M.L.R.); and DFG (WO-671 11-1 to M.F., L.S. and B.W.).

\newpage

\bibliography{references.bib}
\bibliographystyle{siam}

\newpage

\appendix
\input{Appendix_Finite_Dimension_Existence.tex}

\end{document}

config: arxiv


text:
\begin{document}

\title{Designing Stable Elections}

\author{Steven Heilman}
\address{Department of Mathematics, University of Southern California, Los Angeles, CA 90089-2532}
\email{stevenmheilman@gmail.com}
\date{\today}
\thanks{Supported by NSF Grant CCF 1911216 and DMS 1839406.  Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the National Science Foundation.}

\subjclass[2010]{60-02, 91B14, 91B12, 60C05}
\keywords{social choice theory, voting theory, noise stability, majority, plurality}

\maketitle

\section{Introduction}\label{secintro}

Suppose votes have been cast in an election between two candidates, and then an adversary can select a fixed number of votes to change.  Which voting method best preserves the outcome of the election?  A majority vote does, among all voting methods where both candidates have an equal chance of winning the election.

Now, suppose votes have been cast in an election between two candidates, and then each vote is randomly changed with a small probability, independently of the other votes.  It is desirable to keep the outcome of the election the same, regardless of the changes to the votes.  It is well known that the US electoral college system is more than 4 times more likely to have a changed outcome due to vote corruption, when compared to a majority vote.  In fact, Mossel, O'Donnell and Oleszkiewicz proved in 2005 that the majority voting method is most stable to this random vote corruption, among voting methods where each person has a small influence on the election.  Below, we survey the design of elections that are resilient to attempted interference by third parties.  We discuss some recent progress on the analogous result for elections between more than two candidates.  In this case, plurality should be most stable to corruption in votes.  We briefly discuss ranked choice voting methods (where a vote is a ranked list of candidates).

\subsection{Condorcet's Paradox}

Applications of mathematics to the analysis of elections perhaps began with Marquis de Condorcet in the 1700s.  Condorcet's famous paradox demonstrates that an election method that uses ranked preferences of voters might not have a sensible winner.  Consider the following ranking of three candidates $a,b$ and $c$ between three voters $1,2$ and $3$.

\begin{table}[htbp!]
\centering
\begin{tabular}{|c||c|c|c|}
\hline
Voter & Rank 1 & Rank 2 & Rank 3\\
\hline
\hline
1 & $a$ & $b$ & $c$\\
\hline
2 & $b$ & $c$ & $a$\\
\hline
3 & $c$ & $a$ & $b$\\
\hline
\end{tabular}
\caption{Three voters (one for each row of the table) provide rankings of three candidates $a,b$ and $c$.  For example, voter $1$ most prefers candidate $a$.}
\label{table1}
\end{table}

If we ignore candidate $b$, then voters $2$ and $3$ prefer $c$ over $a$, while voter $1$ prefers $a$ over $c$.  So, using a majority rule for these preferences, the voters prefer $c$ over $a$.

\begin{table}[htbp!]
\centering
\begin{tabular}{|c||c|c|}
\hline
Voter & Rank 1 & Rank 2 \\
\hline
\hline
1 & $a$ &  $c$\\
\hline
2 & $c$ & $a$\\
\hline
3 & $c$ & $a$ \\
\hline
\end{tabular}
\caption{If candidate $b$ is ignored in Table \ref{table1}, the remaining rankings of candidates $a$ and $c$ indicate that $c$ is the preferred by the majority of voters.}
\label{table2}
\end{table}

If we ignore candidate $c$ in Table \ref{table1}, then voters $1$ and $3$ prefer $a$ over $b$, while voter $2$ prefers $b$ over $a$.  So, using a majority rule again, the voters prefer $a$ over $b$.

Finally, if we ignore candidate $a$ in Table \ref{table1}, then voters $1$ and $2$ prefer $b$ over $c$, while voter $3$ prefers $c$ over $b$.  So, using a majority rule, the voters prefer $b$ over $c$.

\begin{figure}[h!]

   \def\svgwidth{.3\textwidth}
    \input{vote1.pdf_tex} \\

\end{figure}

In conclusion, the voters prefer $a$ over $b$, they prefer $b$ over $c$, and they prefer $c$ over $a$.  So, \textit{no one has won the election}!  This observation is known as Condorcet's paradox.  The simplest way to use rankings of candidates might lead to no one winning the election.

In fact, if we compare pairs of candidates using something other than a majority rule, then some analogue of Condorcet's paradox must still occur, \textit{unless} we ignore all voters except for one (a dictatorship).  This statement can be formalized as Arrow's Impossibility Theorem.

\subsection{Voting Power}

\begin{wrapfigure}{r}{0.5\textwidth}
\vspace{-1cm}
   \def\svgwidth{.5\textwidth}
    \input{vote2.pdf_tex} \\

    \vspace{-2cm}
\end{wrapfigure}

Game Theorists such as Shapley, Shubik and Banzhaf in the 1950s and 1960s further developed the mathematical and economical analysis of voting methods.  As an illustrative example, we consider the 1965 restructuring of the UN security council.

\begin{vmethod}[Pre-1965 UN Security Council]
In pre-1965 rules, the UN security council had five permanent members, and six nonpermanent members.  A resolution passes in the security council only if:
\begin{itemize}
\item  All five permanent members want it to pass, and
\item at least \textit{two} nonpermanent members want it to pass.
\end{itemize}
\end{vmethod}

\begin{wrapfigure}{r}{0.5\textwidth}
\vspace{-4cm}
   \def\svgwidth{.5\textwidth}
    \input{vote3.pdf_tex} \\

    \vspace{-2cm}
\end{wrapfigure}

In particular, a single permanent member can effectively veto a resolution by voting ``no'' on that resolution.  This voting method was called unfair for the nonpermanent members, so it was restructured in 1965.  After the restructuring, the council had the following form (still in use today).
\begin{vmethod}[Post-1965 UN Security Council]
The UN security council has five permanent members, and now ten nonpermanent members.  A resolution passes in the council only if:
\begin{itemize}
\item  All five permanent members want it to pass, and
\item at least \textit{four} nonpermanent members want it to pass.
\end{itemize}
\end{vmethod}

A rather vague question is then:

\begin{question}\label{q1}
Are the Post-1965 rules more equitable for nonpermanent members of the UN security council than Pre-1965 rules?
\end{question}

There are various ways to answer this question.  One answer, provided by Banzhaf, is to consider the \textbf{power} of a voter in each voting method, i.e. the relative ability of a voter to cause a resolution to pass by changing their vote.  Suppose we label the post-1965 UN security council members by the integers $1$ through $15$, where the numbers $1,2,3,4,5$ represent the five permanent members of the council, and the numbers $6,7,\ldots,15$ represent nonpermament members.  Then, for any integer $i$ between $1$ and $15$, let $b_{i}$ be the number of combinations of votes of members of the council (other than voter $i$), such that when voter $i$ changes their vote from ``no'' to ``yes,'' the resolution changes from not passing to passing.  The \textbf{Banzhaf power index} of a voter $i$ is defined to be the following ratio
$$\frac{b_{i}}{b_{1}+b_{2}+\cdots+b_{15}}.$$

For example, in the post-1965 rules, what would it take for a nonpermanent member to cause the resolution to pass?  First, all permanent members would have to vote ``yes.''  Then, exactly three other nonpermanent members out of nine would vote yes.  So, the number of combinations of votes other members would make is: the number of ways to select $3$ members from a set of $9$, i.e. $\binom{9}{3}=\frac{9\cdot 8\cdot 7}{3\cdot 2}=84$.  So, $b_{6}=b_{7}=\cdots=b_{15}=84$.

In the post-1965 rules, what would it take for a permanent member to cause the resolution to pass?  First, all other permanent members would have to vote ``yes.''  Then, at least four nonpermanent members out of 10 would vote yes.  So, the number of combinations of votes other members would make is: the number of ways to select at least $4$ members from a set of $10$.  This number is $\binom{10}{4}+\binom{10}{5}+\cdots+\binom{10}{10}=848$.  So, $b_{1}=b_{2}=\cdots=b_{5}=848$.

Similar considerations apply for pre-1965 rules.  We summarize the Banzhaf power indices in the following table.

\begin{table}[htbp!]\renewcommand{\arraystretch}{1.5}
\centering
\begin{tabular}{|l|p{5cm}|p{5cm}|c|}
\hline
Voting Method & Banzhaf Power Index for \textit{Non}-Permament Member & Banzhaf Power Index for Permament Member\\
\hline
Pre-1965 Rules & $\frac{5}{6\cdot 5+5\cdot 57}\approx .0159$ & $\frac{57}{6\cdot 5+5\cdot 57}\approx .181$ \\
\hline
Post-1965 Rules & $\frac{84}{10\cdot 84+5\cdot 848}\approx .0165$ & $\frac{848}{10\cdot 84+5\cdot 848}\approx .167$ \\
\hline
\end{tabular}
\caption{Banzhaf Power Indices for UN Security Council Voting Methods}

\end{table}

In summary, the post-1965 rules give more power to non-permanent members, and less power to permanent members of the UN Security Council.  So, according to Banzhaf's definition of voting power, the answer to Question \ref{q1} is: yes.

\subsection{Voting Methods as Functions}

\begin{wrapfigure}{r}{0.5\textwidth}

   \def\svgwidth{.5\textwidth}
    \input{vote4.pdf_tex} \\

    \vspace{-.5cm}
\end{wrapfigure}

Suppose we run an election between two candidates with $n$ voters, where $n$ is a large integer.  For convenience, we denote the two candidates as $+1$ and $-1$ rather than $a$ and $b$.  If person $i$ votes for candidate $1$, we define $x_{i}=1$, and if person $i$ votes for candidate $-1$, we define $x_{i}=-1$.  We then can then make a list of votes as
$$x=(x_{1},x_{2},\ldots,x_{n}).\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$$
A \textbf{voting method} is a function $f$ whose input is the votes $x$ and whose output is the winner of election.  That is, $f(x)=1$ denotes candidate $1$ winning the election when the votes are $x$, and $f(x)=-1$ denotes candidate $-1$ winning the election when the votes are $x$.

\begin{wrapfigure}{r}{0.5\textwidth}

   \def\svgwidth{.5\textwidth}
    \input{vote41.pdf_tex} \\

\vspace{-2cm}
\end{wrapfigure}
Some examples of voting methods appear below.

\begin{example}
The \textbf{majority function} is the function
$$f(x)=\mathrm{sign}(x_{1}+x_{2}+\cdots+x_{n}).\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$$
If there are more $+1$ votes than $-1$ votes, then $f(x)=1$.  And if there are more $-1$ votes than $+1$ votes, then $f(x)=-1$.  That is, $f$ agrees with our usual notion of majority: the candidate receiving the most votes wins the election.  (To guarantee that someone wins the election, we could just assume that $n$ is odd, so that $f$ never takes the value $0$.)

\end{example}

\begin{example}
A \textbf{dictator function} is a function of the form
$$f(x)=x_{1}.\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$$
That is, the vote of the first person is the winner of the election.  In this way, $f$ agrees with our usual notion of dictator: all votes are ignored, except for one.  More generally, if $1\leq i\leq n$, a dictator is a function of the form $$f(x)=x_{i}.$$
\end{example}

\begin{example}
If $w_{1},\ldots,w_{n}$ are fixed real numbers, a \textbf{weighted majority function} on $n$ voters is a function of the form
$$f(x)=\mathrm{sign}(w_{1}x_{1}+w_{2}x_{2}+\cdots+w_{n}x_{n}).$$
If $w_{i}$ is large for some $1\leq i\leq n$, this corresponds to assigning more ``weight'' (i.e. more voting power, or more ``say'') to the $i^{th}$ voter.  And if $w_{i}$ is small, this corresponds to assigning less ``weight'' (i.e. less voting power, or less ``say'') to the $i^{th}$ voter.
\end{example}

\begin{figure}[h!]

 \def\svgwidth{\textwidth}
 \tiny
    \input{vote5.pdf_tex} \\

    \normalsize
    \caption{An iterated majority function with $m=3$ ``states.''}\label{itmaj}
\end{figure}

\begin{example}\label{itmajex}
A two-layer \textbf{iterated majority function} is a function of the form
$$f(x)=g(f_{1}(x),f_{2}(x),\ldots,f_{m}(x)),$$
where $f_{1},f_{2},\ldots,f_{m}$ are each weighted majority functions on $n$ voters, and $g$ is a weighted majority function $m$ voters.

A two-layer iterated majority function is similar to an electoral college system with $m$ states.  The US electoral college system then corresponds to $m=51$.
\end{example}
\begin{remark}
In learning theory, the iterated majority function is sometimes called a two-layer neural network with boolean activation function.  The lines and nodes in Figure \ref{itmaj} are then interpreted as axons and neurons, respectively.
\end{remark}

In the ensuing discussion, it is more convenient to replace the Banzhaf power index of a voter with the (almost identical) notion of \textbf{influence} of a voter.

\begin{definition}[\embolden{Influences}]\label{infdef}
Let $f\colon\{-1,1\}^{n}\to\{-1,1\}$ be a voting method.  Let $1\leq i\leq n$ be an integer.  Define the \textbf{influence} of the $i^{th}$ voter on $f$, denote $\mathrm{Inf}_{i}(f)$, as
\begin{flalign*}
\mathrm{Inf}_{i}(f)
&=\frac{\mbox{\# of combinations of votes where the $i^{th}$ voter can change the election's outcome}}{\mbox{\# of combinations  of votes of all voters}}\\
&=\frac{\#\{(x_{1},\ldots,x_{n})\in\{-1,1\}^{n}\colon f(x_{1},\ldots,x_{n})\neq f(x_{1},\ldots,x_{i-1},-x_{i},x_{i+1},\ldots,x_{n})\}}{\#\{(x_{1},\ldots,x_{n})\in\{-1,1\}^{n}\}}.
\end{flalign*}
That is, $\mathrm{Inf}_{i}(f)$ is the probability that the $i^{th}$ voter can change the outcome of the election, when other voters are equally likely to vote for either candidate.
\end{definition}
\begin{example}
The numbers $b_{1},\ldots,b_{n}$ used to define the Banzhaf power indices are just the influences, multiplied by $2^{n}$.  For example, in the post-1965 UN Security council voting method $f\colon\{-1,1\}^{15}\to\{-1,1\}$ with $n=15$ voters,
$$\mathrm{Inf}_{1}(f)=\cdots=\mathrm{Inf}_{5}(f)=\frac{848}{2^{15}}\approx .0259,\qquad
\mathrm{Inf}_{6}(f)=\cdots=\mathrm{Inf}_{15}(f)=\frac{84}{2^{15}}\approx .00256.$$
Put another way, the Banzhaf power indices are the influences, multiplied by a number causing them to sum to $1$.

\begin{table}[htbp!]\renewcommand{\arraystretch}{1.5}
\centering
\begin{tabular}{|l|p{4cm}|p{4cm}|c|}
\hline
Voting Method & Influence for \textit{Non}-Permament Member & Influence for Permament Member\\
\hline
Pre-1965 Rules & $\frac{5}{2^{11}}\approx .00244$ & $\frac{57}{2^{11}}\approx .0278$ \\
\hline
Post-1965 Rules & $\frac{84}{2^{15}}\approx .00256$ & $\frac{848}{2^{15}}\approx .0259$ \\
\hline
\end{tabular}
\caption{Influences for UN Security Council Voting Methods}

\end{table}

As above, we observe that a non-permanent member has a higher probability of affecting the outcome of a resolution in post-1965 rules.
\end{example}
\begin{example}\label{dictex}
When $f$ is a dictator function of the form $f(x)=x_{1}$, then the first voter can always change the outcome of the election, and the other voters cannot, so
$$I_{1}(f)=1,\quad I_{2}(f)=\cdots=I_{n}(f)=0.$$
When $f$ is a majority function $f(x)=\mathrm{sign}(x_{1}+\cdots+x_{n})$, then an application of Stirling's formula implies that for all $1\leq i\leq n$, $\lim_{n\to\infty}\sqrt{n}I_{i}(f)=\sqrt{\frac{2}{\pi}}$, i.e.
$$I_{1}(f)= I_{2}(f)=\cdots=I_{n}(f)=(1+o(1))\sqrt{\frac{2}{\pi}}\frac{1}{\sqrt{n}}.$$
To see this, note that if $n$ is even, recall that Stirling's Formula implies that
$$\binom{n}{n/2}=\frac{n!}{[(n/2)]!}=(1+o(1))\frac{1}{\sqrt{2\pi}}\frac{\sqrt{n}}{n/2}2^{n}=(1+o(1))2^{n}\frac{1}{\sqrt{n}}\sqrt{\frac{2}{\pi}}.$$
Therefore, $\lim_{n\to\infty}\sqrt{n}I_{i}(f)=\lim_{n\to\infty}(1+o(1))\frac{1}{\sqrt{2\pi}}\frac{2^{n}}{2^{n}}=\frac{1}{\sqrt{2\pi}}$, for all $1\leq i\leq n$.
\end{example}
Perhaps it is a compelling reason to vote in a majority election with one hundred million voters when your probability of changing the election's outcome is around $1$ in ten thousand.

\section{Adversarial Corruption in Voting}

\subsection{Two Candidates}

\begin{wrapfigure}{r}{0.52\textwidth}

   \def\svgwidth{.5\textwidth}
    \input{vote6.pdf_tex} \\

    \vspace{-.5cm}
\end{wrapfigure}

Suppose $n$ people cast their votes in an election between two candidates.  Then, suppose an adversary found a way to change several of the votes.  By changing some votes, the adversary attempts to change the outcome of the election.  Suppose also that the voting method $f\colon\{-1,1\}^{n}\to\{-1,1\}$ is balanced in the following sense.

\begin{definition}[\embolden{Balanced Voting Method}]\label{baldef}
Let $f\colon\{-1,1\}^{n}\to\{-1,1\}$ be a voting method.  We say $f$ is \textbf{balanced} if each of the two candidates has an equal chance of winning the election.  That is, the number of combinations of votes where candidate $1$ wins is equal to the number of combinations of votes where candidate $-1$ wins.
\end{definition}

For example, dictator functions and the majority function are balanced.

\begin{question}
What balanced voting method is most resilient to adversarial changes to votes?

That is, if $k\geq1$ votes can be changed by the adversary, what is the least number of combinations of votes (of all voters) such that the adversary can change the election's outcome?
\end{question}

In a dictatorship, e.g. $f(x_{1},\ldots,x_{n})=x_{1}$, changing the first vote changes the outcome of the election, so this voting method is not at all resilient to adversarial changes.  Similarly, a voting method that is only a function of a small set of voters (sometimes called a junta) will probably not be resilient to adversarial changes to votes.  It turns out that the majority function is the balanced voting method most resilient to adversarial changes; we thank Daniel Kane for telling us the following argument.

\begin{prop}[\embolden{Adversarial Optimality of Majority}]\label{advmaj}
Let $n$ be an odd positive integer and let $k$ be an integer satisfying $1\leq k\leq n$.  After the votes have been cast, suppose an adversary can change $k$ votes in an election between two candidates with $n$ voters.  Then among all balanced voting methods, the majority function has the least number of combinations of votes where the election's outcome can be altered by the adversary.
\end{prop}

Before beginning the proof, we introduce some notation.  For any $x=(x_{1},\ldots,x_{n})\in\R^{n}$, denote the $\ell_{0}$ ``norm'' of $x$ by $\vnorm{x}_{0}\colonequals\#\{1\leq i\leq n\colon x_{i}\neq 0\}$.  (This quantity is not a norm since $\vnorm{tx}_{0}=\vnorm{x}_{0}$ for any $t\neq0$.)  Let $S\subset\{-1,1\}^{n}$.  For any integer $k\geq1$, we denote the distance $k$ neighborhood of $S$ by
\begin{equation}\label{gammadef}
\Gamma_{k}(S)\colonequals\{x\in\{-1,1\}^{n}\colon \exists\, y\in S\,\,\mathrm{such}\,\,\mathrm{that}\,\, \vnorm{x-y}_{0}\leq k\}.
\end{equation}
Then $\Gamma_{k}(S)$ is the set of possible votes that can be obtained by changing at most $k$ votes from a given $y\in S$.  For any $k\geq0$, let $B_{k}\subset\{-1,1\}^{n}$ be a distance $k$ neighborhood of one ``half'' of the hypercube:
\begin{equation}\label{bkdef}
B_{k}\colonequals\Gamma_{k}\big(\{(y_{1},\ldots,y_{n})\in\{-1,1\}^{n}\colon y_{1}+\cdots+y_{n}\geq 0\}\big).
\end{equation}

\begin{wrapfigure}{r}{0.53\textwidth}

   \def\svgwidth{.47\textwidth}
    \input{vote7.pdf_tex} \\

    \vspace{.2cm}
\end{wrapfigure}

The key geometric fact used to prove Proposition \ref{advmaj} is:

\begin{theorem}[\embolden{Harper's Inequality/ Hypercube Vertex Isoperimetric Inequality}]\label{harper}
Let $S\subset\{-1,1\}^{n}$.  Let $k\geq0$.  Assume that
$$\abs{S}\geq\abs{B_{k}}.\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$$
Then
$$\abs{\Gamma_{1}(S)}\geq\abs{\Gamma_{1}(B_{k})}.\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$$
\end{theorem}

\begin{proof}[Proof of Proposition \ref{advmaj}]
We induct on $k$.  Let $f\colon\{-1,1\}^{n}\to\{-1,1\}$ be the majority function, and let $g\colon\{-1,1\}^{n}\to\{-1,1\}$ be another balanced voting method.  Let $S\colonequals\{x\in\{-1,1\}^{n}\colon g(x)=1\}$ be the set of votes where candidate $1$ wins the election, when $g$ is the voting method used to run the election.  Note that $B_{0}=\{x\in\{-1,1\}^{n}\colon f(x)=1\}$.  Since $f$ and $g$ are balanced, $\abs{S}=\abs{B_{0}}=2^{n-1}$.  So, Harper's Inequality, Theorem \ref{harper}, implies that
\begin{equation}\label{one1}
\abs{\Gamma_{1}(S)}\geq\abs{\Gamma_{1}(B_{0})}.
\end{equation}

\begin{equation}\label{one2}
\abs{\Gamma_{1}(S)}-\abs{S}\geq\abs{\Gamma_{1}(B_{0})}-\abs{B_{0}}.
\end{equation}
The same inequality holds also when $S\colonequals\{x\in\{-1,1\}^{n}\colon g(x)=-1\}$.  Taken together, we conclude that the number of combinations of votes for which the outcome of the election can be altered with one adversarial vote change is smallest for the majority vote $f$ (since $f$ corresponds to the right side of \eqref{one2}).  The case $k=1$ therefore follows by \eqref{one2}.

We now proceed with the inductive step.  By the inductive hypothesis, if $S\colonequals\{x\in\{-1,1\}^{n}\colon g(x)=1\}$ or if $S\colonequals\{x\in\{-1,1\}^{n}\colon g(x)=-1\}$, we have
$$\abs{\Gamma_{k}(S)}-\abs{S}\geq\abs{\Gamma_{k}(B_{0})}-\abs{B_{0}}.$$
That is, $\abs{\Gamma_{k}(S)}\geq\abs{\Gamma_{k}(B_{0})}=\abs{B_{k}}$.  We need to prove the case $k+1$.  This again follows by Harper's Inequality, Theorem \ref{harper}, since
$$\abs{\Gamma_{k+1}(S)}\stackrel{\eqref{gammadef}}{=}\abs{\Gamma_{1}(\Gamma_{k}(S))}\geq\abs{\Gamma_{1}(B_{k})}\stackrel{\eqref{bkdef}}{=}\abs{B_{k+1}},$$
Therefore, when $S\colonequals\{x\in\{-1,1\}^{n}\colon g(x)=1\}$ or $S\colonequals\{x\in\{-1,1\}^{n}\colon g(x)=-1\}$,
\begin{equation}\label{one3}
\abs{\Gamma_{k+1}(S)}-\abs{S}\geq \abs{B_{k+1}}-\abs{B_{0}}.
\end{equation}
That is, the number of votes for which the outcome of the election can be altered with $k+1$ adversarial vote changes is smallest for the voting method $f$ (since the majority vote $f$ corresponds to the right side of \eqref{one3}).  The inductive step and the proof are complete.
\end{proof}

For some related observations for ranked choice voting, see e.g. \cite[Lemma 3.3]{mossel13}.

Proposition \ref{advmaj} can easily be extended to unbalanced voting methods.  To state such a result, let $t$ be a real number and define a \textbf{majority function with threshold $t$} to be a function of the form
$$\mathrm{Maj}_{n,t}(x)=\mathrm{sign}(x_{1}+x_{2}+\cdots+x_{n}-t),\qquad\forall\,x=(x_{1},\ldots,x_{n})\in\{-1,1\}^{n}.$$
Also, we say that two voting methods $f,g\colon\{-1,1\}^{n}\to\{-1,1\}$ \textbf{have the same balance} if the number of combinations of votes resulting in candidate $1$ winning are the same for each voting method, i.e.
$$\#\{(x_{1},\ldots,x_{n})\in\{-1,1\}^{n}\colon f(x)=1\}=\#\{(x_{1},\ldots,x_{n})\in\{-1,1\}^{n}\colon g(x)=1\}.$$
For example, the majority function with threshold $t=0$ and the majority function with threshold $t=1$ do not have the same balance.

\begin{prop}[\embolden{Adversarial Optimality of Majority, Unbalanced Case}]\label{advmaj2}
Let $n$ be an odd positive integer and let $k$ be an integer satisfying $1\leq k\leq n$.  After the votes have been cast, suppose an adversary can change $k$ votes in an election between two candidates with $n$ voters.  Let $f$ be a majority function with threshold $t$, where $t$ is an even integer.  Let $g$ be another voting method such that $f$ and $g$ have the same balance.  Then the number of combinations of votes where the election's outcome can be altered by the adversary is lesser for $f$ than for $g$.
\end{prop}

\subsection{More than Two Candidates}

It would be desirable to have an analogue of Proposition \ref{advmaj} for voting methods with more than two candidates.  Such a result might require a version of Harper's Inequality, Theorem \ref{harper}, for multiple sets.  It is unclear if such an inequality can be proven

\subsection{Additional Comments}

Proposition \ref{advmaj} can be strengthened slightly, so that a voting method that is ``close'' to being as resilient as majority must itself be ``close'' to majority.  Instead of applying Theorem \ref{harper}, one instead uses a stronger version, such as \cite{keevash18}.

The majority function is known to be optimal in various senses.  For example, the majority function maximizes the number of votes that agree with the outcome of the election \cite[Theorem 2.33]{odonnell14}.  Apparently Rousseau argued this was an ideal choice for a voting method in 1762 in ``Du contrat social.''  Theorem \ref{mis} below, the Majority is Stablest Theorem, also characterizes the majority function as being the most stable to random corruption in votes, among a reasonable class of voting methods.

For more background on social choice theory, see e.g. \cite[Chapter 2]{odonnell14}, \cite{odonnell14b}, \cite[Section 3]{kalai18}.

\section{Independent Random Corruption of Votes}

\begin{wrapfigure}{r}{0.5\textwidth}

   \def\svgwidth{.5\textwidth}
    \input{vote6.pdf_tex} \\

    \vspace{-1cm}
\end{wrapfigure}

In Proposition \ref{advmaj}, we showed that the majority function is the most stable voting method to adversarial corruption.  The majority function is also most stable when votes are corrupted randomly, as shown below.

\begin{theorem}[\embolden{Majority is Stablest, Informal Version}, {\cite[Theorem 4.4]{mossel10}}]\label{misinf}
Suppose we run an election with a large number $n$ of voters and two candidates.  In this election, voters are modelled to have the following random behavior:
\begin{itemize}
\item[(i)] Voters cast their votes randomly, independently, with equal probability of voting for either candidate.
\item[(ii)] Each voter has a small influence on the outcome of the election.  (That is, all influences from Definition \ref{infdef} are small.)
\end{itemize}
Then the majority function is the balanced voting method that best preserves the outcome of the election, when votes have been corrupted independently.
\end{theorem}

The definition of ``best'' here is intentionally vague.  We will define ``best'' to mean: maximizing noise stability, as defined below in Definition \ref{nsdef}.  Also, the probability of each vote being changed (corrupted) should be less than $1/2$ in Theorem \ref{misinf}.  Otherwise the majority preferences of the electorate are reversed upon corruption.

Some remarks concerning the sensibility of the assumptions of Theorem \ref{misinf} now follow.

\begin{itemize}
\item Suppose we completely ignore the votes, and just declare that the first candidate wins.  This voting method is as stable to vote corruption as one can imagine, since any amount of corruption in votes cannot change the outcome of the election.  Since this voting method is certainly undemocratic and uninteresting, some assumption in Theorem \ref{misinf} must eliminate it.  And indeed, this voting method is not balanced, so Theorem \ref{misinf} ignores it.  This voting method corresponds to a constant function $f$.
\item As we saw in Example \ref{dictex}, a dictator function has one large influence, and the remaining voters have no influence on the election's outcome.  Consequently, the dictator voting method is quite stable to independently random changes to votes, since changing the votes of the non-dictators has no effect on the election's outcome.  So, as in the previous example, the dictator function is rather stable to vote corruption for a rather uninteresting reason.  We therefore eliminate dictator functions from consideration by imposing the democratic assumption $(ii)$ that each voter has a small influence on the outcome of the election.
\end{itemize}

\subsection{Two Candidates}

In this section, we will formalize the assumptions in Theorem \ref{misinf}, resulting in the formal version of the Majority is Stablest Theorem \ref{mis}.

\begin{assumption}[\embolden{Voter Assumptions}]\label{voteas}
\hfill
\begin{itemize}
\item There are $n$ voters denoted $\{1,\ldots,n\}$.  There are two candidates denoted $-1$ and $1$.
\item For any $1\leq i\leq n$, the $i^{th}$ voter casts a single \textit{random} vote $X_{i}$ taking the value $-1$ or $1$.  (In particular, we are not dealing with ranked voting methods)
\item The votes $(X_{1},\ldots,X_{n})$ are independent, identically distributed (i.i.d.) random variables.  That is, voters are modelled as independent decision makers with the same probabilities of voting for either candidate.
\end{itemize}
The \textbf{voting method} $f$ is a function $f\colon\{-1,1\}^{n}\to\{-1,1\}$.  If the votes are $(X_{1},\ldots,X_{n})$, then the winner of the election is $f(X_{1},\ldots,X_{n})$.
\end{assumption}

\begin{remark}
One could argue that the voter assumptions are not realistic, since e.g. a small group of friends will most likely share similar views, read similar news items, etc., so that their decisions are not truly independent.  On the other hand, modeling a large number of voters to be independent individuals is somewhat plausible, from an aggregate perspective.
\end{remark}

\begin{assumption}[\embolden{Voter Corruption Assumptions}]\label{corras}
Let $0\leq\rho\leq1$.  Suppose we are given the votes $X_{1},\ldots,X_{n}$ of $n$ voters choosing between $2$ candidates.  The corrupted votes $Y_{1},\ldots,Y_{n}$ are defined as follows.
\begin{itemize}
\item The \textbf{corrupted votes} $Y_{1},\ldots,Y_{n}$ are independent, identically distributed (i.i.d.) random variables.
\item For each $1\leq i\leq n$, if $X_{i}=x_{i}\in\{-1,1\}$, then with probability $1-\rho$, $Y_{i}$ is a uniformly random element of $\{-1,1\}$, and with probability $\rho$, $Y_{i}=x_{i}$.
\end{itemize}
\end{assumption}
\begin{remark}
When $\rho=1$, $Y_{i}=X_{i}$ for all $1\leq i\leq n$, i.e. no vote corruption has occurred.  When $\rho$ is close to $1$, $Y_{1}$ is almost the same as $X_{1}$, i.e. $X_{1}$ and $Y_{1}$ are strongly correlated, and a small amount of vote corruption has occurred.

When $\rho=0$, the votes $(X_{1},\ldots,X_{n})$ and $(Y_{1},\ldots,Y_{n})$ are independent of each other, i.e. the corrupted votes $(Y_{1},\ldots,Y_{n})$ have been so scrambled that they have no dependence (or correlation) with the original votes $(X_{1},\ldots,X_{n})$.
\end{remark}

\noindent\textbf{Notation.}  We denote the original (random) votes cast in the election as $X=(X_{1},\ldots,X_{n})$, and we denote the corrupted votes as $Y=(Y_{1},\ldots,Y_{n})$.

Recall that the voting method $f$ takes the value $1$ or $-1$, according to which candidate ($1$ or $-1$) won the election.  So, if the winner of the election $f(X)$ is the same as the winner of the election with corrupted votes $f(Y)$, then
$$f(X)f(Y)=1.$$
On the other hand, if the winner of the election $f(X)$ is different than the winner of the election with corrupted votes $f(Y)$, then
$$f(X)f(Y)=-1.$$
So, the voting method that has the largest average value of
$$f(X)f(Y)$$
will be the most stable on average to random vote corruption.  This observation motivates the following definition.

\begin{definition}[\embolden{Noise Stability}]\label{nsdef}
Let $f\colon\{-1,1\}^{n}\to\{-1,1\}$ be a voting method.  The \textbf{noise stability} of $f$ with correlation parameter $0\leq\rho\leq1$ is
$$S_{\rho}(f)\colonequals \E f(X)f(Y).$$
Here $\E$ denotes expected value, or average value, with respect to the random variables $X=(X_{1},\ldots,X_{n}),Y=(Y_{1},\ldots,Y_{n})$ defined in Assumptions \ref{voteas} and \ref{corras}.
\end{definition}

\begin{remark}\label{nsprobrk}
The probability that the election's outcome stays the same after vote corruption has occurred is $\frac{1}{2}(1+S_{\rho}(f))$.
\end{remark}

\subsubsection{Unbiased Case}

Theorem \ref{misinf} can be restated as: the majority function maximizes noise stability, among a reasonable class of voting methods.

In the Theorem below, we denote the Majority function as $\mathrm{Maj}_{n}\colon\{-1,1\}^{n}\to\{-1,1\}$, so that

$$\mathrm{Maj}_{n}(x_{1},\ldots,x_{n})=\mathrm{sign}(x_{1}+\cdots+x_{n}),\qquad\mathrm{for}\,\,\mathrm{all}\,\,(x_{1},\ldots,x_{n})\in\{-1,1\}^{n}.$$

\pagebreak

\begin{wrapfigure}{r}{0.5\textwidth}
\vspace{-1cm}
\centering
    \,\,\includegraphics[width=.45\textwidth]{singlebubble.pdf} \\

    \caption[blah]{The proof of Theorem \ref{mis} is related to the fact that soap bubbles take a spherical shape.  A soap bubble\footnotemark\, encloses a fixed volume of air, and it minimizes its surface area. The majority function has an analogous optimality property.  We will discuss this connection more in Section \ref{otherapp}.}

      \vspace{-1cm}
\end{wrapfigure}

For simplicity, we first state the balanced case of the Theorem.  That is, we make the assumption that the random votes $X_{1},\ldots,X_{n}$ are each uniformly distributed in $\{-1,1\}$.  So, e.g. $X_{1}=1$ with $1/2$ probability, and $X_{1}=-1$ with $1/2$ probability.

\begin{theorem}[\embolden{Majority is Stablest, Formal Version}, {\cite[Conjecture 1.1]{mossel10}}]\label{mis}
Let $0\leq\rho\leq1$ and let $\epsilon>0$.  Then there exists $\tau>0$ such that, if $f\colon\{-1,1\}^{n}\to\{-1,1\}$ satisfies $\E f(X)=0$ and $\mathrm{Inf}_{i}(f)\leq\tau$ for all $1\leq i\leq n$, then
$$S_{\rho}(f)\leq\lim_{n\to\infty} S_{\rho}(\mathrm{Maj}_{n})+\epsilon=\frac{2}{\pi}\sin^{-1}(\rho)+\epsilon.\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad$$
\end{theorem}

The assumption $\E f(X)$ says that $f$ is balanced according to Definition \ref{baldef}, and the assumption $\max_{1\leq i\leq n}\mathrm{Inf}_{i}(f)\leq\tau$ corresponds to part (ii) of Theorem \ref{misinf}.

\footnotetext{Picture taken from https://commons.wikimedia.org/wiki/File:Reflection\underline{ }in\underline{ }a\underline{ }soap\underline{ }bubble\underline{ }edit.jpg}

\subsubsection{Biased Case}

The assumption in Theorem \ref{mis} that the votes are uniformly distributed in $\{-1,1\}$ can be relaxed, as we now describe.  Let $0<p<1$.  Let $X_{1},\ldots,X_{n}$ be independent identically distributed random variables where $\P(X_{i}=1)=1-\P(X_{i}=-1)=p$ for all $1\leq i\leq n$.

\begin{theorem}[\embolden{Majority is Stablest, Formal, Biased Case}, {\cite[Theorem 4.4]{mossel10}}]\label{misg}
Let $0\leq\rho\leq1$.  Let $-1\leq\mu\leq 1$.  Let $t=t_{n}\in\R$ such that $\abs{\E \mathrm{Maj}_{n,t}(X)-\mu}=\min_{t'\in\R}\abs{\E\mathrm{Maj}_{n,t'}-\mu}$.  Let $\tau>0$ and let $f\colon\{-1,1\}^{n}\to\{-1,1\}$ satisfy $\E f(X)=\mu$ and $\mathrm{Inf}_{i}(f)\leq\tau$ for all $1\leq i\leq n$, then
$$S_{\rho}(f)\leq\lim_{n\to\infty} S_{\rho}(\mathrm{Maj}_{n,t_{n}})+O_{p,1-\rho}\Big(\frac{\log\log(1/\tau)}{\log(1/\tau)}\Big).$$
\end{theorem}

For an even more general version of Theorem \ref{misg}, see \cite[Theorem 4.4]{mossel10}

\subsection{More than Two Candidates}

In this section, we consider elections between $k\geq3$ candidates, where each of $n$ voters casts a single vote for a single candidate.

Theorem \ref{misg} (and its generalizations such as \cite[Theorem 4.4]{mossel10}) essentially completely characterize majority functions as the most stable to independently random corruption of votes, \textit{when the election has only two candidates}.  Unfortunately, analogous statements for three or more candidates seem harder to prove.  With more than two candidates, a suitable replacement for the majority is the plurality function.  In a plurality election, the candidate with the most votes wins the election.

\begin{wrapfigure}{r}{0.52\textwidth}

\vspace{-.5cm}

\centering
    \includegraphics[width=.26\textwidth]{doublebubblecartoon.pdf} \\

    \caption{Generalizing Theorem \ref{misg} to elections with three candidates is related to: proving that two joint soap bubbles take the pictured ``double-bubble'' shape.  Two soap bubbles enclose two separate and fixed volumes of air, and they minimize their total surface area \cite{hutchings02}. The plurality function should have an analogous optimality property.  We will discuss this connection more in Section \ref{otherapp}.}
    \label{doublepic}

    \includegraphics[width=.3\textwidth]{tribubblecartoon.pdf} \\

    \caption{Three soap bubbles that have collided take the shape shown here.}\label{tripic}
        \vspace{-2.2cm}
\end{wrapfigure}

It was conjectured \cite{khot07,isaksson11} that the plurality function is the balanced voting method that is most stable to independent, random vote corruption

\begin{conj}[\embolden{Plurality is Stablest, Informal Version}, {\cite{khot07}, \cite[Conjecture 1.9]{isaksson11}}]\label{pisinf}
Suppose we run an election with a large number $n$ of voters and $k\geq3$ candidates.  In this election, voters are modelled to have the following random behavior:
\begin{itemize}
\item Voters cast their votes randomly,\\ independently, with equal probability of voting for each candidate.
\item Each voter has a small influence on\\ the outcome of the election.
\end{itemize}
Then the plurality function is the balanced\\ voting method that best preserves the out-\\ come of the election, when votes\\ have been corrupted independently.
\end{conj}

In the case that the probability of vote corruption is small ($\rho$ is close to $1$), we proved the first known case of Conjecture \ref{pisinf} in \cite{heilman18b}, culminating a series of previous works. Conjecture \ref{pisinf} for all parameters $0<\rho<1$ is still open.  Unlike the case of the Majority is Stablest (Theorem \ref{misg}), Conjecture \ref{pisinf} \textit{cannot hold} when the candidates have unequal chances of winning the election \cite{heilman14}.  This realization is an obstruction to proving Conjecture \ref{pisinf}.  It suggested that proof methods for Theorem \ref{misg} cannot apply to Conjecture \ref{pisinf}.  Indeed, calculus of variations methods have emerged as a promising avenue for proving Conjecture \ref{pisinf}, when the candidates have equal chances of winning the election.

 \subsection{Additional Comments}

Discrete Fourier analysis often plays a prominent role in noise stability and voting.  The surveys \cite{odonnell14b,khot10b} and book \cite{odonnell14} describe the interconnectedness of these topics.

\pagebreak

\begin{wrapfigure}{r}{0.5\textwidth}

\centering
    \includegraphics[width=.3\textwidth]{triplebubblepic.pdf} \\

    \caption[blah]{Three soap bubbles that have collided take the shape shown here\footnotemark.}
    \vspace{-1cm}
\end{wrapfigure}

We have not focussed much on ranked choice voting methods.  For more on this topic, see e.g. \cite{mossel13} or the comprehensive works \cite{arrow02,brandt16}.

\begin{question}\label{rankedq}
Is it possible to state a sensible version of the Plurality is Stablest Conjecture \ref{pisinf} for ranked choice voting methods?
\end{question}

\begin{wrapfigure}{r}{0.5\textwidth}
\vspace{-.5cm}

\centering
    \includegraphics[width=.25\textwidth]{propeller.pdf} \\

    \caption{The partition of Euclidean space with three regions of fixed Gaussian volume and minimal total Gaussian surface area takes this shape \cite{milman18b,heilman18b}.}
     \vspace{-1.3cm}
\end{wrapfigure}

In ranked choice voting, each voter provides a ranked list of the candidates.  Suppose a voting method is then a function only of the pairwise comparisons of each candidate, as in Table \ref{table2}.  Suppose then that each of these pairwise comparisons is independently corrupted.  Then one possible answer to Question \ref{rankedq} says that the Plurality of the pairwise comparisons is most stable to this kind of vote corruption.  Taking the Plurality of pairwise comparisons is known as the Second Order Copeland voting method.  So, one could argue that this method is most stable to vote corruption.  However, under other models of vote corruption, it is not clear what the ``best'' ranked choice voting method should be.

\footnotetext{Picture taken from https://www.flickr.com/photos/sm/2603411754/sizes/o/}

\section{Brief Discussion of US Electoral College}

The US Electoral College system is similar but not identical to the two-tier majority function described in Example \ref{itmajex} with $m=51$ equal-sized ``states.''  Suppose we run an election between two candidates, where $g$ is a two-tier majority function with $m=51$, and $f$ is the usual majority function with $n$ a large odd number of voters.  We already know from Theorem \ref{misg} that the majority function is more stable to vote corruption that the electoral college system.  But how much more stable is it?

We consider the noise stability $S_{\rho}$ of each of these voting methods where $\rho=1-2\epsilon$ and $\epsilon>0$ is small with $51<1/\epsilon<n$.  That is, the probability of each vote being corrupted is small.  Then \cite[p. 9]{odonnell08}
$$S_{1-2\epsilon}(f)\approx 1-\frac{4}{\pi}\sqrt{\epsilon},\qquad S_{1-2\epsilon}(g)\approx 1-2(\frac{2}{\pi})^{3/2}\sqrt{51}\sqrt{\epsilon}.$$
So, by Remark \ref{nsprobrk}, the probability that vote corruption changes the election's outcome is about 5.7 times greater for the electoral college, than for majority.  Here we used
$$\frac{2(2/\pi)^{3/2}\sqrt{51}}{4/\pi}\approx 5.698035\ldots$$

Computer simulation similarly shows that, when the size of each ``state'' defining the two-tier majority function agrees with their size from the 2010 census, then the probability that vote corruption changes the election's outcome is more than 4 times greater for the electoral college, than for majority.

Strictly speaking, the US Electoral College system is not a two-tier majority function.  Each state (except for Maine and Nebraska) runs its own plurality vote, so that the candidate winning the most votes in that state wins that particular state.  Then each state's winner is entered into a nationwide weighted majority vote.  If no candidate wins this weighted majority vote, then the House of Representatives chooses the president, with one vote for each of the 50 states.  In an election between two candidates, a perfect tie in the electoral college is unlikely, i.e. it is unlikely for the House of Representatives to choose the president.  Moreover, since Maine and Nebraska are small states, their chance of changing the outcome in the electoral college is small.  So, the probability that vote corruption changes the U.S. presidential election's outcome is still more than 4 times greater for the electoral college, than for majority.

The integer weight of each state in the nationwide majority vote is equal to the number of national congressional representatives in each state (with a weight of three given to Washington D.C.)  Consequently, each state has a minimum weight of $3$ in the nationwide majority vote (i.e. the electoral college vote).  The apportionment of members to the House of Representatives is a nontrivial task, since the ratios of state populations should somehow closely match the ratios of their numbers of electoral votes.  Apportionment methods were hotly debated over the nation's history; for more on this history see e.g. \cite{balinski75}.

As noted by Banzhaf in 1968, the probability of one single voter changing the election's outcome, if all other voters cast their votes randomly, tends to be higher for voters in larger states.  However, the assumption that all other voters cast their votes uniformly at random is unrealistic.  Despite our similarly unrealistic assumptions of voter behavior, i.e. Assumption \ref{voteas}, actual data for presidential elections in the U.S. (in Table \ref{table5}) demonstrates that it is much more likely for a small number of vote changes to change the electoral college's outcome than a plurality vote.

\begin{table}[htbp!]\label{table5}
\small
\centering
\begin{tabular}{crrlcc|}
  &  \multicolumn{5}{c}{U.S. Presidential Election Vote Margins}\\
 \cline{2-6}
  Elec-& \multicolumn{1}{|c}{Popular Vote } & Vote Changes  &Percent & Electoral  & State where votes would \\
   tion& \multicolumn{1}{|c}{Margin, } & Sufficient to  & of Popular &Vote & be changed (corresponding\\
   Year& \multicolumn{1}{|c}{Rounded} & Sway Election & Vote &Margin & electoral votes) \\
 \cline{1-6}
  \multicolumn{1}{|c|}{1844} & 40,000 &2,554 & .09\% &65 & New York (36)\\
 \multicolumn{1}{|c|}{1848} & 140,000 & 6,669 & .23\% &36 & Pennsylvania (26)\\
\multicolumn{1}{|c|}{1856} & 500,000  & 11,155 &.28\% & 60 & Illinois, Tennessee, Kentucky (35) \\

 \multicolumn{1}{|c|}{\textcolor{red}{1876}} & \textcolor{red}{-250,000}  & 445 & .005\%  & 1 & South Carolina (7)\\
 \multicolumn{1}{|c|}{\textcolor{blue}{1880}} & \textcolor{blue}{2,000}$^{*}$  & 8,416 & .09\% & 59 & OR, CT, CO, NH, IN (32)\\
 \multicolumn{1}{|c|}{1884} & 60,000 & 575  & .006\% & 37 & New York (36)\\
 \multicolumn{1}{|c|}{\textcolor{red}{1888}} & \textcolor{red}{-90,000}   & 7,187 & .06\% & 65 & NY (36)\\
 \multicolumn{1}{|c|}{1892} & 400,000   & 25,362 & .21\%  & 132 & CA, IN, ND, KA, WI, WV, IL (68)\\
 \multicolumn{1}{|c|}{1896} & 600,000   & 18,602 & .13\%  & 95 & KY, CA, OR, IN,  WV, DE (50)\\
 \multicolumn{1}{|c|}{1916} & 600,000   & 1,887  &  .01\% & 23 & California (13)\\
 \multicolumn{1}{|c|}{1948} & 2,200,000  & 29,294 & .06\% & 114 & OH, CA, IL (78)\\
 \multicolumn{1}{|c|}{1960} & 110,000   & 14,265  & .02\% & 84 & HI, IL, MO, SC (59)\\
 \multicolumn{1}{|c|}{1968} & 500,000   & 41,971 & .06\% & 110 & Missouri, New Jersey, Alaska (32)$^{**}$\\
 \multicolumn{1}{|c|}{1976} & 1,700,000  & 12,791 & .02\%  & 57 & Ohio and Mississippi (32)\\
 \multicolumn{1}{|c|}{\textcolor{red}{2000}} & \textcolor{red}{-500,000}   & 269 & .0003\% & 5 & Florida (25)\\
 \multicolumn{1}{|c|}{2004} & 3,000,000  & 59,301 & .05\% & 35 & Ohio (20)\\
 \multicolumn{1}{|c|}{2008} & 10,000,000  & 495,310 & .38\% & 192 & NC, IN, FL, OH, VA, IA, NH (97)\\
 \multicolumn{1}{|c|}{2012} & 5,000,000  & 214,764 & .17\% & 126 & FL, OH, VA, NH (64)\\
 \multicolumn{1}{|c|}{\textcolor{red}{2016}} & \textcolor{red}{-3,000,000}  & 38,875 & .03\%  & 77 & MI, PA, WI (46)\\
\cline{1-6}
\end{tabular}
\caption{\tiny In 17 of the country's 58 elections between 1788 and 2016, the popular vote was so narrow that changing a relatively small number of votes in just a few states would have shifted the result of the national election. In some years, \textcolor{red}{the person elected president lost the popular vote}. In one year, 1880, \textcolor{blue}{the Electoral College vote was just about as close as the popular vote}.  $^{*}$Historians disagree about the popular vote margin in the 1880 election.
$^{**}$In 1968, the House of Representatives was controlled by a different party than won the presidential election, so changing the election's outcome would have only required the winner to fail to receive a majority in the Electoral College.}
\vspace{-1cm}

\end{table}

\section{Other Applications}\label{otherapp}

As mentioned above, Majority is Stablest and Plurality is Stablest are closely related to geometric optimization problems involving soap bubbles.  For a general introduction to minimal surfaces, see the surveys \cite{colding19,colding11} or the book by the same authors.  For more discussion on the connections between voting and geometry, see the surveys \cite{odonnell14b,khot10b}.

 In 2002, it was proven that the two regions of fixed volume that minimize their total surface area are those pictured in Figure \ref{doublepic} \cite{hutchings02}.  The analogous result for three regions, as in Figure \ref{tripic}, is still open.  This problem is only solved in the plane by Wichiramala.  Surprisingly, the Gaussian versions of these problem were recently resolved in \cite{milman18b}, and then strengthened in \cite{heilman18b}.

 The initial motivation for the Majority is Stablest Theorem \ref{misg} and the Plurality is Stablest Conjecture \ref{pisinf} came from theoretical computer science.  These inequalities imply sharp computational hardness for MAX-CUT and its generalizations.  That is, we can efficiently, approximately solve some computational problem, and improving on this approximation is impossible to do efficiently, assuming the Unique Games Conjecture, a standard complexity theoretic assumption.  For more on the relation between voting and computer science applications, see \cite{khot10b,khot07,isaksson11}.

The noise stability of functions, as used in the Majority is Stablest Theorem \ref{misg}, has developed into a subject of its own.  Various references exist on the subject, such as \cite{diakon10}.

Besides the applications of voting mentioned above, voting is also used as a subroutine in various machine learning algorithms, such as ``boosting'' algorithms of Freund and Schapire.  In a ``boosting'' algorithm, one has access to several ``weak'' learning algorithms (or ``weak'' experts) who can each correctly classify e.g. an email as spam or not spam, with 51\% probability.  (The experts are called ``weak'' since it is easy to correctly classify an email as spam or not spam with 50\% probability, just by randomly choosing either spam or not spam, with equal probability.)  Using an appropriately chosen weighted majority vote among all of the classifications of these experts, their aggregate classification of the email can be correct with close to 100\% probability.  So-called ``boosting'' algorithms combine ``weak'' expert opinions to ``boost'' the probability of correct classification in this way.

\medskip
\noindent\textbf{Acknowledgement}.  Thanks to Daniel Kane and Elchanan Mossel for helpful discussions.

\bibliographystyle{amsalpha}
\bibliography{12162011}

\end{document}