mathlib3

f0ceb6bb - feat(analysis/mean_inequalities): add young_inequality for nnreal and ennreal with real exponents (#5242)

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. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>