theorem rpow_lintegral_le {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ENNReal} (hf : AEMeasurable f μ) {r : ℝ} (hr : 1 ≤ r) : (∫⁻ (x : X), f x ∂μ) ^ r ≤ μ Set.univ ^ (r - 1) * ∫⁻ (x : X), f x ^ r ∂μ

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