English
Let p and q be conjugate exponents and let f and g be nonnegative functions indexed by i in a finite set, with the p-th power sums of f and the q-th power sums of g given as A^p and B^q, respectively. Then there exists a nonnegative C with C ≤ A·B such that the sum of products f_i g_i converges to C.
Русский
Пусть p и q сопряжены, f и g неотрицательные функции на конечном множестве индексов, причём суммы f_i^p и g_i^q равны A^p и B^q. Тогда существует неотрицательная C такая, что C ≤ A·B и сумма ∑ f_i g_i сходится к C.
LaTeX
$$$\exists C \ge 0\; (C \le AB) \;\land\; HasSum\bigl(\lambda i. f(i) \cdot g(i)\bigr)\, C$$$
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 not already expressed as
`p`-th powers, see `inner_le_Lp_mul_Lq_tsum_of_nonneg`. -/
theorem inner_le_Lp_mul_Lq_hasSum_of_nonneg (hpq : p.HolderConjugate q) {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B)
(hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) (hf_sum : HasSum (fun i => f i ^ p) (A ^ p))
(hg_sum : HasSum (fun i => g i ^ q) (B ^ q)) : ∃ C : ℝ, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C :=
by
lift f to ι → ℝ≥0 using hf
lift g to ι → ℝ≥0 using hg
lift A to ℝ≥0 using hA
lift B to ℝ≥0 using hB
beta_reduce at *
norm_cast at hf_sum hg_sum
obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum
refine ⟨C, C.prop, hC, ?_⟩
norm_cast
