English
For nonnegative w_i and f_i, ∑ w_i f_i ≤ (∑ w_i)^{1-1/p} (∑ w_i f_i^p)^{1/p} when p≥1.
Русский
Для неотрицательных w_i и f_i выполняется неравенство Хольдера со взвешиванием.
LaTeX
$$$\sum_{i\in s} w_i f_i \le \left(\sum_{i\in s} w_i\right)^{1-\frac{1}{p}} \left(\sum_{i\in s} w_i f_i^{p}\right)^{\frac{1}{p}}$$$
Lean4
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. Version for sums over finite sets,
with real-valued nonnegative functions. -/
theorem inner_le_Lp_mul_Lq_of_nonneg (hpq : HolderConjugate p q) (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) :
∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := by
convert inner_le_Lp_mul_Lq s f g hpq using 3 <;> apply sum_congr rfl <;> intro i hi <;>
simp only [abs_of_nonneg, hf i hi, hg i hi]
