prod_norm_eq_card — Mathlib

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

Похожие утверждения