expect_neg_index — Mathlib

English

Let S be a finite set and f : S → M. Then the average over the negated indices -S equals the average of f over S with negated arguments: E_{i∈-S} f(i) = E_{i∈S} f(-i).

Русский

Пусть S — конечное множество, f:S→M. Тогда среднее по отрицательным индексам -S равно среднему по S от f(-i).

LaTeX

$$$\dfrac{1}{|S|}\sum_{i\in -S} f(i) = \dfrac{1}{|S|}\sum_{i\in S} f(-i).$$$

Lean4

@[simp]
theorem expect_neg_index [DecidableEq ι] [InvolutiveNeg ι] (s : Finset ι) (f : ι → M) :
    𝔼 i ∈ -s, f i = 𝔼 i ∈ s, f (-i) :=
  expect_image neg_injective.injOn

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