English
Let s be a finite index set, p>1, weights w_i ≥ 0 and functions f_i ≥ 0. Then sum w_i f_i ≤ (sum w_i)^{1-1/p} (sum w_i f_i^p)^{1/p}.
Русский
Пусть есть конечный множество индексов, веса w_i ≥ 0 и функции f_i ≥ 0. Тогда ∑ w_i f_i ≤ (∑ w_i)^{1-1/p} (∑ w_i f_i^p)^{1/p}.
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
/-- **Weighted Hölder inequality**. -/
theorem inner_le_weight_mul_Lp (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι → ℝ≥0) :
∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ :=
by
obtain rfl | hp := hp.eq_or_lt
· simp
calc
_ = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i) := ?_
_ ≤ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) * (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) :=
(inner_le_Lp_mul_Lq _ _ _ (.symm <| Real.holderConjugate_iff.mpr ⟨hp, by simp⟩))
_ = _ := ?_
· congr with i
rw [← mul_assoc, ← rpow_of_add_eq _ one_ne_zero, rpow_one]
simp
· have hp₀ : p ≠ 0 := by positivity
have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne']
simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁]
