theorem norm_toLp_eq_sum_component_norm_rpow {m : ℕ} {p : ℝ} {E : Fin m → Type u} [(i : Fin m) → NormedAddCommGroup (E i)] (hp : 1 ≤ p) (u : (i : Fin m) → E i) : ‖WithLp.toLp (ENNReal.ofReal p) u‖ = (∑ i : Fin m, ‖u i‖ ^ p) ^ (1 / p)

The canonical PiLp norm on a finite family of normed spaces is the textbook composite l_p norm formula.