Commit 2022-09-01 11:45 394f6e63

View on Github →

feat(measure_theory/integral/bochner): Hölder's inequality for real nonnegative functions (#16291) We already have several versions of Hölder's inequality for the Lebesgue integral and functions with values in nnreal or ennreal. This PR introduces two versions of this inequality for the Bochner integral, one of which applies to nonnegative real functions.

Estimated changes

Modified src/measure_theory/function/ess_sup.lean

added theorem ennreal.ess_sup_mul_le

Modified src/measure_theory/function/lp_space.lean

added theorem measure_theory.mem_ℒp.smul

added theorem measure_theory.snorm_smul_le_mul_snorm

added theorem measure_theory.snorm_smul_le_snorm_mul_snorm_top

added theorem measure_theory.snorm_smul_le_snorm_top_mul_snorm

Modified src/measure_theory/integral/bochner.lean

added theorem measure_theory.integral_mul_le_Lp_mul_Lq_of_nonneg

added theorem measure_theory.integral_mul_norm_le_Lp_mul_Lq

Modified src/order/filter/ennreal.lean

added theorem ennreal.limsup_mul_le