theorem ENNReal.rpow_add_le_mul_rpow_add_rpow' (z₁ z₂ : ENNReal) {p : ℝ} (hp : 0 ≤ p) : (z₁ + z₂) ^ p ≤ MeasureTheory.LpAddConst (ENNReal.ofReal p)⁻¹ * (z₁ ^ p + z₂ ^ p)

theorem ENNReal.rpow_add_le_mul_rpow_add_rpow'' (z₁ z₂ : ENNReal) {p : ENNReal} : (z₁ + z₂) ^ p.toReal⁻¹ ≤ MeasureTheory.LpAddConst p * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)