commProb_pi
theorem commProb_pi :
∀ {α : Type u_2} (i : α → Type u_3) [inst : Fintype α] [inst_1 : (a : α) → Mul (i a)],
commProb ((a : α) → i a) = Finset.univ.prod fun a => commProb (i a)
This theorem, `commProb_pi`, states that for every type `α` and a function `i` from `α` to some other type, given that `α` is a finite type and for each element `a` in `α` there exists a multiplication operation on `i a`, the commuting probability of the function type from `α` to `i a` is equal to the product of the commuting probabilities over each `i a` for all `a` in the universal set of `α`. In simpler terms, the theorem relates the commuting probability of a function type to the product of the commuting probabilities of its range types. The commuting probability here refers to the ratio of the number of pairs of elements that commute under multiplication to the square of the total number of elements.
More concisely: Given a finite type `α` and a function `i : α → C` to a commutative monoid `C`, the commuting probability of the function type `α → C` is equal to the product of the commuting probabilities of the ranges `i a` for all `a` in `α`.
|
DihedralGroup.commProb_reciprocal
theorem DihedralGroup.commProb_reciprocal :
∀ (n : ℕ), commProb (DihedralGroup.Product (DihedralGroup.reciprocalFactors n)) = 1 / ↑n
This theorem is a construction of a group with a specific commuting property. It states that for every natural number `n`, the commuting probability of the product of a list of Dihedral groups (each group determined by a natural number in the list) is `1 / n`. The list of Dihedral groups is generated by the `reciprocalFactors` function in relation to the natural number `n`. Thus, essentially, this theorem provides a way to construct a group such that the chance that two elements drawn from the group commute is exactly `1 / n`.
More concisely: For every natural number `n`, there exists a group generated by the Dihedral groups determined by the reciprocal factors of `n`, where the probability of any two elements commuting is `1/n`.
|