sum_div_card_sq_le_sum_sq_div_card

English

For a finite set s and nonnegative f, the mean of squares dominates the square of the mean: ( (∑ f(i))/|s| )^2 ≤ (∑ f(i)^2)/|s|.

Русский

Для конечного множества s и неотрицательных f имеет место: (среднее по квадратам) ≥ (среднее)^2, то есть ( (∑ f(i))/|s| )^2 ≤ (∑ f(i)^2)/|s|.

LaTeX

$$$\left(\frac{\sum_{i \in s} f(i)}{|s|}\right)^2 \le \frac{\sum_{i \in s} f(i)^2}{|s|}$$$

Lean4

theorem sum_div_card_sq_le_sum_sq_div_card : ((∑ i ∈ s, f i) / #s) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) / #s :=
  by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp
  rw [div_pow, div_le_div_iff₀ (by positivity) (by positivity), sq (#s : α), mul_left_comm, ← mul_assoc]
  exact mul_le_mul_of_nonneg_right sq_sum_le_card_mul_sum_sq (by positivity)

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