The triangle bound for the ℓ^p product norm

Mathlib bounds each factor of WithLp p (α × β) by the whole (WithLp.norm_fst_le and WithLp.norm_snd_le) and computes the norm exactly for p = 1 and p = 2. This file records the opposite bound, valid for every exponent 1 ≤ p ≤ ∞: the ℓ^p norm of a pair is at most the sum of the norms of its two components. For p = 1 the bound is an identity for every pair.

Main statements

• WithLp.prod_norm_le_norm_fst_add_norm_snd — the bound ‖x‖ ≤ ‖x.fst‖ + ‖x.snd‖.

theorem WithLp.prod_norm_le_norm_fst_add_norm_snd {p : ENNReal} [Fact (1 ≤ p)] {α : Type u_1} {β : Type u_2} [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (x : WithLp p (α × β)) : ‖x‖ ≤ ‖x.fst‖ + ‖x.snd‖

The ℓ^p norm of a pair is at most the sum of the norms of its two components.