English
For hp: 0 < p.toReal and f ∈ WithLp p (α × β), the norm is the p‑norm of the coordinate norms: ‖f‖ = (‖f.fst‖^{p.toReal} + ‖f.snd‖^{p.toReal})^{1/p.toReal}.
Русский
Для hp: 0 < p.toReal и f ∈ WithLp p (α × β) норма равна p‑норме норм координат: \|f\| = (\|f.fst\|^{p.toReal} + \|f.snd\|^{p.toReal})^{1/p.toReal}.
LaTeX
$$$$\|f\| = \Big( \|f.fst\|^{\;p.toReal} + \|f.snd\|^{\;p.toReal} \Big)^{1 / p.toReal}$$$$
Lean4
@[simp]
theorem prod_norm_eq_card (f : WithLp 0 (α × β)) :
‖f‖ = (if ‖f.fst‖ = 0 then 0 else 1) + (if ‖f.snd‖ = 0 then 0 else 1) := by convert if_pos rfl