arith_mean_weighted_of_constant — Mathlib

English

If the weights sum to 1 and z_i are allowed to vary with the weight, then the weighted arithmetic mean equals a target value x when each z_i with nonzero weight equals x.

Русский

Если веса суммируются к 1 и z_i равны x на поддержке весов, то взвешенная арифметическая средняя равна x.

LaTeX

$$$\\sum_{i\\in s} w_i z_i = x$ under the stated condition$$

Lean4

theorem arith_mean_weighted_of_constant (w z : ι → ℝ) (x : ℝ) (hw' : ∑ i ∈ s, w i = 1)
    (hx : ∀ i ∈ s, w i ≠ 0 → z i = x) : ∑ i ∈ s, w i * z i = x :=
  calc
    ∑ i ∈ s, w i * z i = ∑ i ∈ s, w i * x :=
      by
      refine sum_congr rfl fun i hi => ?_
      rcases eq_or_ne (w i) 0 with hwi | hwi
      · rw [hwi, zero_mul, zero_mul]
      · rw [hx i hi hwi]
    _ = x := by rw [← sum_mul, hw', one_mul]

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