theorem convexOn_subsingleton {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Subsingleton E] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [Module 𝕜 β] (s : Set E) (f : E → β) : ConvexOn 𝕜 s f

theorem convexOn_rpow_norm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ Set.univ fun (x : E) => ‖x‖ ^ p

theorem lpNorm_congr {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [NormedAddCommGroup ε] {f g : α → ε} (hfg : f =ᵐ[μ] g) : MeasureTheory.lpNorm f p μ = MeasureTheory.lpNorm g p μ

theorem lpNorm_rpow_nnreal_eq_integral {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup ε] {f : α → ε} {p : NNReal} (hp : p ≠ 0) (hf : MeasureTheory.AEStronglyMeasurable f μ) : MeasureTheory.lpNorm f (↑p) μ ^ ↑p = ∫ (a : α), ‖f a‖ ^ ↑p ∂μ