theorem ENNReal.lintegral_Lp_finsum_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {ι : Type u_2} {f : ι → α → ENNReal} {I : Finset ι} (hf : ∀ i ∈ I, AEMeasurable (f i) μ) (hp : 1 ≤ p) : (∫⁻ (a : α), (∑ i ∈ I, f i) a ^ p ∂μ) ^ (1 / p) ≤ ∑ i ∈ I, (∫⁻ (a : α), f i a ^ p ∂μ) ^ (1 / p)

theorem ENNReal.lintegral_Lp_finsum_le' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ℝ} {ι : Type u_2} {f : ι → α → ENNReal} {I : Finset ι} (hf : ∀ i ∈ I, AEMeasurable (f i) μ) (hp : 1 ≤ p) : (∫⁻ (a : α), (∑ i ∈ I, f i a) ^ p ∂μ) ^ (1 / p) ≤ ∑ i ∈ I, (∫⁻ (a : α), f i a ^ p ∂μ) ^ (1 / p)

theorem ENNReal.rpow_finsetSum_le_finsetSum_rpow {p : ℝ} {ι : Type u_1} {I : Finset ι} {f : ι → ENNReal} (hp : 0 < p) (hp1 : p ≤ 1) : (∑ i ∈ I, f i) ^ p ≤ ∑ i ∈ I, f i ^ p