expect_eq_ite — Mathlib

English

For a finite group G and an additive character ψ, the average 𝔼 a, ψ a equals 1 if ψ is trivial and 0 otherwise.

Русский

Среднее 𝔼 a, ψ a равно 1, если ψ тривиальна, и иным образом 0.

LaTeX

$$$\\mathbb{E}_{a \\in G}[\\psi(a)] = \\begin{cases} 1, & \\psi = 0, \\\\ 0, & \\psi \\neq 0. \\end{cases}$$$

Lean4

theorem expect_eq_ite (ψ : AddChar G R) : 𝔼 a, ψ a = if ψ = 0 then 1 else 0 := by
  simp [Fintype.expect_eq_sum_div_card, sum_eq_ite, ite_div]

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