English
For ENNReal finite sums with p and q conjugate, bound holds with ∑ f_i g_i ≤ (∑ f_i^p)^{1/p} (∑ g_i^q)^{1/q}.
Русский
Для ENNReal на конечном наборе индексов справедливо неравенство Холдера.
LaTeX
$$$\sum_{i\in s} f_i g_i \le (\sum_{i\in s} f_i^p)^{1/p} (\sum_{i\in s} g_i^q)^{1/q}$$$
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 `ℝ≥0∞`-valued functions. -/
theorem inner_le_Lp_mul_Lq (hpq : p.HolderConjugate q) :
∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) :=
by
by_cases H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0
· replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0 := by
simpa [ENNReal.rpow_eq_zero_iff, hpq.pos, hpq.symm.pos, asymm hpq.pos, asymm hpq.symm.pos,
sum_eq_zero_iff_of_nonneg] using H
have : ∀ i ∈ s, f i * g i = 0 := fun i hi => by rcases H with H | H <;> simp [H i hi]
simp [sum_eq_zero this]
push_neg at H
by_cases H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = ⊤
· rcases H' with H' | H' <;> simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
simpa [ENNReal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos, ENNReal.sum_eq_top,
not_or] using H'
have :=
ENNReal.coe_le_coe.2
(@NNReal.inner_le_Lp_mul_Lq _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _ _ hpq)
simp [ENNReal.coe_rpow_of_nonneg, hpq.pos.le, hpq.symm.pos.le] at this
convert this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp] <;>
· refine Finset.sum_congr rfl fun i hi => ?_
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul]
