Generalizing a p=2 ENNReal proof to L^p: what actually changes

When porting a p=2 lintegral proof to general p on ℝ≥0∞, most lines carry over by replacing ^2 with ^p (rpow). Three things change. (1) pow_le_pow_left₀ becomes ENNReal.rpow_le_rpow h hp0, and mul_pow becomes ENNReal.mul_rpow_of_nonneg _ _ hp0. (2) x * x^(p-1) = x^p comes from ENNReal.rpow_add_of_nonneg _ _ zero_le_one hp1 after show p = 1 + (p-1), with no x ≠ 0/∞ side conditions. (3) Indicator integrals such as ∫ (1_R)^p need ENNReal.zero_rpow_of_pos hp0 inside simp. Keeping the conjugate exponent as a hypothesis (p-1)*(s-1) = 1, rather than HolderConjugate, makes the swapped half a one-line mul_comm.