Hölder Inequality for ENNReal-Valued Infinite Sums

This file provides a tsum version of Hölder's inequality for ℝ≥0∞-valued functions, obtained by specializing the lintegral Hölder inequality to the counting measure.

The main advantage over NNReal.inner_le_Lp_mul_Lq_tsum in Mathlib is that no Summable hypotheses are needed: ℝ≥0∞ sums always converge (to ⊤ in the worst case).

Main Results

• ENNReal.inner_le_Lp_mul_Lq_tsum: Hölder's inequality for ℝ≥0∞-valued tsum.

theorem ENNReal.inner_le_Lp_mul_Lq_tsum {ι : Type u_1} {p q : ℝ} (hpq : p.HolderConjugate q) (f g : ι → ENNReal) : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Hölder's inequality for ℝ≥0∞-valued infinite sums: ∑' i, f i * g i ≤ (∑' i, f i ^ p) ^ (1/p) * (∑' i, g i ^ q) ^ (1/q).

Obtained by specializing ENNReal.lintegral_mul_le_Lp_mul_Lq to the counting measure with DiscreteMeasurableSpace. No Summable hypotheses are needed.