Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-08 13:47 64ddb126

View on Github →

feat(analysis/mean_inequalities): add Hölder's inequality for the Lebesgue integral of ennreal and nnreal functions (#5267)

Estimated changes

Modified src/analysis/mean_inequalities.lean

added theorem ennreal.ae_eq_zero_of_lintegral_rpow_eq_zero

added theorem ennreal.fun_eq_fun_mul_inv_snorm_mul_snorm

added def ennreal.fun_mul_inv_snorm

added theorem ennreal.fun_mul_inv_snorm_rpow

added theorem ennreal.lintegral_mul_eq_zero_of_lintegral_rpow_eq_zero

added theorem ennreal.lintegral_mul_le_Lp_mul_Lq

added theorem ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top

added theorem ennreal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_ne_top

added theorem ennreal.lintegral_mul_le_one_of_lintegral_rpow_eq_one

added theorem ennreal.lintegral_rpow_fun_mul_inv_snorm_eq_one

added theorem nnreal.lintegral_mul_le_Lp_mul_Lq

Modified src/analysis/special_functions/pow.lean

added theorem ennreal.inv_rpow_of_pos

added theorem nnreal.of_real_rpow_of_nonneg

Modified src/data/real/conjugate_exponents.lean

added theorem real.is_conjugate_exponent.inv_add_inv_conj_ennreal

Modified src/data/real/ennreal.lean

added theorem ennreal.of_real_div_of_pos

added theorem ennreal.of_real_inv_of_pos

Modified src/measure_theory/integration.lean

added theorem measure_theory.lintegral_zero_fun