Convexity of the finite-dimensional norm and the power smoothing kernel.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lpNorm_add_le {d : ℕ} {p : ℝ} (hp : 1 ≤ p) (u v : Point d) : lpNorm p (u + v) ≤ lpNorm p u + lpNorm p v

theorem V7.Stage5AboveTwoLowerS5A2Envelope.convexOn_lpNorm {p : ℝ} (hp : 1 ≤ p) {d : ℕ} : ConvexOn ℝ Set.univ (lpNorm p)

Convexity of the literal finite-dimensional lpNorm, kept in the same representation as the frozen carrier.

theorem V7.Stage5AboveTwoLowerS5A2Envelope.lowerKernelPhi_convex {r theta : ℝ} (hr : 1 ≤ r) (htheta : 1 < theta) {d : ℕ} : O3.IsConvexObjective (lowerKernelPhi r theta)

Convexity of the concrete kernel follows from norm convexity and convex, monotone real power on the nonnegative half-line.