Commit 2020-12-07 08:45 f0ceb6bb
View on Github →feat(analysis/mean_inequalities): add young_inequality for nnreal and ennreal with real exponents (#5242) The existing young_inequality for nnreal has nnreal exponents. This adds a version with real exponents with the is_conjugate_exponent property, and a similar version for ennreal with real exponents.