commProb_reciprocal — Mathlib

English

For any natural number n, the commuting probability of the product of DihedralGroup factors given by reciprocalFactors(n) equals 1/n.

Русский

Для любого натурального числа n, вероятность коммутирования произведения групп DihedralGroup, заданного списком reciprocalFactors(n), равна 1/n.

LaTeX

$$$ \operatorname{commProb}( \operatorname{Product}( \operatorname{reciprocalFactors}(n) )) = \frac{1}{n}. $$$

Lean4

/-- Construction of a group with commuting probability `1 / n`. -/
theorem commProb_reciprocal (n : ℕ) : commProb (Product (reciprocalFactors n)) = 1 / n :=
  by
  by_cases h0 : n = 0
  · rw [h0, reciprocalFactors_zero, commProb_cons, commProb_nil, mul_one, Nat.cast_zero, div_zero]
    apply commProb_eq_zero_of_infinite
  by_cases h1 : n = 1
  · rw [h1, reciprocalFactors_one, commProb_nil, Nat.cast_one, div_one]
  rcases Nat.even_or_odd n with h2 | h2
  · have := div_two_lt h0
    rw [reciprocalFactors_even h0 h2, commProb_cons, commProb_reciprocal (n / 2), commProb_odd (by decide)]
    simp [field, h2.two_dvd]
    norm_num
  · have := div_four_lt h0 h1
    rw [reciprocalFactors_odd h1 h2, commProb_cons, commProb_reciprocal (n / 4 + 1)]
    have key : n % 4 = 1 ∨ n % 4 = 3 := Nat.odd_mod_four_iff.mp (Nat.odd_iff.mp h2)
    have hn : Odd (n % 4) := by rcases key with h | h <;> rw [h] <;> decide
    rw [commProb_odd (hn.mul h2), div_mul_div_comm, mul_one, div_eq_div_iff, one_mul] <;> norm_cast
    · have h0 : (n % 4) ^ 2 + 3 = n % 4 * 4 := by rcases key with h | h <;> rw [h] <;> norm_num
      have h1 := (Nat.div_add_mod n 4).symm
      zify at h0 h1 ⊢
      linear_combination (h0 + h1 * (n % 4)) * n
    · have := hn.pos.ne'
      positivity

Похожие утверждения