Lp functions with respect to a composition of kernels and measures

theorem MeasureTheory.Measure.memLp_comp_iff {α : Type u_1} {β : Type u_2} {E : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [NormedAddCommGroup E] {κ : ProbabilityTheory.Kernel α β} {μ : Measure α} {f : β → E} {p : ENNReal} (hp0 : p ≠ 0) (hp_top : p ≠ ⊤) (hf : AEStronglyMeasurable f (μ.bind ⇑κ)) : MemLp f p (μ.bind ⇑κ) ↔ (∀ᵐ (x : α) ∂μ, MemLp f p (κ x)) ∧ Integrable (fun (x : α) => ∫ (y : β), ‖f y‖ ^ p.toReal ∂κ x) μ

theorem MeasureTheory.norm_integral_rpow_le_integral_norm_rpow {α : Type u_1} {E : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [IsProbabilityMeasure μ] [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → E} {p : ENNReal} (hp1 : 1 ≤ p) (hp_top : p ≠ ⊤) (hf : MemLp f p μ) : ‖∫ (x : α), f x ∂μ‖ ^ p.toReal ≤ ∫ (x : α), ‖f x‖ ^ p.toReal ∂μ

Jensen's inequality for the convex function x ↦ ‖x‖ ^ p, 1 ≤ p.