English
For a finite set s and nonnegative weights w_i and nonnegative f_i, there is a Hölder-type bound: ∑ w_i f_i ≤ (∑ w_i)^{1-1/p} (∑ w_i f_i^p)^{1/p}.
Русский
Для конечного множества s и неотрицательных весов w_i и значений f_i существует неравенство Холдер-тип: ∑ 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_of_nonneg (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
have hp₀ : 0 < p := by positivity
have hp₁ : p⁻¹ < 1 := inv_lt_one_of_one_lt₀ hp
by_cases H : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = 0 ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = 0
· replace H : (∀ i ∈ s, w i = 0) ∨ ∀ i ∈ s, w i = 0 ∨ f i = 0 := by
simpa [hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_zero_iff_of_nonneg] using H
have (i) (hi : i ∈ s) : w i * f i = 0 := by rcases H with H | H <;> simp [H i hi]
simp [sum_eq_zero this]
push_neg at H
by_cases H' : (∑ i ∈ s, w i) ^ (1 - p⁻¹) = ⊤ ∨ (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹ = ⊤
· rcases H' with H' | H' <;> simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]
replace H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤ := by
simpa [rpow_eq_top_iff, hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_top, not_or] using H'
have :=
coe_le_coe.2 <|
NNReal.inner_le_weight_mul_Lp s hp.le (fun i ↦ ENNReal.toNNReal (w i)) fun i ↦ ENNReal.toNNReal (f i)
rw [coe_mul] at this
simp_rw [coe_rpow_of_nonneg _ <| inv_nonneg.2 hp₀.le, coe_finset_sum, ← ENNReal.toNNReal_rpow, ← ENNReal.toNNReal_mul,
sum_congr rfl fun i hi ↦ coe_toNNReal (H'.2 i hi)] at this
simp [ENNReal.coe_rpow_of_nonneg, hp₁.le] at this
convert this using 2 with i hi
· obtain hw | hw := eq_or_ne (w i) 0
· simp [hw]
rw [coe_toNNReal (H'.1 _ hi), coe_toNNReal]
simpa [mul_eq_top, hw, hp₀, hp₀.not_gt, H'.1 _ hi] using H'.2 _ hi
· convert rfl with i hi
exact coe_toNNReal (H'.1 _ hi)
