Weighted Hoelder on a set in ENNReal: (∫_s f σ)^p ≤ (∫_s f^p σ)·σ(s)^{p-1}

To get Hoelder against a density sigma on a set in ℝ≥0∞ with no finiteness hypotheses, apply ENNReal.lintegral_mul_le_Lp_mul_Lq on volume.restrict s to the two factors f * sigma^(1/p) and sigma^(1/q), where q = p/(p-1) and Real.HolderConjugate.conjExponent supplies the conjugate pair. Recombine with ENNReal.rpow_add_of_nonneg, which needs no x ≠ 0 or x ≠ top side conditions, unlike rpow_add, and with 1/p + 1/q = 1 from simpa only [one_div] using hpq.inv_add_inv_eq_one. Then rewrite with simp only [Pi.mul_apply, e1, e2, e3] at the Hoelder hypothesis and raise both sides to the power p. This one lemma gives the forward half of the two-weight weak-type theorem (stopping cube Q: t|Q| < ∫_Q f sigma).