centerMass_ite_eq — Mathlib

English

If i belongs to t, then the center of mass of the indicator weights (1 at i and 0 elsewhere) picks out the i-th element: t.centerMass of the indicator weights equals z_i.

Русский

Если i принадлежит t, то центр массы для весов, равных 1 в позиции i и 0 в остальных, даёт z_i.

LaTeX

$$t.centerMass\, (i \mapsto \mathbf{1}_{i})\, z = z_i$$

Lean4

theorem centerMass_ite_eq [DecidableEq ι] (hi : i ∈ t) : t.centerMass (fun j => if i = j then (1 : R) else 0) z = z i :=
  by
  rw [Finset.centerMass_eq_of_sum_1]
  · trans ∑ j ∈ t, if i = j then z i else 0
    · congr with i
      split_ifs with h
      exacts [h ▸ one_smul _ _, zero_smul _ _]
    · rw [sum_ite_eq, if_pos hi]
  · rw [sum_ite_eq, if_pos hi]

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