English
For f ∈ WithLp ∞ (α × β), the norm is the maximum of the coordinate norms: ‖f‖ = ‖f.fst‖ ⊔ ‖f.snd‖.
Русский
Для f ∈ WithLp ∞ (α × β) норма равна максимуму норм координат: \|f\| = \|f.fst\| ⊔ \|f.snd\|.
LaTeX
$$$$\|f\| = \|f.fst\| \sqcup \|f.snd\|$$$$
Lean4
/-- Endowing the space `WithLp p (α × β)` with the `L^p` norm. We register this instance
separate from `WithLp.instProdSeminormedAddCommGroup` since the latter requires the type class
hypothesis `[Fact (1 ≤ p)]` in order to prove the triangle inequality.
Registering this separately allows for a future norm-like structure on `WithLp p (α × β)` for
`p < 1` satisfying a relaxed triangle inequality. These are called *quasi-norms*. -/
instance instProdNorm : Norm (WithLp p (α × β)) where
norm
f :=
if _hp : p = 0 then (if ‖f.fst‖ = 0 then 0 else 1) + (if ‖f.snd‖ = 0 then 0 else 1)
else if p = ∞ then ‖f.fst‖ ⊔ ‖f.snd‖ else (‖f.fst‖ ^ p.toReal + ‖f.snd‖ ^ p.toReal) ^ (1 / p.toReal)
