Commuting Probability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file introduces the commuting probability of finite groups.

Main definitions #

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

Todo #

Neumann's theorem.

source

noncomputable def comm_prob (M : Type u_1) [has_mul M] :

ℚ

The commuting probability of a finite type with a multiplication operation

Equations

comm_prob M = ↑(nat.card {p // p.fst * p.snd = p.snd * p.fst}) / ↑(nat.card M) ^ 2

source

theorem comm_prob_def (M : Type u_1) [has_mul M] :

comm_prob M = ↑(nat.card {p // p.fst * p.snd = p.snd * p.fst}) / ↑(nat.card M) ^ 2

source

theorem comm_prob_pos (M : Type u_1) [has_mul M] [finite M] [h : nonempty M] :

0 < comm_prob M

source

theorem comm_prob_le_one (M : Type u_1) [has_mul M] [finite M] :

comm_prob M ≤ 1

source

theorem comm_prob_eq_one_iff {M : Type u_1} [has_mul M] [finite M] [h : nonempty M] :

comm_prob M = 1 ↔ commutative has_mul.mul

source

theorem card_comm_eq_card_conj_classes_mul_card (G : Type u_2) [group G] [finite G] :

nat.card {p // p.fst * p.snd = p.snd * p.fst} = nat.card (conj_classes G) * nat.card G

source

theorem comm_prob_def' (G : Type u_2) [group G] [finite G] :

comm_prob G = ↑(nat.card (conj_classes G)) / ↑(nat.card G)

source

theorem subgroup.comm_prob_subgroup_le {G : Type u_2} [group G] [finite G] (H : subgroup G) :

comm_prob ↥H ≤ comm_prob G * ↑(H.index) ^ 2

source

theorem subgroup.comm_prob_quotient_le {G : Type u_2} [group G] [finite G] (H : subgroup G) [H.normal] :

comm_prob (G ⧸ H) ≤ comm_prob G * ↑(nat.card ↥H)

source

theorem inv_card_commutator_le_comm_prob (G : Type u_2) [group G] [finite G] :

(↑(nat.card ↥(commutator G)))⁻¹ ≤ comm_prob G