pow_sum_div_card_le_sum_pow — Mathlib

English

Special case of Jensen's inequality for sums of powers: If f(i) ≥ 0 on s and n ∈ ℕ, then (∑ i∈s f(i))^(n+1) / |s|^n ≤ ∑ i∈s f(i)^(n+1).

Русский

Специальный случай неравенства Дженса для степеней: если f(i) ≥ 0 на s и n ∈ ℕ, то (∑ f(i))^(n+1) / |s|^n ≤ ∑ f(i)^(n+1).

LaTeX

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

Lean4

/-- Special case of **Jensen's inequality** for sums of powers. -/
theorem pow_sum_div_card_le_sum_pow (hf : ∀ i ∈ s, 0 ≤ f i) (n : ℕ) :
    (∑ i ∈ s, f i) ^ (n + 1) / #s ^ n ≤ ∑ i ∈ s, f i ^ (n + 1) :=
  by
  obtain rfl | hs := s.eq_empty_or_nonempty
  · simp
  rw [div_le_iff₀' (by positivity)]
  exact pow_sum_le_card_mul_sum_pow hf _

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