English
Let f,g: ι → ℝ≥0 with p,q conjugate. If ∑ f_i^p and ∑ g_i^q are summable, then ∑ f_i g_i converges and satisfies the Hölder bound.
Русский
Пусть f,g: ι → ℝ≥0, p,q сопряжённые. Если суммы ∑ f_i^p и ∑ g_i^q сходятся, то ∑ f_i g_i сходится и удовлетворяет неравенству Хольдера.
LaTeX
$$$\left(\sum_{i} f_i g_i\right) \text{ суммируема} \quad \text{и} \quad \sum_i f_i g_i \le (\sum_i f_i^p)^{1/p} (\sum_i 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. A version for `NNReal`-valued
functions. For an alternative version, convenient if the infinite sums are already expressed as
`p`-th powers, see `inner_le_Lp_mul_Lq_hasSum`. -/
theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.HolderConjugate q) (hf : Summable fun i => f i ^ p)
(hg : Summable fun i => g i ^ q) :
(Summable fun i => f i * g i) ∧ ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) :=
by
have H₁ : ∀ s : Finset ι, ∑ i ∈ s, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) :=
by
intro s
refine le_trans (inner_le_Lp_mul_Lq s f g hpq) (mul_le_mul ?_ ?_ bot_le bot_le)
· rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.pos)]
exact hf.sum_le_tsum _ (fun _ _ => zero_le _)
· rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.symm.pos)]
exact hg.sum_le_tsum _ (fun _ _ => zero_le _)
have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i) :=
by
refine ⟨(∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q), ?_⟩
rintro a ⟨s, rfl⟩
exact H₁ s
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
exact ⟨H₂, H₂.tsum_le_of_sum_le H₁⟩
