English
The Lp-norm of the infinite sum is bounded by the sum of Lp-norms for summable sequences.
Русский
Норма Lp бесконечной суммы ограничена суммой норм Lp для сходящихся поLp последовательностей.
LaTeX
$$$\left(\sum_{i} (f_i+g_i)^p\right)^{1/p} \le \left(\sum_i f_i^p\right)^{1/p} + \left(\sum_i g_i^p\right)^{1/p}$$$
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 `ℝ`-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_of_nonneg`. -/
theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.HolderConjugate q) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i)
(hf_sum : Summable fun i => f i ^ p) (hg_sum : 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
lift f to ι → ℝ≥0 using hf
lift g to ι → ℝ≥0 using hg
beta_reduce at *
norm_cast at *
exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum
