English
Let f,g: ι → ℝ≥0. For p ∈ ℝ, with p and q conjugate, the finite sum of products is bounded by the product of p- and q-norms: ∑ f_i g_i ≤ (∑ f_i^p)^{1/p} (∑ g_i^q)^{1/q}.
Русский
Пусть f,g: ι → ℝ≥0. При конјугированнх по Холдера p и q справедливо: конечная сумма произведений меньше або равна произведению норм p и q.
LaTeX
$$$\sum_{i \in s} f_i g_i \le \left(\sum_{i \in s} f_i^{p}\right)^{1/p} \left(\sum_{i \in s} g_i^{q}\right)^{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 (f g : ι → ℝ≥0) {p q : ℝ} (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
obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
· exact inner_le_Lp_mul_Lp_of_norm_eq_zero s f g hpq hf
obtain hg | hg := eq_zero_or_pos (∑ i ∈ s, g i ^ q)
·
calc
∑ i ∈ s, f i * g i = ∑ i ∈ s, g i * f i := by
congr with i
rw [mul_comm]
_ ≤ (∑ i ∈ s, g i ^ q) ^ (1 / q) * (∑ i ∈ s, f i ^ p) ^ (1 / p) :=
(inner_le_Lp_mul_Lp_of_norm_eq_zero s g f hpq.symm hg)
_ = (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := mul_comm _ _
let f' i := f i / (∑ i ∈ s, f i ^ p) ^ (1 / p)
let g' i := g i / (∑ i ∈ s, g i ^ q) ^ (1 / q)
suffices (∑ i ∈ s, f' i * g' i) ≤ 1
by
simp_rw [f', g', div_mul_div_comm, ← sum_div] at this
rwa [div_le_iff₀, one_mul] at this
exact mul_pos (rpow_pos hf) (rpow_pos hg)
refine inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq ?_) (le_of_eq ?_)
· simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one, div_self hf.ne']
· simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero, rpow_one, div_self hg.ne']
