English
For any subgroup H ≤ G, the commuting probability satisfies commProb(H) ≤ commProb(G) · (H.index)^2.
Русский
Для подгруппы H ≤ G выполняется commProb(H) ≤ commProb(G) · (индекс H)^2.
LaTeX
$$commProb(H) \le commProb(G) \cdot (H:\,G)^2$$
Lean4
theorem commProb_subgroup_le : commProb H ≤ commProb G * (H.index : ℚ) ^ 2 := by
/- After rewriting with `commProb_def`, we reduce to showing that `G` has at least as many
commuting pairs as `H`. -/
rw [commProb_def, commProb_def, div_le_iff₀, mul_assoc, ← mul_pow, ← Nat.cast_mul, mul_comm H.index, H.card_mul_index,
div_mul_cancel₀, Nat.cast_le]
· refine Nat.card_le_card_of_injective (fun p ↦ ⟨⟨p.1.1, p.1.2⟩, Subtype.ext_iff.mp p.2⟩) ?_
exact fun p q h ↦ by simpa only [Subtype.ext_iff, Prod.ext_iff] using h
· exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr Finite.card_pos.ne')
· exact pow_pos (Nat.cast_pos.mpr Finite.card_pos) 2
