Documentation

Mathlib.GroupTheory.CommutingProbability

Commuting Probability #

This file introduces the commuting probability of finite groups.

Main definitions #

TODO #

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

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

Equations
Instances For
    source
    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
    source
    theorem commProb_prod (M : Type u_1) [Mul M] (M' : Type u_2) [Mul M'] :
    commProb (M × M') = commProb M * commProb M'
    source
    theorem commProb_pi {α : Type u_2} (i : α → Type u_3) [Fintype α] [(a : α) → Mul (i a)] :
    commProb ((a : α) → i a) = ∏ a : α, commProb (i a)
    source
    theorem commProb_function {α : Type u_2} {β : Type u_3} [Fintype α] [Mul β] :
    commProb (α → β) = commProb β ^ Fintype.card α
    source
    @[simp]
    theorem commProb_eq_zero_of_infinite (M : Type u_1) [Mul M] [Infinite M] :
    commProb M = 0
    source
    theorem commProb_pos (M : Type u_1) [Mul M] [Finite M] [h : Nonempty M] :
    0 < commProb M
    source
    theorem commProb_le_one (M : Type u_1) [Mul M] [Finite M] :
    commProb M ≤ 1
    source
    theorem commProb_eq_one_iff {M : Type u_1} [Mul M] [Finite M] [h : Nonempty M] :
    commProb M = 1 ↔ IsMulCommutative M
    source
    theorem commProb_def' (G : Type u_2) [Group G] :
    commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
    source
    theorem Subgroup.commProb_subgroup_le {G : Type u_2} [Group G] [Finite G] (H : Subgroup G) :
    commProb ↥H ≤ commProb G * ↑H.index ^ 2
    source
    theorem Subgroup.commProb_quotient_le {G : Type u_2} [Group G] [Finite G] (H : Subgroup G) [H.Normal] :
    commProb (G ⧸ H) ≤ commProb G * ↑(Nat.card ↥H)
    source
    theorem inv_card_commutator_le_commProb (G : Type u_2) [Group G] [Finite G] :
    (↑(Nat.card ↥(commutator G)))⁻¹ ≤ commProb G
    source
    theorem DihedralGroup.commProb_odd {n : ℕ} (hn : Odd n) :
    commProb (DihedralGroup n) = (↑n + 3) / (4 * ↑n)
    source
    @[irreducible]
    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.
    Instances For
      source
      @[simp]
      theorem DihedralGroup.reciprocalFactors_zero :
      reciprocalFactors 0 = [0]
      source
      @[simp]
      theorem DihedralGroup.reciprocalFactors_one :
      reciprocalFactors 1 = []
      source
      theorem DihedralGroup.reciprocalFactors_even {n : ℕ} (h0 : n ≠ 0) (h2 : Even n) :
      reciprocalFactors n = 3 :: reciprocalFactors (n / 2)
      source
      theorem DihedralGroup.reciprocalFactors_odd {n : ℕ} (h1 : n ≠ 1) (h2 : Odd n) :
      reciprocalFactors n = n % 4 * n :: reciprocalFactors (n / 4 + 1)
      source
      @[reducible, inline]
      abbrev DihedralGroup.Product (l : List ℕ) :
      Type

      A finite product of Dihedral groups.

      Equations
      Instances For
        source
        theorem DihedralGroup.commProb_nil :
        commProb (Product []) = 1
        source
        theorem DihedralGroup.commProb_cons (n : ℕ) (l : List ℕ) :
        commProb (Product (n :: l)) = commProb (DihedralGroup n) * commProb (Product l)
        source
        theorem DihedralGroup.commProb_reciprocal (n : ℕ) :
        commProb (Product (reciprocalFactors n)) = 1 / ↑n

        Construction of a group with commuting probability 1 / n.