expect_apply_eq_ite — Mathlib

English

For a finite α and any a ∈ α, the average value (expectation) of ψ(a) over all additive characters ψ: α → ℂ is 1 if a = 0 and 0 otherwise.

Русский

Для конечной группы α и любого элемента a ∈ α среднее значение ψ(a) по всем аддитивным характером ψ: α → ℂ равно 1, если a = 0, и 0 в противном случае.

LaTeX

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

Lean4

theorem expect_apply_eq_ite [Finite α] [DecidableEq α] (a : α) : 𝔼 ψ : AddChar α ℂ, ψ a = if a = 0 then 1 else 0 := by
  simpa using expect_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

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