Commuting Probability

This file introduces the commuting probability of finite groups.

Main definitions

• commProb: The commuting probability of a finite type with a multiplication operation.

Todo

• Neumann's theorem.

def commProb (M : Type u_1) [Mul M] : ℚ

The commuting probability of a finite type with a multiplication operation.

Equations

• commProb M = ↑(Nat.card { p : M × M // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2

theorem commProb_def (M : Type u_1) [Mul M] : commProb M = ↑(Nat.card { p : M × M // Commute p.1 p.2 }) / ↑(Nat.card M) ^ 2

theorem commProb_prod (M : Type u_1) [Mul M] (M' : Type u_2) [Mul M'] : commProb (M × M') = commProb M * commProb M'

theorem commProb_pi {α : Type u_3} (i : α → Type u_2) [Fintype α] [(a : α) → Mul (i a)] : commProb ((a : α) → i a) = Finset.prod Finset.univ fun (a : α) => commProb (i a)

theorem commProb_function {α : Type u_2} {β : Type u_3} [Fintype α] [Mul β] : commProb (α → β) = commProb β ^ Fintype.card α

@[simp]

theorem commProb_eq_zero_of_infinite (M : Type u_1) [Mul M] [Infinite M] : commProb M = 0

theorem commProb_pos (M : Type u_1) [Mul M] [Finite M] [h : Nonempty M] : 0 < commProb M

theorem commProb_le_one (M : Type u_1) [Mul M] [Finite M] : commProb M ≤ 1

theorem commProb_eq_one_iff {M : Type u_1} [Mul M] [Finite M] [h : Nonempty M] : commProb M = 1 ↔ Commutative fun (x x_1 : M) => x * x_1

theorem commProb_def' (G : Type u_2) [Group G] : commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)

theorem Subgroup.commProb_subgroup_le {G : Type u_2} [Group G] [Finite G] (H : Subgroup G) : commProb ↥H ≤ commProb G * ↑(Subgroup.index H) ^ 2

theorem Subgroup.commProb_quotient_le {G : Type u_2} [Group G] [Finite G] (H : Subgroup G) [Subgroup.Normal H] : commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)

theorem inv_card_commutator_le_commProb (G : Type u_2) [Group G] [Finite G] : (↑(Nat.card ↥(commutator G)))⁻¹ ≤ commProb G

theorem DihedralGroup.commProb_odd {n : ℕ} (hn : Odd n) : commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)

def DihedralGroup.reciprocalFactors (n : ℕ) : List ℕ

A list of Dihedral groups whose product will have commuting probability 1 / n.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem DihedralGroup.reciprocalFactors_zero : DihedralGroup.reciprocalFactors 0 = [0]

@[simp]

theorem DihedralGroup.reciprocalFactors_one : DihedralGroup.reciprocalFactors 1 = []

theorem DihedralGroup.reciprocalFactors_even {n : ℕ} (h0 : n ≠ 0) (h2 : Even n) : DihedralGroup.reciprocalFactors n = 3 :: DihedralGroup.reciprocalFactors (n / 2)

theorem DihedralGroup.reciprocalFactors_odd {n : ℕ} (h1 : n ≠ 1) (h2 : Odd n) : DihedralGroup.reciprocalFactors n = n % 4 * n :: DihedralGroup.reciprocalFactors (n / 4 + 1)

@[inline, reducible]

abbrev DihedralGroup.Product (l : List ℕ) : Type

A finite product of Dihedral groups.

Equations

• DihedralGroup.Product l = ((i : Fin (List.length l)) → DihedralGroup l[i])

theorem DihedralGroup.commProb_nil : commProb (DihedralGroup.Product []) = 1

theorem DihedralGroup.commProb_cons (n : ℕ) (l : List ℕ) : commProb (DihedralGroup.Product (n :: l)) = commProb (DihedralGroup n) * commProb (DihedralGroup.Product l)

theorem DihedralGroup.commProb_reciprocal (n : ℕ) : commProb (DihedralGroup.Product (DihedralGroup.reciprocalFactors n)) = 1 / ↑n

Construction of a group with commuting probability 1 / n.