Young's inequality with a parameter in ℝ≥0∞ by a case split (no convexity)

For conjugate exponents stated as (p-1)*(s-1) = 1, x*y ≤ ε⁻¹*x^p + ε^(s-1)*y^s on ℝ≥0∞ has a short proof without convexity or Real.add_pow_le_pow_mul_pow_of_add_eq_one. Case y ≤ ε⁻¹*x^(p-1): then x*y ≤ ε⁻¹*x*x^(p-1), and x*x^(p-1) = x^p by ENNReal.rpow_add_of_nonneg, which needs no ≠0/≠∞ side conditions. Otherwise x^(p-1) ≤ ε*y, so x = (x^(p-1))^(s-1) ≤ (ε*y)^(s-1), using ← ENNReal.rpow_mul and hps. Then x*y ≤ ε^(s-1)*y^s. Stating two-weight splitting conditions with averages, (avg_g)^s*ν(Q) ≤ (avg_f)^p*μ(Q), rather than integrals with ν(Q)^(1-s), also removes every ν(Q)=0 case split.